Debug printing update, now the unification bug

seems to be in tac_zero_inf_pos.

We get '0 < 1 + 0' instead of '0 < 1'.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 446b2ef4b0ac92f95be24194ee6021fc5cb78f27..5fa37103070316b30b6d96e8980137335bf5e7f8 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -428,62 +428,48 @@ Construction de la preuve en cas de succ
 i.e. on obtient une contradiction.
 *)
 
-let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
+
+let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
+let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
 let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
 let _R1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") 0 ;;
+let _R = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") 0 ;;
+let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
+let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
+let _Rfourier_ge_to_le  =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
+let _Rfourier_gt_to_lt         =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
+let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
+let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
+let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
+let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
+let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
+let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
+let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
+let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
+let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
+let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
 let _Rinv  = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
+let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
+let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
 let _Rle_mult_inv_pos =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") 0 ;;
 let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") 0 ;;
 let _Rle_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_1.con") 0 ;;
 let _Rle_zero_pos_plus1 =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_pos_plus1.con") 0 ;;
 let _Rle_zero_zero = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_zero_zero.con") 0 ;;
+let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
 let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") 0 ;;
 let _Rlt_not_le =  Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") 0 ;;
 let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") 0 ;;
 let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
 let _Rminus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con") 0 ;;
-
+let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
+let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
 let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") 0 ;;
+let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
 let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") 0 ;;
 let _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") 0 ;;
-let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") 0 ;;
-let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") 0 ;;
-let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") 0 ;;
-let _Rfourier_gt_to_lt         =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") 0 ;;
-
-let _Rfourier_ge_to_le  =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") 0 ;;
-let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") 0 ;;
-let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") 0 ;;
-let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") 0 ;;
-let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") 0 ;;
-
-let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") 0 ;;
-
-let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") 0 ;;
-let _Rlt = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") 0 ;;
-let _Rle = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") 0 ;;
-let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
-
 let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
-
-let _Rfourier_lt=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") 0 ;;
-let _Rfourier_le=Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") 0 ;;
- 
-let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
-
-let _Rinv_R1 = Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) 0;;
-
-
-let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") 0 ;;
-let _Rnot_le_le =Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") 0 ;;
-
-
-
-
-
-
+(*****************************************************************************************************)
 let is_int x = (x.den)=1
 ;;
 
@@ -521,6 +507,8 @@ let rational_to_real x =
 (* preuve que 0<n*1/d
 *)
 
+
+(*
 let tac_zero_inf_pos gl (n,d) =
    (*let cste = pf_parse_constr gl in*)
    let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
@@ -530,9 +518,38 @@ let tac_zero_inf_pos gl (n,d) =
    for i=1 to d-1 do
        tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd); done;
    (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) ~continuations:[!tacn;!tacd])
-;;
+;;*)
+let tac_zero_inf_pos (n,d) ~status =
+   (*let cste = pf_parse_constr gl in*)
+   let pall str ~status:(proof,goal) t =
+     debug ("tac "^str^" :\n" );
+     let curi,metasenv,pbo,pty = proof in
+     let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+     debug ("th = "^ CicPp.ppterm t ^"\n"); 
+     debug ("ty = "^ CicPp.ppterm ty^"\n"); 
+   in
+   let tacn=ref 
+     (fun ~status -> pall "n0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
+   let tacd=ref 
+     (fun ~status -> pall "d0" ~status _Rlt_zero_1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ~status ) in
 
 
+  for i=1 to n-1 do 
+       tacn:=(Tacticals.then_ ~start:(fun ~status -> pall ("n"^string_of_int i) ~status _Rlt_zero_pos_plus1;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacn); done;
+   for i=1 to d-1 do
+       tacd:=(Tacticals.then_ ~start:(fun ~status -> pall "d" ~status _Rlt_zero_pos_plus1 ;PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1 ~status) ~continuation:!tacd); done;
+
+
+
+debug("\nTAC ZERO INF POS\n");
+
+(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos) 
+  ~continuations:[
+   !tacn ;
+   !tacd ] 
+  ~status)
+;;
+
 
 
 (* preuve que 0<=n*1/d
@@ -570,7 +587,7 @@ let tac_zero_inf_false gl (n,d) =
 
 let tac_zero_infeq_false gl (n,d) =
      (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
-             ~continuation:(tac_zero_inf_pos gl (-n,d)))
+             ~continuation:(tac_zero_inf_pos (-n,d)))
 ;;
 
 
@@ -615,18 +632,24 @@ let my_cut ~term:c ~status:(proof,goal)=
 
 let exact = PrimitiveTactics.exact_tac;;
 
-let tac_use h = match h.htype with
-               "Rlt" -> exact ~term:h.hname
-              |"Rle" -> exact ~term:h.hname
-              |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
-                                ~continuation:(exact ~term:h.hname))
-              |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
-                                ~continuation:(exact ~term:h.hname))
-              |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
-                                ~continuation:(exact ~term:h.hname))
-              |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
-                                ~continuation:(exact ~term:h.hname))
-              |_->assert false
+let tac_use h ~status = 
+debug("Inizio TC_USE\n");
+let res = 
+match h.htype with
+  "Rlt" -> exact ~term:h.hname ~status
+  |"Rle" -> exact ~term:h.hname ~status
+  |"Rgt" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_gt_to_lt)
+      ~continuation:(exact ~term:h.hname)) ~status
+  |"Rge" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_ge_to_le)
+      ~continuation:(exact ~term:h.hname)) ~status
+  |"eqTLR" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqLR_to_le)
+      ~continuation:(exact ~term:h.hname)) ~status
+  |"eqTRL" -> (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_eqRL_to_le)
+      ~continuation:(exact ~term:h.hname)) ~status
+  |_->assert false
+in
+debug("Fine TAC_USE");
+res
 ;;
 
 
