Several bug-fixes:

 - apply_tac and my_cut used to generate a new metavariable without
   updating the metasenv
 - a boolean "false" was used in place of the propositional "False"
 - minor fixes

The equality_replace tactic is completely wrong. For now the whole
proof branch that needs it is commented out.

Open bugs:
 Some unification problem in the proof that the linear combination can
 be derived from the initial disequations.

diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml
index 585513e59816445293d4c8ebc4cd6dfea76ead3b..446b2ef4b0ac92f95be24194ee6021fc5cb78f27 100644 (file)
--- a/helm/gTopLevel/fourierR.ml
+++ b/helm/gTopLevel/fourierR.ml
@@ -428,6 +428,7 @@ 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 _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 _Rinv  = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
@@ -436,7 +437,7 @@ let _Rle_not_lt = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_
 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_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.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 ;;
@@ -470,7 +471,7 @@ let _sym_eqT = Cic.Const(UriManager.uri_of_string "/Coq/Init/Logic_Type/Equality
 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.MutConstruct(UriManager.uri_of_string "cic:/Coq/Init/Datatypes/bool.ind") 0 1 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;;
 
@@ -575,16 +576,18 @@ let tac_zero_infeq_false gl (n,d) =
 
 (* *********** ********** ******** ??????????????? *********** **************)
 
-let mkMeta (proof,goal)  = 
-let curi,metasenv,pbo,pty = proof in
-let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-Cic.Meta (ProofEngineHelpers.new_meta proof) 
-         (ProofEngineHelpers.identity_relocation_list_for_metavariable context)
-;;
-
 let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) = 
-   let new_m = mkMeta (proof,goal) in
-   PrimitiveTactics.apply_tac ~term:(Cic.Appl ((Cic.Cast (new_m,t))::al)) ~status:(proof,goal)
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+  let fresh_meta = ProofEngineHelpers.new_meta proof in
+  let irl =
+   ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+  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)
+    in
+     proof'',fresh_meta::goals
 ;;
 
 
@@ -594,7 +597,19 @@ let apply_type_tac ~cast:t ~applist:al ~status:(proof,goal) =
 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
-  apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,ty)) ~applist:[mkMeta(proof,goal)] ~status:(proof,goal)
+
+  let fresh_meta = ProofEngineHelpers.new_meta proof in
+  let irl =
+   ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+  let metasenv' = (fresh_meta,context,c)::metasenv in
+   let proof' = curi,metasenv',pbo,pty in
+    let proof'',goals =
+     apply_type_tac ~cast:(Cic.Prod(Cic.Name "Anonymous",c,CicSubstitution.lift 1 ty)) ~applist:[Cic.Meta(fresh_meta,irl)] ~status:(proof',goal)
+    in
+     (* We permute the generated goals to be consistent with Coq *)
+     match goals with
+        [] -> assert false
+      | he::tl -> proof'',he::fresh_meta::tl
 ;;
 
 
@@ -679,9 +694,22 @@ let rec superlift c n=
 ;;
 
 (* fix !!!!!!!!!!  this may not work *)
-let equality_replace a b =
+let equality_replace a b ~status =
+  let proof,goal = status in
+  let curi,metasenv,pbo,pty = proof in
+  let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
+prerr_endline ("### IN MY_CUT: ") ;
+prerr_endline ("@ " ^ CicPp.ppterm ty) ;
+List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
+prerr_endline ("##- IN MY_CUT ") ;
+let res =
        let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
-       PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;a;b])
+(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
+       PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status
+in
+prerr_endline "EUREKA" ;
+res
 ;;
 
 let tcl_fail a ~status:(proof,goal) =
@@ -882,10 +910,15 @@ let rec fourier ~status:(s_proof,s_goal)=
            in
            tac:=(Tacticals.thens ~start:(my_cut ~term:ineq) 
                      ~continuations:[Tacticals.then_  (* ?????????????????????????????? *)
-                       ~start:(PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq] ))
+                       ~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
+                                  PrimitiveTactics.change_tac ~what:ty ~with_what:(Cic.Appl [ _not; ineq]) ~status)
                        ~continuation:(Tacticals.then_ 
                                ~start:(PrimitiveTactics.apply_tac 
                                                ~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
+                                ~continuation:Ring.id_tac
+(*CSC
                                ~continuation:(Tacticals.thens 
                                                ~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
                                                ~continuations:[tac2;(Tacticals.thens 
@@ -903,7 +936,7 @@ let rec fourier ~status:(s_proof,s_goal)=
                                
                                         )
                                                ] (* end continuations before comment *)
-                                       )
+                                       ) *)
                                );
                        !tac1]
                );(*end tac:=*)