- porting to the new theory with explicit named substitutions completed

- bug fixed: fold used to undo an over-simplification of RewriteSimpl

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 247a47248600e87d270f561bb3398d5480c4e20b..bdba623190cc8ab47fa6b533f232ff5a26aec7a7 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -33,14 +33,14 @@ let rewrite_tac ~term:equality ~status:(proof,goal) =
   let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
    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]
+       C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind") ->
          let eq_ind_r =
           C.Const
            (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
          in
           eq_ind_r,ty,t1,t2
-     | C.Appl [C.MutInd (uri,0,_) ; ty ; t1 ; t2]
+     | C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
         when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
          let eqT_ind_r =
           C.Const
@@ -78,9 +78,9 @@ prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
       (proof',[fresh_meta])
 ;;
 
-let rewrite_simpl_tac ~term =
- Tacticals.then_ ~start:(rewrite_tac ~term)
-  ~continuation:ReductionTactics.simpl_tac
+
+let rewrite_simpl_tac ~term ~status =
+ Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:ReductionTactics.simpl_tac ~status
 ;;
 
 (******************** THE FOURIER TACTIC ***********************)
@@ -198,23 +198,6 @@ let flin_emult a f =
 (*****************************************************************************)
 
 
-(**
-       @param t a term
-       @return proiection on string of t
-*)
-let rec string_of_term t =
- match t with
-   Cic.Cast  (t,_) -> string_of_term t
-  |Cic.Const (u,_) -> UriManager.string_of_uri u
-  |Cic.Var   (u,_) -> UriManager.string_of_uri u
-  | _ -> "not_of_constant"
-;;
-
-(* coq wrapper 
-let string_of_constr = string_of_term
-;;
-*)
-
 (**
        @param t a term
        @raise Failure if conversion is impossible
@@ -491,143 +474,86 @@ i.e. on obtient une contradiction.
 *)
 
 
-let _eqT =
- Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [];;
-let _False =
- Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [];;
-let _not =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") [];;
-let _R0 =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") [];;
-let _R1 =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con") [];;
-let _R =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R.con") [];;
-let _Rfourier_eqLR_to_le=
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [];;
-let _Rfourier_eqRL_to_le =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [];;
-let _Rfourier_ge_to_le =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [];;
-let _Rfourier_gt_to_lt =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [];;
-let _Rfourier_le =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le.con")[];;
-let _Rfourier_le_le =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con")
-  [];;
-let _Rfourier_le_lt =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con")
-  [] ;;
-let _Rfourier_lt =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") []
-;;
-let _Rfourier_lt_le =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con")
-  []
-;;
-let _Rfourier_lt_lt =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con")
-  []
-;;
-let _Rfourier_not_ge_lt =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [];;
-let _Rfourier_not_gt_le =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [];;
-let _Rfourier_not_le_gt =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [];;
-let _Rfourier_not_lt_ge =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [];;
-let _Rinv =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con")[];;
-let _Rinv_R1 =
- Cic.Const(UriManager.uri_of_string "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [];;
-let _Rle =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rle.con") [];;
-let _Rle_mult_inv_pos =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [];;
-let _Rle_not_lt =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [];;
-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 _Rlt =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rlt.con") [];;
-let _Rlt_mult_inv_pos =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [];;
-let _Rlt_not_le =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [];;
-let _Rlt_zero_1 =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [];;
-let _Rlt_zero_pos_plus1 =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [];;
-let _Rminus =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rminus.con")
-  []
-;;
-let _Rmult =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con")
-  []
-;;
-let _Rnot_le_le =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [];;
-let _Rnot_lt0 =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [];;
-let _Rnot_lt_lt =
- Cic.Const
-  (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [];;
-let _Ropp =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.con") []
-;;
-let _Rplus =
- Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") []
-;;
-let _sym_eqT =
- Cic.Const
-  (UriManager.uri_of_string
-    "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") [];;
+let _eqT = Cic.MutInd(UriManager.uri_of_string 
+ "cic:/Coq/Init/Logic_Type/eqT.ind") 0 [] ;;
+let _False = Cic.MutInd (UriManager.uri_of_string 
+ "cic:/Coq/Init/Logic/False.ind") 0 [] ;;
+let _not = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Init/Logic/not.con") [];;
+let _R0 = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/R0.con") [] ;;
+let _R1 = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/R1.con") [] ;;
+let _R = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/R.con") [] ;;
+let _Rfourier_eqLR_to_le=Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqLR_to_le.con") [] ;;
+let _Rfourier_eqRL_to_le=Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_eqRL_to_le.con") [] ;;
+let _Rfourier_ge_to_le  =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_ge_to_le.con") [] ;;
+let _Rfourier_gt_to_lt         =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_gt_to_lt.con") [] ;;
+let _Rfourier_le=Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le.con") [] ;;
+let _Rfourier_le_le =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le_le.con") [] ;;
+let _Rfourier_le_lt =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_le_lt.con") [] ;;
+let _Rfourier_lt=Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt.con") [] ;;
+let _Rfourier_lt_le =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt_le.con") [] ;;
+let _Rfourier_lt_lt =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_lt_lt.con") [] ;;
+let _Rfourier_not_ge_lt = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_ge_lt.con") [] ;;
+let _Rfourier_not_gt_le = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_gt_le.con") [] ;;
+let _Rfourier_not_le_gt = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_le_gt.con") [] ;;
+let _Rfourier_not_lt_ge = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rfourier_not_lt_ge.con") [] ;;
+let _Rinv  = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rinv.con") [] ;;
+let _Rinv_R1 = Cic.Const(UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rbase/Rinv_R1.con" ) [] ;;
+let _Rle = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rle.con") [] ;;
+let _Rle_mult_inv_pos =  Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rle_mult_inv_pos.con") [] ;;
+let _Rle_not_lt = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rle_not_lt.con") [] ;;
+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 _Rlt = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con") [] ;;
+let _Rlt_mult_inv_pos = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rlt_mult_inv_pos.con") [] ;;
+let _Rlt_not_le =  Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rlt_not_le.con") [] ;;
+let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.con") [] ;;
+let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") [] ;;
+let _Rminus = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rminus.con") [] ;;
+let _Rmult = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rmult.con") [] ;;
+let _Rnot_le_le =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rnot_le_le.con") [] ;;
+let _Rnot_lt0 = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt0.con") [] ;;
+let _Rnot_lt_lt =Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/fourier/Fourier_util/Rnot_lt_lt.con") [] ;;
+let _Ropp = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Ropp.con") [] ;;
+let _Rplus = Cic.Const (UriManager.uri_of_string 
+ "cic:/Coq/Reals/Rdefinitions/Rplus.con") [] ;;
 
 (******************************************************************************)
 
@@ -768,16 +694,43 @@ let tac_zero_inf_false gl (n,d) ~status=
      )
 ;;
 
-(* preuve que 0<=(-n)*(1/d) => False 
+(* preuve que 0<=n*(1/d) => False ; n est negatif
 *)
 
-let tac_zero_infeq_false gl (n,d) ~status=
-debug("stat tac_zero_infeq_false");
+let tac_zero_infeq_false gl (n,d) ~status:(proof,goal as status)=
+debug("stat tac_zero_infeq_false\n");
 let r = 
-     (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
+     let curi,metasenv,pbo,pty = proof in
+     let metano,context,ty =List.find (function (m,_,_) -> m=goal) metasenv in
+     
+     debug("faccio fold di " ^ CicPp.ppterm
+            (Cic.Appl
+              [_Rle ; _R0 ;
+               Cic.Appl
+                [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+              ]
+            ) ^ "\n") ;
+     debug("apply di _Rlt_not_le a "^ CicPp.ppterm ty ^"\n");
+     (*CSC: Patch to undo the over-simplification of RewriteSimpl *)
+     Tacticals.then_
+      ~start:
+        (ReductionTactics.fold_tac
+          ~term:
+            (Cic.Appl
+              [_Rle ; _R0 ;
+               Cic.Appl
+                [_Rmult ; int_to_real n ; Cic.Appl [_Rinv ; int_to_real d]]
+              ]
+            )
+        )
+      ~continuation:
+        (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+         ~continuation:(tac_zero_inf_pos (-n,d))) ~status in
+ debug("end tac_zero_infeq_false\n");
+ r
+(*PORTING
+ Tacticals.id_tac ~status
+*)
 ;;
 
 
@@ -1214,6 +1167,7 @@ theoreme,so let's parse our thesis *)
    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) ->
@@ -1236,9 +1190,27 @@ theoreme,so let's parse our thesis *)
                                        r)
                        ; "id", Tacticals.id_tac] 
                 ])
-(* CSC: NOW THE BUG IS HERE: tac2 DOES NOT WORK ANY MORE *)
-              ;tac2]))
-        ;!tac1]);(*end 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) 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.Anonymous,a,b) -> (Cic.Appl [_not;a])
+                    |_ -> assert false)
+                  in
+                  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:=*)
        tac:=(Tacticals.thens 
          ~start:(PrimitiveTactics.cut_tac ~term:_False)
         ~continuations:[Tacticals.then_