*)
+(******************** 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
+
+ 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") ->
+ 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
+
+ let (proof',goals) =
+ PrimitiveTactics.exact_tac
+ ~term:(C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ assert (List.length goals = 0) ;
+ (proof',[fresh_meta])
+;;
+
+(* ti ho beccato !!!!!!!!!! qui' salta fuori un or. perche'?*)
+
+
+
+let simpl_tac ~status:(proof,goal) =
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+prerr_endline("simpl_tac su "^CicPp.ppterm ty);
+
+ let new_ty = ProofEngineReduction.simpl context ty in
+
+prerr_endline("ritorna "^CicPp.ppterm new_ty);
+
+ let new_metasenv =
+ List.map
+ (function
+ (n,_,_) when n = metano -> (metano,context,new_ty)
+ | _ as t -> t
+ ) metasenv
+ in
+ (curi,new_metasenv,pbo,pty), [metano]
+
+;;
+
+let rewrite_simpl_tac ~term ~status =
+
+ Tacticals.then_ ~start:(rewrite_tac ~term) ~continuation:simpl_tac ~status
+
+;;
+
+(******************** 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.
*)
-(*open Term // in coq/kernel
-open Tactics
-open Clenv
-open Names
-open Tacmach*)
open Fourier
+
+let debug x = print_string ("____ "^x) ; flush stdout;;
+
+let debug_pcontext x =
+ let str = ref "" in
+ List.iter (fun y -> match y with Some(Cic.Name(a),_) -> str := !str ^
+ a ^ " " | _ ->()) x ;
+ debug ("contesto : "^ (!str) ^ "\n")
+;;
+
(******************************************************************************
Operations on linear combinations.
_ -> (flin_add (flin_zero()) arg2 a)
end
with
- _-> (flin_add (flin_zero()) arg1 (rational_of_term arg2 ))
+ _-> (flin_add(flin_zero()) arg1 (rational_of_term arg2))
end
|"cic:/Coq/Reals/Rdefinitions/Rinv.con"->
let a=(rational_of_term (List.hd next)) in
*)
let ineq1_of_term (h,t) =
- match t with
+ debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
+ match t with (* match t *)
Cic.Appl (t1::next) ->
let arg1= List.hd next in
let arg2= List.hd(List.tl next) in
- (match t1 with
+ (match t1 with (* match t1 *)
Cic.Const (u,boh) ->
- (match UriManager.string_of_uri u with
- "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> [{hname=h;
+ (match UriManager.string_of_uri u with (* match u *)
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" ->
+ [{hname=h;
htype="Rlt";
hleft=arg1;
hright=arg2;
hflin= flin_minus (flin_of_term arg1)
(flin_of_term arg2);
hstrict=true}]
- |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
+ [{hname=h;
htype="Rgt";
hleft=arg2;
hright=arg1;
hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
hstrict=true}]
- |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
+ [{hname=h;
htype="Rle";
hleft=arg1;
hright=arg2;
hflin= flin_minus (flin_of_term arg1)
(flin_of_term arg2);
hstrict=false}]
- |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> [{hname=h;
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
+ [{hname=h;
htype="Rge";
hleft=arg2;
hright=arg1;
hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
hstrict=false}]
- |_->assert false)
+ |_->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;
hflin= flin_minus (flin_of_term arg2)
(flin_of_term arg1);
hstrict=false}]
- |_-> assert false)
- |_-> assert false)
- |_-> assert false)
- |_-> assert false)
- |_-> assert false
+ |_-> 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;;
(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
*)
+let rec print_rl l =
+ match l with
+ []-> ()
+ | a::next -> Fourier.print_rational a ; print_string " " ; print_rl next
+;;
+
+let rec print_sys l =
+ match l with
+ [] -> ()
+ | (a,b)::next -> (print_rl a;
+ print_string (if b=true then "strict\n"else"\n");
+ print_sys next)
+ ;;
+
+(*let print_hash h =
+ Hashtbl.iter (fun x y -> print_string ("("^"-"^","^"-"^")")) h
+;;*)
+
let fourier_lineq lineq1 =
let nvar=ref (-1) in
let hvar=Hashtbl.create 50 in (* la table des variables des inéquations *)
Hashtbl.add hvar x (!nvar))
f.hflin.fhom)
lineq1;
+ (*print_hash hvar;*)
+ debug("Il numero di incognite e' "^string_of_int (!nvar+1)^"\n");
let sys= List.map (fun h->
let v=Array.create ((!nvar)+1) r0 in
Hashtbl.iter (fun x c -> v.(Hashtbl.find hvar x)<-c)
h.hflin.fhom;
((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
lineq1 in
+ debug ("chiamo unsolvable sul sistema di "^
+ string_of_int (List.length sys) ^"\n");
+ print_sys sys;
unsolvable sys
;;
-(******************************************************************************
+(*****************************************************************************
Construction de la preuve en cas de succès de la méthode de Fourier,
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 = 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 _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 _sym_eqT = Cic.Const(UriManager.uri_of_string
+ "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con") 0 ;;
+
+(******************************************************************************)
+
let is_int x = (x.den)=1
;;
(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
*)
-(*et int_to_real n =
- let nn=abs n in
- let s=ref Cic.term
- if nn=0
- then s:="R0"
- else (s:="R1";
- for i=1 to (nn-1) do s:="(Rplus R1 "^(!s)^")"; done;);
- if n<0 then s:="(Ropp "^(!s)^")";
- !s
-;;*)
-let _Ropp = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Ropp.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 _Rplus = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con") 0 ;;
-
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) ]
;;
(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
*)
-let _Rmult = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rmult.con") 0 ;;
-let _Rinv = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rinv.con") 0 ;;
-
let rational_to_real x =
let (n,d)=rational_to_fraction x in
(* preuve que 0<n*1/d
*)
-let _Rlt_zero_pos_plus1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_pos_plus1.con") 0 ;;
-
-let _Rlt_zero_1 = Cic.Const (UriManager.uri_of_string "cic:/Coq/fourier/Fourier_util/Rlt_zero_1.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 tac_zero_inf_pos gl (n,d) =
+let tac_zero_inf_pos (n,d) ~status =
(*let cste = pf_parse_constr gl in*)
- let tacn=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
- let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
- for i=1 to n-1 do
- tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_zero_pos_plus1) ~continuation:!tacn); done;
- 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 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)
;;
+
+
(* preuve que 0<=n*1/d
*)
-(*let tac_zero_infeq_pos gl (n,d)=
- let cste = pf_parse_constr gl in
- let tacn=ref (if n=0
- then (apply (cste "Rle_zero_zero"))
- else (apply (cste "Rle_zero_1"))) in
- let tacd=ref (apply (cste "Rlt_zero_1")) in
- for i=1 to n-1 do
- tacn:=(tclTHEN (apply (cste "Rle_zero_pos_plus1")) !tacn); done;
- for i=1 to d-1 do
- tacd:=(tclTHEN (apply (cste "Rlt_zero_pos_plus1")) !tacd); done;
- (tclTHENS (apply (cste "Rle_mult_inv_pos")) [!tacn;!tacd])
-;;*)
-
+
+let tac_zero_infeq_pos gl (n,d) ~status =
+ (*let cste = pf_parse_constr gl in*)
+ debug("inizio tac_zero_infeq_pos\n");
+ let tacn = ref
+ (if n=0 then
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_zero )
+ else
+ (PrimitiveTactics.apply_tac ~term:_Rle_zero_1 )
+ )
+ in
+ let tacd=ref (PrimitiveTactics.apply_tac ~term:_Rlt_zero_1 ) in
+ for i=1 to n-1 do
+ tacn:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rle_zero_pos_plus1) ~continuation:!tacn);
+ done;
+ for i=1 to d-1 do
+ tacd:=(Tacticals.then_ ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rlt_zero_pos_plus1) ~continuation:!tacd);
+ done;
+ let r =
+ (Tacticals.thens ~start:(PrimitiveTactics.apply_tac
+ ~term:_Rle_mult_inv_pos) ~continuations:[!tacn;!tacd]) ~status in
+ debug("fine tac_zero_infeq_pos\n");
+ r
+;;
+
+
+
(* preuve que 0<(-n)*(1/d) => False
*)
-(*let tac_zero_inf_false gl (n,d) =
- let cste = pf_parse_constr gl in
- if n=0 then (apply (cste "Rnot_lt0"))
+
+let tac_zero_inf_false gl (n,d) ~status=
+ debug("inizio tac_zero_inf_false\n");
+ if n=0 then
+ (debug "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
+ debug("fine\n");
+ r)
else
- (tclTHEN (apply (cste "Rle_not_lt"))
- (tac_zero_infeq_pos gl (-n,d)))
-;;*)
+ (debug "2\n";let r = (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
+ debug("!!!!!!!!1:unify "^CicPp.ppterm _Rle_not_lt^" with "
+ ^ CicPp.ppterm ty ^" fails\n");
+ let r = PrimitiveTactics.apply_tac ~term:_Rle_not_lt ~status in
+ debug("!!!!!!!!!2\n");
+ r
+ )
+ ~continuation:(tac_zero_infeq_pos gl (-n,d))) ~status in
+ debug("fine\n");
+ r
+ )
+;;
(* preuve que 0<=(-n)*(1/d) => False
*)
-(*let tac_zero_infeq_false gl (n,d) =
- let cste = pf_parse_constr gl in
- (tclTHEN (apply (cste "Rlt_not_le"))
- (tac_zero_inf_pos gl (-n,d)))
+
+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("end tac_zero_infeq_false\n");
+ r*)
+ Ring.id_tac ~status
+;;
+
+
+(* *********** ********** ******** ??????????????? *********** **************)
+
+let apply_type_tac ~cast:t ~applist: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 create_meta () = mkMeta(new_meta());;
+
+
+
-let my_cut c gl=
- let concl = pf_concl gl in
- apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl
-;;
-let exact = exact_check;;
-
-let tac_use h = match h.htype with
- "Rlt" -> exact h.hname
- |"Rle" -> exact h.hname
- |"Rgt" -> (tclTHEN (apply (parse "Rfourier_gt_to_lt"))
- (exact h.hname))
- |"Rge" -> (tclTHEN (apply (parse "Rfourier_ge_to_le"))
- (exact h.hname))
- |"eqTLR" -> (tclTHEN (apply (parse "Rfourier_eqLR_to_le"))
- (exact h.hname))
- |"eqTRL" -> (tclTHEN (apply (parse "Rfourier_eqRL_to_le"))
- (exact h.hname))
- |_->assert false
+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
+
+ 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 ~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
+;;
+
+
+
let is_ineq (h,t) =
- match (kind_of_term t) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" -> true
- |"Coq.Reals.Rdefinitions.Rgt" -> true
- |"Coq.Reals.Rdefinitions.Rle" -> true
- |"Coq.Reals.Rdefinitions.Rge" -> true
- |"Coq.Init.Logic_Type.eqT" -> (match (string_of_constr args.(0)) with
- "Coq.Reals.Rdefinitions.R"->true
- |_->false)
+ match t with
+ Cic.Appl ( Cic.Const(u,boh)::next) ->
+ (match (UriManager.string_of_uri u) with
+ "cic:/Coq/Reals/Rdefinitions/Rlt.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rgt.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rle.con" -> true
+ |"cic:/Coq/Reals/Rdefinitions/Rge.con" -> true
+ |"cic:/Coq/Init/Logic_Type/eqT.con" ->
+ (match (List.hd next) with
+ Cic.Const (uri,_) when
+ UriManager.string_of_uri uri =
+ "cic:/Coq/Reals/Rdefinitions/R.con" -> true
+ | _ -> false)
|_->false)
|_->false
;;
let list_of_sign s = List.map (fun (x,_,z)->(x,z)) s;;
let mkAppL a =
- let l = Array.to_list a in
- mkApp(List.hd l, Array.of_list (List.tl l))
-;;*)
+ Cic.Appl(Array.to_list a)
+;;
(* Résolution d'inéquations linéaires dans R *)
+let rec strip_outer_cast c = match c with
+ | Cic.Cast (c,_) -> strip_outer_cast c
+ | _ -> c
+;;
-(*
-let rec fourier gl=
- let parse = pf_parse_constr gl in
- let goal = strip_outer_cast (pf_concl gl) in
- let fhyp=id_of_string "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 (kind_of_term goal) with
- App (f,args) ->
- (match (string_of_constr f) with
- "Coq.Reals.Rdefinitions.Rlt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_ge_lt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rle" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_gt_le"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rgt" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_le_gt"))
- (intro_using fhyp))
- fourier)
- |"Coq.Reals.Rdefinitions.Rge" ->
- (tclTHEN
- (tclTHEN (apply (parse "Rfourier_not_lt_ge"))
- (intro_using fhyp))
- fourier)
- |_->assert false)
- |_->assert false
- in tac gl)
- with _ ->
-*)
- (* les hypothèses *)
-
-(*
- let hyps = List.map (fun (h,t)-> (mkVar h,(body_of_type t)))
- (list_of_sign (pf_hyps gl)) in
- let lineq =ref [] in
- List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
- with _-> ())
- hyps;
-*)
-
- (* lineq = les inéquations découlant des hypothèses *)
+let find_in_context id context =
+ let rec find_in_context_aux c n =
+ match c with
+ [] -> failwith (id^" not found in context")
+ | a::next -> (match a with
+ Some (Cic.Name(name),_) when name = id -> n
+ (*? magari al posto di _ qualcosaltro?*)
+ | _ -> find_in_context_aux next (n+1))
+ in
+ find_in_context_aux context 1
+;;
+(* mi sembra quadratico *)
+let rec filter_real_hyp context cont =
+ match context with
+ [] -> []
+ | Some(Cic.Name(h),Cic.Decl(t))::next -> (
+ let n = find_in_context h cont in
+ [(Cic.Rel(n),t)] @ filter_real_hyp next cont)
+ | a::next -> debug(" no\n"); filter_real_hyp next cont
+;;
-(*
- let res=fourier_lineq (!lineq) in
- let tac=ref tclIDTAC in
- if res=[]
- then (print_string "Tactic Fourier fails.\n";
- flush stdout)
+(* lifts everithing at the conclusion level *)
+let rec superlift c n=
+ match c with
+ [] -> []
+ | Some(name,Cic.Decl(a))::next -> [Some(name,Cic.Decl(
+ CicSubstitution.lift n a))] @ superlift next (n+1)
+ | Some(name,Cic.Def(a))::next -> [Some(name,Cic.Def(
+ CicSubstitution.lift n a))] @ superlift next (n+1)
+ | _::next -> superlift next (n+1) (*?? ??*)
+
+;;
-*)
- (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
+let equality_replace a b ~status =
+debug("inizio EQ\n");
+ 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
+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)
+ in
+ let new_goals = fresh_meta::goals in
+debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
+ ^string_of_int( List.length goals)^"+ meta\n");
+ (proof,new_goals)
+;;
-(*
- else (match res with
- [(cres,sres,lc)]->
-*)
- (* lc=coefficients multiplicateurs des inéquations
- qui donnent 0<cres ou 0<=cres selon sres *)
- (*print_string "Fourier's method can prove the goal...";flush stdout;*)
-
-
-(*
- let lutil=ref [] in
- List.iter
- (fun (h,c) ->
- if c<>r0
- then (lutil:=(h,c)::(!lutil)(*;
- print_rational(c);print_string " "*)))
- (List.combine (!lineq) lc);
-
-*)
- (* on construit la combinaison linéaire des inéquation *)
-
-(*
- (match (!lutil) with
- (h1,c1)::lutil ->
- 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
- List.iter (fun (h,c) ->
+let tcl_fail a ~status:(proof,goal) =
+ match a with
+ 1 -> raise (ProofEngineTypes.Fail "fail-tactical")
+ |_-> (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 0 in
+ let tac_list = List.map
+ ( fun x -> num := !num + 1;
+ match x with
+ Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
+ | _ -> ("fake",tcl_fail 1)
+ )
+ context
+ in
+ Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
+;;
+
+(* !!!!! fix !!!!!!!!!! *)
+let contradiction_tac ~status:(proof,goal)=
+ Tacticals.then_
+ ~start:(PrimitiveTactics.intros_tac ~name:"bo?" )
+ ~continuation:(Tacticals.then_
+ ~start:(Ring.elim_type_tac ~term:_False)
+ ~continuation:(assumption_tac))
+ ~status:(proof,goal)
+;;
+
+(* ********************* TATTICA ******************************** *)
+
+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(s_goal)^" e contesto :\n");
+ debug_pcontext s_context;
+
+ let fhyp = String.copy "new_hyp_for_fourier" in
+
+(* here we need to negate the thesis, but to do this we need 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 ?????*)
+ (* 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 _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
+ hyps;
+
+
+ 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;
+ failwith "fourier can't proove it")
+ else
+ (
+ match res with (*match res*)
+ [(cres,sres,lc)]->
+
+ (* 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
+ List.iter
+ (fun (h,c) -> if c<>r0 then (lutil:=(h,c)::(!lutil);
+ (* 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 *)
+
+ (match (!lutil) with (*match (!lutil) *)
+ (h1,c1)::lutil ->
+ debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
+
+ let s=ref (h1.hstrict) 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) ->
s:=(!s)||(h.hstrict);
- t1:=(mkAppL [|parse "Rplus";
- !t1;
- mkAppL [|parse "Rmult";
- parse (rational_to_real c);
- h.hleft|] |]);
- t2:=(mkAppL [|parse "Rplus";
- !t2;
- mkAppL [|parse "Rmult";
- parse (rational_to_real c);
- h.hright|] |]))
+ t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
+ [_Rmult;rational_to_real c;h.hleft ] ]);
+ t2:=(Cic.Appl [_Rplus;!t2;Cic.Appl
+ [_Rmult;rational_to_real c;h.hright] ]))
lutil;
- let ineq=mkAppL [|parse (if (!s) then "Rlt" else "Rle");
- !t1;
- !t2 |] in
- let tc=parse (rational_to_real cres) in
-*)
- (* puis sa preuve *)
-(*
- let tac1=ref (if h1.hstrict
- then (tclTHENS (apply (parse "Rfourier_lt"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])
- else (tclTHENS (apply (parse "Rfourier_le"))
- [tac_use h1;
- tac_zero_inf_pos gl
- (rational_to_fraction c1)])) in
- s:=h1.hstrict;
- List.iter (fun (h,c)->
- (if (!s)
- then (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_lt_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_lt_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)]))
- else (if h.hstrict
- then tac1:=(tclTHENS (apply (parse "Rfourier_le_lt"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (parse "Rfourier_le_le"))
- [!tac1;tac_use h;
- tac_zero_inf_pos gl
- (rational_to_fraction c)])));
- s:=(!s)||(h.hstrict))
- lutil;
- let tac2= if sres
- then tac_zero_inf_false gl (rational_to_fraction cres)
- else tac_zero_infeq_false gl (rational_to_fraction cres)
- in
- tac:=(tclTHENS (my_cut ineq)
- [tclTHEN (change_in_concl
- (mkAppL [| parse "not"; ineq|]
- ))
- (tclTHEN (apply (if sres then parse "Rnot_lt_lt"
- else parse "Rnot_le_le"))
- (tclTHENS (Equality.replace
- (mkAppL [|parse "Rminus";!t2;!t1|]
- )
- tc)
- [tac2;
- (tclTHENS (Equality.replace (parse "(Rinv R1)")
- (parse "R1"))
-*)
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
-(*
- [tclORELSE
- (Ring.polynom [])
- tclIDTAC;
- (tclTHEN (apply (parse "sym_eqT"))
- (apply (parse "Rinv_R1")))]
-
- )
- ]));
- !tac1]);
- tac:=(tclTHENS (cut (parse "False"))
- [tclTHEN intro contradiction;
- !tac])
- |_-> assert false) |_-> assert false
- );
- ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *) )) gl)
- (!tac gl)
- ((tclABSTRACT None !tac) gl)
-
-;;
-
-let fourier_tac x gl =
- fourier gl
-;;
-
-let v_fourier = add_tactic "Fourier" fourier_tac
+
+ let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
+ let tc=rational_to_real cres in
+
+
+(* ora ho i termini che descrivono i passi di fourier per risolvere il sistema *)
+
+ debug "inizio a costruire tac1\n";
+ Fourier.print_rational(c1);
+
+ let tac1=ref ( fun ~status ->
+ 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
+ (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
+ (rational_to_fraction c)])
+ )
+ else
+ (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
+ (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
+ (rational_to_fraction c)])
+ )
+ else
+ (debug("tac1 4\n");
+ tac1:=(Tacticals.thens
+ ~start:(PrimitiveTactics.apply_tac ~term:_Rfourier_le_le)
+ ~continuations:[!tac1;tac_use h;tac_zero_inf_pos
+ (rational_to_fraction c)])
+ )
+ )
+ );
+ s:=(!s)||(h.hstrict)) lutil;(*end List.iter*)
+
+ let tac2 =
+ if sres then
+ tac_zero_inf_false goal (rational_to_fraction cres)
+ else
+ tac_zero_infeq_false goal (rational_to_fraction cres)
+ in
+ tac:=(Tacticals.thens
+ ~start:(my_cut ~term:ineq)
+ ~continuations:[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
+
+ debug("Change_tac "^CicPp.ppterm ty^" with "^CicPp.ppterm (Cic.Appl [ _not; ineq]) ^"\n");
+
+ 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:(Tacticals.thens
+ ~start:(
+ fun ~status ->
+ let r = equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc
+ ~status
+ in
+ (match r with (p,gl) ->
+ debug("eq1 ritorna "^string_of_int(List.length gl)^"\n" ));
+ r)
+ ~continuations:[(Tacticals.thens
+ ~start:(
+ 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" ));
+ r)
+ ~continuations:
+ [PrimitiveTactics.apply_tac ~term:_Rinv_R1
+(* CSC: Il nostro goal e' 1^-1 = 1 e non 1 = 1^-1. Quindi non c'e' bisogno
+ 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?
+ ~continuations:[Tacticals.then_
+ ~start:(
+ fun ~status:(proof,goal as status) ->
+ debug("ECCOCI\n");
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=
+ goal) metasenv in
+ debug("ty = "^CicPp.ppterm ty^"\n");
+ let r = PrimitiveTactics.apply_tac ~term:_sym_eqT
+ ~status in
+ debug("fine ECCOCI\n");
+ r)
+ ~continuation:(PrimitiveTactics.apply_tac ~term:_Rinv_R1)
*)
+ ;Tacticals.try_tactics
+ ~tactics:[ "ring", (fun ~status ->
+ debug("begin RING\n");
+ let r = Ring.ring_tac ~status in
+ debug ("end RING\n");
+ r)
+ ; "id", Ring.id_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.Anonimous,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:Ring.id_tac(*tac2*)]))
+ ;Ring.id_tac(*!tac1*)]);(*end tac:=*)
+ tac:=(Tacticals.thens
+ ~start:(PrimitiveTactics.cut_tac ~term:_False)
+ ~continuations:[Tacticals.then_
+ ~start:(PrimitiveTactics.intros_tac ~name:"??")
+ ~continuation:contradiction_tac
+ ;!tac])
+
+
+ |_-> assert false)(*match (!lutil) *)
+ |_-> assert false); (*match res*)
+ debug ("finalmente applico tac\n");
+ (!tac ~status:(proof,goal))
+;;
+
+let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
-(*open CicReduction*)
-(*open PrimitiveTactics*)
-(*open ProofEngineTypes*)
-let fourier_tac ~status:(proof,goal) = (proof,[goal]) ;;
projects / helm.git / blobdiff