@@ -863,43 +886,55 @@ let rec fourier ~status:(s_proof,s_goal)=
        
           debug "inizio a costruire tac1\n";
          
-          let tac1=ref ( if h1.hstrict then 
+          let tac1=ref ( fun ~status -> 
+                       debug "Sotto tattica t1\n";
+                       if h1.hstrict then 
                            (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_lt)
-                                             ~continuations:[tac_use h1;tac_zero_inf_pos goal            
-                                                    (rational_to_fraction c1)])
+                                             ~continuations:[tac_use h1;tac_zero_inf_pos (rational_to_fraction c1)] ~status)
                          else 
                            (Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le)
-                                             ~continuations:[tac_use h1;tac_zero_inf_pos  goal
-                                                    (rational_to_fraction c1)]))
+                                             ~continuations:[tac_use h1;tac_zero_inf_pos                                                 (rational_to_fraction c1)] ~status))
+                                                   
           in
           s:=h1.hstrict;
          
           List.iter (fun (h,c) -> 
                (if (!s) then 
                    (if h.hstrict then 
+                       (debug("tac1 1\n");
                        tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
                                                       ~term:_Rfourier_lt_lt)
                                               ~continuations:[!tac1;tac_use h;
-                                                      tac_zero_inf_pos  goal 
-                                                      (rational_to_fraction c)])
+                                                      tac_zero_inf_pos   
+                                                      (rational_to_fraction c)]))
                    else 
+                   (
+                       debug("tac1 2\n");
                        tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac 
                                                       ~term:_Rfourier_lt_le)
                                               ~continuations:[!tac1;tac_use h; 
-                                                      tac_zero_inf_pos  goal
-                                                       (rational_to_fraction c)])
+                                                      tac_zero_inf_pos  
+                                                       (rational_to_fraction c)]))
                     )
                else 
                    (if h.hstrict then 
+                       (
+                       
+                       debug("tac1 3\n");
                        tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_lt)
                                               ~continuations:[!tac1;tac_use h; 
-                                                      tac_zero_inf_pos  goal
-                                                       (rational_to_fraction c)])
+                                                      tac_zero_inf_pos  
+                                                       (rational_to_fraction c)]))
                    else 
-                       tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
+                       (
+                       debug("tac1 4\n");
+                       tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
                                               ~continuations:[!tac1;tac_use h; 
-                                                      tac_zero_inf_pos  goal
-                                                       (rational_to_fraction c)])));
+                                                      tac_zero_inf_pos  
+                                                       (rational_to_fraction c)]))
+                                                      
+                                                      )
+                                                     );
              s:=(!s)||(h.hstrict))
               lutil;(*end List.iter*)
              
@@ -953,7 +988,7 @@ let rec fourier ~status:(s_proof,s_goal)=
       |_-> assert false)(*match (!lutil) *)
   |_-> assert false); (*match res*)
 
-  debug ("finalmente applico t1\n");
+  debug ("finalmente applico tac\n");
   (!tac ~status:(proof,goal)) 
 
 ;;