*)
+(******************** OTHER USEFUL TACTICS **********************)
+
+let rewrite_tac ~term:equality ~status:(proof,goal) =
+ let module C = Cic in
+ 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 =
+ 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") ->
+ let eq_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
+ in
+ eq_ind_r,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
+ (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
+ in
+ eqT_ind_r,ty,t1,t2
+ | _ ->
+ raise
+ (ProofEngineTypes.Fail
+ "Rewrite: the argument is not a proof of an equality")
+ in
+ let pred =
+ let gty' = CicSubstitution.lift 1 gty in
+ let t1' = CicSubstitution.lift 1 t1 in
+ let gty'' =
+ ProofEngineReduction.replace_lifting
+ ~equality:
+ (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
+ ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+ in
+ C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+ in
+prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+ PrimitiveTactics.exact_tac
+ (C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ((curi,metasenv',pbo,pty),goal)
+;;
+
+(******************** THE FOURIER TACTIC ***********************)
(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
des inéquations et équations sont entiers. En attendant la tactique Field.
i.e. on obtient une contradiction.
*)
+
+let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 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_mult_inv_pos = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/_Rlt_mult_inv_pos.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.MutConstruct(UriManager.uri_of_string "cic:/Coq/Init/Datatypes/bool.ind") 0 1 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
;;
let rec int_to_real_aux n =
match n with
0 -> _R0 (* o forse R0 + R0 ????? *)
+ | 1 -> _R1
| _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
;;
(* 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
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("TAC ZERO INF POS\n");
+(Tacticals.thens ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_mult_inv_pos)
+ ~continuations:[
+ !tacn ;
+ !tacd ]
+ ~status)
+;;
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)))
;;
(* *********** ********** ******** ??????????????? *********** **************)
-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
;;
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
;;
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:(proof,goal as status) =
+debug("Inizio TC_USE\n");
+let curi,metasenv,pbo,pty = proof in
+let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+debug ("hname = "^ CicPp.ppterm h.hname ^"\n");
+debug ("ty = "^ CicPp.ppterm ty^"\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\n");
+res
;;
;;
-(* fix !!!!!!!!!! this may not work *)
-let equality_replace a b =
- 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])
+let equality_replace a b ~status =
+ let module C = Cic in
+ let proof,goal = status in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+ let (proof,goals) =
+ rewrite_tac ~term:(C.Meta (fresh_meta,irl))
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ (proof,fresh_meta::goals)
;;
let tcl_fail a ~status:(proof,goal) =
let assumption_tac ~status:(proof,goal)=
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let num = ref (-1) in
+ let num = ref 0 in
let tac_list = List.map
( fun x -> num := !num + 1;
match x with
(* ********************* TATTICA ******************************** *)
-let rec fourier ~status:(proof,goal)=
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+let rec fourier ~status:(s_proof,s_goal)=
+ let s_curi,s_metasenv,s_pbo,s_pty = s_proof in
+ let s_metano,s_context,s_ty = List.find (function (m,_,_) -> m=s_goal) s_metasenv in
- debug ("invoco fourier_tac sul goal "^string_of_int(goal)^" e contesto :\n");
- debug_pcontext context;
+ debug ("invoco fourier_tac sul goal "^string_of_int(s_goal)^" e contesto :\n");
+ debug_pcontext s_context;
- (* il goal di prima dovrebbe essere ty
-
- let goal = strip_outer_cast (pf_concl gl) in *)
-
let fhyp = String.copy "new_hyp_for_fourier" in
- (* si le but est une inéquation, on introduit son contraire,
- et le but à prouver devient False *)
-
- try (let tac =
- match ty with
- Cic.Appl ( Cic.Const(u,boh)::args) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_ge_lt)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_gt_le)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_le_gt)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
- (Tacticals.then_
- ~start:(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_not_lt_ge)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp))
- ~continuation:fourier)
- |_->assert false)
- |_->assert false
- in tac (proof,goal) )
- with _ ->
-
- (* les hypothèses *)
+
+ (* here we need to negate the thesis, but to do this we nned to apply the right theoreme,
+ so let's parse our thesis *)
+
+ let th_to_appl = ref _Rfourier_not_le_gt in
+ (match s_ty with
+ Cic.Appl ( Cic.Const(u,boh)::args) ->
+ (match UriManager.string_of_uri u with
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> th_to_appl := _Rfourier_not_ge_lt
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> th_to_appl := _Rfourier_not_gt_le
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> th_to_appl := _Rfourier_not_le_gt
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> th_to_appl := _Rfourier_not_lt_ge
+ |_-> failwith "fourier can't be applyed")
+ |_-> failwith "fourier can't be applyed"); (* fix maybe strip_outer_cast goes here?? *)
+
+ (* now let's change our thesis applying the th and put it with hp *)
+
+ let proof,gl = Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+ ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
+ ~status:(s_proof,s_goal) in
+ let goal = if List.length gl = 1 then List.hd gl else failwith "a new goal" in
+
+ debug ("port la tesi sopra e la nego. contesto :\n");
+ debug_pcontext s_context;
+
+ (* now we have all the right environment *)
+
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+
+ (* now we want to convert hp to inequations, but first we must lift
+ everyting to thesis level, so that a variable has the save Rel(n)
+ in each hp ( needed by ineq1_of_term ) *)
(* ? fix if None ?????*)
- let new_context = superlift context 1 in
- let hyps = filter_real_hyp new_context new_context in
+ (* fix change superlift with a real name *)
+
+ let l_context = superlift context 1 in
+ let hyps = filter_real_hyp l_context l_context in
+
debug ("trasformo in diseq. "^ string_of_int (List.length hyps)^" ipotesi\n");
+
let lineq =ref [] in
+
+ (* transform hyps into inequations *)
+
List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
with _-> ())
hyps;
- (* lineq = les inéquations découlant des hypothèses *)
-
debug ("applico fourier a "^ string_of_int (List.length !lineq)^" disequazioni\n");
let res=fourier_lineq (!lineq) in
let tac=ref Ring.id_tac in
- if res=[] then (print_string "Tactic Fourier fails.\n";flush stdout)
- (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
- else (
-
+ if res=[] then
+ (print_string "Tactic Fourier fails.\n";flush stdout;failwith "fourier_tac fails")
+ else
+ (
match res with (*match res*)
[(cres,sres,lc)]->
- (* lc=coefficients multiplicateurs des inéquations
- qui donnent 0<cres ou 0<=cres selon sres *)
-
+
+ (* in lc we have the coefficient to "reduce" the system *)
print_string "Fourier's method can prove the goal...\n";flush stdout;
+ debug "I coeff di moltiplicazione rit sono: ";
let lutil=ref [] in
- debug "I coeff di moltiplicazione rit sono: ";
List.iter
(fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
- Fourier.print_rational(c);print_string " ")
+ (* DBG *)Fourier.print_rational(c);print_string " "(* DBG *))
)
(List.combine (!lineq) lc);
+
print_string (" quindi lutil e' lunga "^string_of_int (List.length (!lutil))^"\n");
- (* on construit la combinaison linéaire des inéquation *)
-
-
+
+ (* on construit la combinaison linéaire des inéquation *)
+
(match (!lutil) with (*match (!lutil) *)
(h1,c1)::lutil ->
- debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
+
+ debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
+
let s=ref (h1.hstrict) in
+
(* let t1=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hleft|]) in
- let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in*)
- let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
+ let t2=ref (mkAppL [|parse "Rmult";parse (rational_to_real c1);h1.hright|]) in
+ *)
+
+ let t1 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hleft] ) in
let t2 = ref (Cic.Appl [_Rmult;rational_to_real c1;h1.hright]) in
List.iter (fun (h,c) ->
let tc=rational_to_real cres in
- (* puis sa preuve *)
+ (* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
+
debug "inizio a costruire tac1\n";
- let tac1=ref ( 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)])
+ Fourier.print_rational(c1);
+
+ let tac1=ref ( fun ~status ->
+ debug ("Sotto tattica t1 "^(if h1.hstrict then "strict" else "lasc")^"\n");
+ if h1.hstrict then
+ (Tacticals.thens ~start:(
+ fun ~status ->
+ debug ("inizio t1 strict\n");
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ debug ("th = "^ CicPp.ppterm _Rfourier_lt ^"\n");
+ debug ("ty = "^ CicPp.ppterm ty^"\n");
+
+ PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
+ ~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)
+ ~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
- tac1:=(Tacticals.thens ~start:(PrimitiveTactics.apply_tac
- ~term:_Rfourier_lt_le)
+ (
+ debug("tac1 2\n");
+ Fourier.print_rational(c1);
+ tac1:=(Tacticals.thens ~start:(
+ fun ~status ->
+ debug("INIZIO TAC 1 2\n");
+
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ debug ("th = "^ CicPp.ppterm _Rfourier_lt_le ^"\n");
+ debug ("ty = "^ CicPp.ppterm ty^"\n");
+
+ PrimitiveTactics.apply_tac ~term:_Rfourier_lt_le ~status
+
+ )
~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*)
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))
|_-> assert false)(*match (!lutil) *)
|_-> assert false); (*match res*)
- debug ("finalmente applico t1\n");
+ debug ("finalmente applico tac\n");
(!tac ~status:(proof,goal))
;;
let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
-
projects / helm.git / blobdiff