From: Enrico Tassi Date: Wed, 20 Nov 2002 15:53:35 +0000 (+0000) Subject: - removed: cut_tac False to demostrate False X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=44fca010f5f7c9585c9530c4b6b30cd774b7cd1c;p=helm.git - removed: cut_tac False to demostrate False - removed: apply_tac Rle_zero_zero - a new big example --- diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index dc883e4e4..ba51e64ad 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -12,7 +12,37 @@ alias R0 /Coq/Reals/Rdefinitions/R0.con alias R /Coq/Reals/Rdefinitions/R.con alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 alias not /Coq/Init/Logic/not.con - +alias or /Coq/Init/Logic/or.ind#1/1 + +(*test real*) +!x:R.!y:R.!z:R. +(Rge +(Rplus + (Rmult (Ropp (Rplus R1 R1)) x) (Rplus + (Rmult (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))) y) (Rplus + (Rmult (Rplus R1 (Rplus R1 R1)) z) R1) +)) R0) +-> +(Rge +(Rplus + (Rmult (Ropp (Rplus R1 (Rplus R1 R1))) x) (Rplus + (Rmult (Ropp (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 (Rplus R1 R1)))))) y) (Rplus + R1 (Rplus R1 R1)) +)) R0) +-> +(Rgt +(Rplus + x (Rplus + (Rmult (Rplus R1 R1) y) (Ropp z) ) +) R0) +-> +(Rgt +(Rplus + (Rmult (Rplus R1 (Rplus R1 R1)) x) (Rplus + z (Ropp R1)) +) R0) + +-> (Rlt z R1) //test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) @@ -25,19 +55,35 @@ alias not /Coq/Init/Logic/not.con /Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con +intros + /Coq/Init/Logic/False.ind#1/1 -(Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))) +(not (Rle (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)))) /Coq/fourier/Fourier_util/Rnot_le_le.con t1=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) + t2=(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) + +(t1-t2)=(Rminus +(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y)) +(Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x))) + tc=(Rmult (Ropp R1) (Rinv R1)) rewrite=(eqT R (Rminus (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus y R1)) (Rmult (Rmult R1 (Rinv R1)) x)) (Rplus (Rmult (Rmult R1 (Rinv R1)) (Rplus x (Rplus R1 R1))) (Rmult (Rmult R1 (Rinv R1)) y))) (Rmult (Ropp R1) (Rinv R1))) +change=(not (or +(Rlt R0 (Rmult (Ropp R1) (Rinv R1))) +(eqT R R0 (Rmult (Ropp R1) (Rinv R1))) +)) + +tac2 +/Coq/fourier/Fourier_util/Rnot_lt0.con + //test base4 ok !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1)) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index 90657b598..17ff3f8fe 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -531,8 +531,8 @@ let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") [] ;; let _Rle_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") [] ;; -let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string - "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;; +(*let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string + "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") [] ;;*) let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;; let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string @@ -647,11 +647,11 @@ let tac_zero_infeq_pos gl (n,d) ~status = (*let cste = pf_parse_constr gl in*) debug("inizio tac_zero_infeq_pos\n"); let tacn = ref - (if n=0 then + (*(if n=0 then (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero ) - else + else*) (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 ) - ) + (* ) *) in let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in for i=1 to n-1 do @@ -748,8 +748,10 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = let metasenv' = (fresh_meta,context,t)::metasenv in let proof' = curi,metasenv',pbo,pty in let proof'',goals = - PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (Cic.Meta - (fresh_meta,irl),t))::al)) ~status:(proof',goal) + PrimitiveTactics.apply_tac + (*~term:(Cic.Appl ((Cic.Cast (Cic.Meta (fresh_meta,irl),t))::al)) (* ??? *)*) + ~term:(Cic.Appl ((Cic.Meta (fresh_meta,irl))::al)) (* ??? *) + ~status:(proof',goal) in proof'',fresh_meta::goals ;; @@ -1141,7 +1143,7 @@ theoreme,so let's parse our thesis *) in tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) - ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)Tacticals.then_ + ~continuations:[(*Tacticals.id_tac;Tacticals.id_tac*)(**)Tacticals.then_ ~start:(fun ~status:(proof,goal as status) -> let curi,metasenv,pbo,pty = proof in let metano,context,ty = List.find (function (m,_,_) -> m=goal) @@ -1170,25 +1172,6 @@ theoreme,so let's parse our thesis *) r) ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1 -(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno - di applicare sym_eqT. Perche' in Coq il goal e' al contrario? Forse i - parametri della equality_replace vengono passati al contrario? Oppure la - tattica usa i parametri al contrario? - CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac - ~continuations:[Tacticals.then_ - ~start:( - fun ~status:(proof,goal as status) -> - debug("ECCOCI\n"); - let curi,metasenv,pbo,pty = proof in - let metano,context,ty = List.find (function (m,_,_) -> m= - goal) metasenv in - debug("ty = "^CicPp.ppterm ty^"\n"); - let r = PrimitiveTactics.apply_tac ~term:_sym_eqT - ~status in - debug("fine ECCOCI\n"); - r) - ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1) -*) ;Tacticals.try_tactics ~tactics:[ "ring", (fun ~status -> debug("begin RING\n"); @@ -1197,7 +1180,8 @@ theoreme,so let's parse our thesis *) r) ; "id", Tacticals.id_tac] ]) - ;Tacticals.then_ + ;(*Tacticals.id_tac*) + Tacticals.then_ ~start: ( fun ~status:(proof,goal as status) -> @@ -1215,6 +1199,7 @@ theoreme,so let's parse our thesis *) let r = PrimitiveTactics.change_tac ~what:ty ~with_what:w1 ~status in debug("fine MY_CHNGE\n"); r + ) ~continuation:(*PORTINGTacticals.id_tac*)tac2])) ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*) @@ -1223,14 +1208,18 @@ theoreme,so let's parse our thesis *) ~continuations:[Tacticals.then_ ~start:(PrimitiveTactics.intros_tac ~name:"??") ~continuation:contradiction_tac - ;!tac])*) - tac:=!tac + ;!tac]) FIXED - this was useless*) + (* tac:=!tac*) |_-> assert false)(*match (!lutil) *) |_-> assert false); (*match res*) debug ("finalmente applico tac\n"); - (!tac ~status:(proof,goal)) + ( + let r = !tac ~status:(proof,goal) in + debug("\n\n]]]]]]]]]]]]]]]]]) That's all folks ([[[[[[[[[[[[[[[[[[[\n\n");r + + ) ;; let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;