(proof',[fresh_meta])
;;
+
+
+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
(flin_of_term arg2);
hstrict=true}]
|"cic:/Coq/Reals/Rdefinitions/Rgt.con" ->
- [{hname=h;
+ [{hname=h;
htype="Rgt";
hleft=arg2;
hright=arg1;
(flin_of_term arg1);
hstrict=true}]
|"cic:/Coq/Reals/Rdefinitions/Rle.con" ->
- [{hname=h;
+ [{hname=h;
htype="Rle";
hleft=arg1;
hright=arg2;
(flin_of_term arg2);
hstrict=false}]
|"cic:/Coq/Reals/Rdefinitions/Rge.con" ->
- [{hname=h;
+ [{hname=h;
htype="Rge";
hleft=arg2;
hright=arg1;
*)
let tac_zero_inf_false gl (n,d) ~status=
-debug("inizio tac_zero_inf_false\n");
+ 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 "1\n";let r =(PrimitiveTactics.apply_tac ~term:_Rnot_lt0 ~status) in
debug("fine\n");
r)
else
(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 ^"\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
+ 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 ^"\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
)
let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl)));
let (proof,goals) =
- rewrite_tac ~term:(C.Meta (fresh_meta,irl))
+ 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");
+debug("fine EQ -> goals : "^string_of_int( List.length new_goals) ^" = "
+ ^string_of_int( List.length goals)^"+ meta\n");
(proof,new_goals)
;;
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)
+ match x with
+ Some(Cic.Name(nm),t) -> (nm,exact ~term:(Cic.Rel(!num)))
+ | _ -> ("fake",tcl_fail 1)
)
context
in
(* 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";
+ (h1,c1)::lutil ->
+ debug ("elem di lutil ");Fourier.print_rational c1;print_string "\n";
- let s=ref (h1.hstrict) in
+ 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
+ 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) ->
+ List.iter (fun (h,c) ->
s:=(!s)||(h.hstrict);
t1:=(Cic.Appl [_Rplus;!t1;Cic.Appl
[_Rmult;rational_to_real c;h.hleft ] ]);
[_Rmult;rational_to_real c;h.hright] ]))
lutil;
- let ineq=Cic.Appl [(if (!s) then _Rlt else _Rle);!t1;!t2 ] in
- let tc=rational_to_real cres in
+ 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);
+ debug "inizio a costruire tac1\n";
+ 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 (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
- 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:[(*tac2;*)(Tacticals.thens
- ~start:(
- fun ~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:
- (* ******* *)
- [
- 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]
-
- ]
-
- );tac2(* < order *)
- ] (* end continuations before comment *)
- )
- );
- !tac1]
- );(*end tac:=*)
- tac:=(Tacticals.thens ~start:(PrimitiveTactics.cut_tac ~term:_False)
- ~continuations:[Tacticals.then_
- (* ???????????????????????????????
- in coq era intro *)
- ~start:(PrimitiveTactics.intros_tac ~name:"??")
- (* ????????????????????????????? *)
-
- ~continuation:contradiction_tac;!tac])
-
-
- |_-> assert false)(*match (!lutil) *)
+ 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
+ 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 ->
+ 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:[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]
+ ])
+ ;tac2]))
+ ;!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);;
-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
-
-;;
projects / helm.git / commitdiff