An old bug in 'eqT' hipotesys solved

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index a76b4586a2076712830eccd035a83c702f29e0ca..dc883e4e4888fd11463339122b528af7320bd3d7 100644 (file)
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -6,10 +6,13 @@ alias Ropp     /Coq/Reals/Rdefinitions/Ropp.con
 alias Rinv     /Coq/Reals/Rdefinitions/Rinv.con
 alias Rplus     /Coq/Reals/Rdefinitions/Rplus.con
 alias Rminus    /Coq/Reals/Rdefinitions/Rminus.con
+alias Rmult    /Coq/Reals/Rdefinitions/Rmult.con
 alias R1        /Coq/Reals/Rdefinitions/R1.con
 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
+
 
 //test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
@@ -20,13 +23,28 @@ alias eqT   /Coq/Init/Logic_Type/eqT.ind#1/1
 //test base3 ok
 !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1)))
 
+/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con
+
+/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)))
+
+/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))
+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)))
+
 //test base4 ok
 !x:R.!y:R.(Rgt x y) -> (Rle (Rminus y R1) (Rplus x R1))
 
 //test base5 ok
 !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0))
 
-//test base6 (fourier fails)
+//test base6 ok
 !x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
 
 //test base7 (should fail) ok

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 66e895119daf37b7239ef88b48f46dad0d9ad6da..90657b598fbbcaf5576e32e4b423489c143f56a3 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -394,7 +394,7 @@ let ineq1_of_term (h,t) =
                 |_->assert false)(* match u *)
           | Cic.MutInd (u,i,o) ->
               (match UriManager.string_of_uri u with 
-                "cic:/Coq/Init/Logic_Type/eqT.con" ->  
+                "cic:/Coq/Init/Logic_Type/eqT.ind" ->  
                           let t0= arg1 in
                            let arg1= arg2 in
                            let arg2= List.hd(List.tl (List.tl next)) in
@@ -762,6 +762,9 @@ let my_cut ~term:c ~status:(proof,goal)=
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
 
+debug("my_cut di "^CicPp.ppterm c^"\n");
+
+
   let fresh_meta = ProofEngineHelpers.new_meta proof in
   let irl =
    ProofEngineHelpers.identity_relocation_list_for_metavariable context in
@@ -923,7 +926,7 @@ let assumption_tac ~status:(proof,goal)=
 (* !!!!! fix !!!!!!!!!! *)
 let contradiction_tac ~status:(proof,goal)=
        Tacticals.then_ 
-               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+               ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima  della chiamata*)
                ~continuation:(Tacticals.then_ 
                        ~start:(Ring.elim_type_tac ~term:_False) 
                        ~continuation:(assumption_tac))
@@ -1138,7 +1141,7 @@ theoreme,so let's parse our thesis *)
        in
        tac:=(Tacticals.thens 
          ~start:(my_cut ~term:ineq) 
-         ~continuations:[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) 
@@ -1151,6 +1154,7 @@ theoreme,so let's parse our thesis *)
             ~continuation:(Tacticals.thens 
               ~start:( 
                 fun ~status ->
+                debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
                 let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc 
                  ~status
                 in
@@ -1214,12 +1218,13 @@ theoreme,so let's parse our thesis *)
                  ) 
                 ~continuation:(*PORTINGTacticals.id_tac*)tac2]))
         ;(*Tacticals.id_tac*)!tac1]);(*end tac:=*)
-       tac:=(Tacticals.thens 
+       (*tac:=(Tacticals.thens 
          ~start:(PrimitiveTactics.cut_tac ~term:_False)
         ~continuations:[Tacticals.then_ 
           ~start:(PrimitiveTactics.intros_tac ~name:"??")
           ~continuation:contradiction_tac
-        ;!tac])
+        ;!tac])*)
+        tac:=!tac
 
 
     |_-> assert false)(*match (!lutil) *)