bug found:

 - >= is splitted in > or = ,so unification fails

diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic
index cae3925a7102fc58a1539f7c2a72e6994ff76374..09caea79be6c9617500e850bb255e7c9b15ca5ee 100644 (file)
--- a/helm/gTopLevel/esempi/fourier.cic
+++ b/helm/gTopLevel/esempi/fourier.cic
@@ -1,8 +1,35 @@
 alias Rge       /Coq/Reals/Rdefinitions/Rge.con
 alias Rle       /Coq/Reals/Rdefinitions/Rle.con
+alias Rgt       /Coq/Reals/Rdefinitions/Rgt.con
+alias Rlt       /Coq/Reals/Rdefinitions/Rlt.con
+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 R1        /Coq/Reals/Rdefinitions/R1.con
+alias R0        /Coq/Reals/Rdefinitions/R0.con
 alias R        /Coq/Reals/Rdefinitions/R.con
+alias Eq       /Coq/Init/Logic_Type/eqT.ind#1/1
 
+//test base1 ok
 !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1))
+
+//test base2 ok
+!x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+
+//test base3 (unification fails)
+!x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 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 (unification fails)
+!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1))
+
+//test base7 (should fail) ok
+!x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1))
+
+

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index c23cc448ddf4e826816931608f93035aa99fc82d..a4630ab7aca1e47db84676838ceaead5d6ffb742 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -31,7 +31,9 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
  let module U = UriManager in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
-   let eq_ind_r,ty,t1,t2 = 
+
+  prerr_endline("rewrite chiamata con "^CicPp.ppterm gty^"\n");
+  let eq_ind_r,ty,t1,t2 = 
     match CicTypeChecker.type_of_aux' metasenv context equality with
        C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/Equality/eq.ind") ->
@@ -79,6 +81,8 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
       (proof',[fresh_meta])
 ;;
 
+(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*)
+
 
 
 let simpl_tac ~status:(proof,goal) =
@@ -391,6 +395,7 @@ type hineq={hname:Cic.term; (* le nom de l'hypoth
 *)
 
 let ineq1_of_term (h,t) =
+       debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
     match t with (* match t *)
        Cic.Appl (t1::next) ->
          let arg1= List.hd next in
@@ -433,14 +438,16 @@ 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" ->  
-                          let t0= arg1 in
+                "cic:/Coq/Init/Logic_Type/eqT.ind" ->  
+                          debug("Ho trovato una ==\n");
+                          let t0= arg1 in
                            let arg1= arg2 in
                            let arg2= List.hd(List.tl (List.tl next)) in
                    (match t0 with
                          Cic.Const (u,boh) ->
                           (match UriManager.string_of_uri u with
                              "cic:/Coq/Reals/Rdefinitions/R.con"->
+                             
                          [{hname=h;
                            htype="eqTLR";
                           hleft=arg1;
@@ -455,11 +462,11 @@ let ineq1_of_term (h,t) =
                           hflin= flin_minus (flin_of_term arg2)
                                              (flin_of_term arg1);
                           hstrict=false}]
-                           |_-> assert false)
-                         |_-> assert false)
-                   |_-> assert false)
-          |_-> assert false)(* match t1 *)
-        |_-> assert false (* match t *)
+                           |_-> debug("eqT deve essere applicato a const R\n");assert false)
+                         |_-> debug("eqT deve essere appl a const\n");assert false)
+                   |_-> debug("Il trmine e' un appl mutind ma non eqT\n");assert false)
+          |_-> debug("Il termine non e' una app di const o app di mutind\n");assert false)(* match t1 *)
+        |_-> debug("Il termine non e' una applicazione\n");assert false (* match t *)
 ;;
 (* coq wrapper 
 let ineq1_of_constr = ineq1_of_term;;
@@ -741,13 +748,19 @@ let tac_zero_inf_false gl (n,d) ~status=
 (* preuve que 0<=(-n)*(1/d) => False 
 *)
 
-let tac_zero_infeq_false gl (n,d) ~status=
-debug("stat tac_zero_infeq_false");
-let r = 
-     (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+debug("stat tac_zero_infeq_false\n");
+(*let r = 
+     (
+     let curi,metasenv,pbo,pty = proof in
+     let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+     
+     debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+     Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
              ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
-        debug("stat tac_zero_infeq_false");
-        r
+ debug("end tac_zero_infeq_false\n");
+ r*)
+ Ring.id_tac ~status
 ;;
 
 
@@ -901,7 +914,7 @@ debug("inizio EQ\n");
    let irl =
     ProofEngineHelpers.identity_relocation_list_for_metavariable context in
    let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
-debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
+debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n");
    let (proof,goals) =
     rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl))
      ~status:((curi,metasenv',pbo,pty),goal)
@@ -1010,7 +1023,7 @@ theoreme,so let's parse our thesis *)
   (* transform hyps into inequations *)
   
   List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
-                       with _-> ())
+                       with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
               hyps;
 
            
@@ -1021,7 +1034,7 @@ theoreme,so let's parse our thesis *)
   let tac=ref Ring.id_tac in
   if res=[] then 
        (print_string "Tactic Fourier fails.\n";flush stdout;
-        failwith "fourier_tac fails")
+        failwith "fourier can't proove it")
   else 
   (
   match res with (*match res*)
@@ -1176,7 +1189,8 @@ theoreme,so let's parse our thesis *)
                  r)
               ~continuations:[(Tacticals.thens 
                 ~start:(
-                  fun ~status ->
+                  fun ~status:(proof,goals as status) ->
+
                   let r = equality_replace (Cic.Appl[_Rinv;_R1]) _R1 ~status in
                   (match r with (p,gl) ->
                     debug("eq2 ritorna "^string_of_int(List.length gl)^"\n" ));
@@ -1218,6 +1232,7 @@ theoreme,so let's parse our thesis *)
                    goal) metasenv in
                   (* check if ty is of type *)
                   let w1 = 
+                    debug("qui c'e' gia' l'or "^CicPp.ppterm ty^"\n");
                     (match ty with
                     (* Fix: aspetta mail di Claudio per capire cosa comporta anonimous*)
                     Cic.Prod (Cic.Anonimous,a,b) -> (Cic.Appl [_not;a])
@@ -1227,8 +1242,8 @@ theoreme,so let's parse our thesis *)
                   debug("fine MY_CHNGE\n");
                   r
                  ) 
-                ~continuation:tac2]))
-        ;!tac1]);(*end tac:=*)
+                ~continuation:Ring.id_tac(*tac2*)]))
+        ;Ring.id_tac(*!tac1*)]);(*end tac:=*)
        tac:=(Tacticals.thens 
          ~start:(PrimitiveTactics.cut_tac ~term:_False)
         ~continuations:[Tacticals.then_