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 =
+
+ 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") ->
(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
*)
let ineq1_of_term (h,t) =
+ debug("Trasformo in ineq "^CicPp.ppterm t^"\n");
match t with (* match t *)
Cic.Appl (t1::next) ->
let arg1= List.hd next in
(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;
|_->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)(* match t1 *)
- |_-> assert false (* match t *)
+ |_-> 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;;
*)
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 ^" 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) ~status=
-debug("stat tac_zero_infeq_false");
-let r =
- (Tacticals.then_ ~start:(PrimitiveTactics.apply_tac ~term:_Rlt_not_le)
+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("stat tac_zero_infeq_false");
- r
+ debug("end tac_zero_infeq_false\n");
+ r*)
+ Ring.id_tac ~status
;;
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)));
+debug("chamo rewrite tac su "^CicPp.ppterm (C.Meta (fresh_meta,irl))^" e ty "^CicPp.ppterm ty ^"\n");
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
(* transform hyps into inequations *)
List.iter (fun h -> try (lineq:=(ineq1_of_term h)@(!lineq))
- with _-> ())
+ with _-> debug("Impossibile trasformare l'ipotesi "^CicPp.ppterm (snd h)^" in ineq\n");)
hyps;
let tac=ref Ring.id_tac in
if res=[] then
(print_string "Tactic Fourier fails.\n";flush stdout;
- failwith "fourier_tac fails")
+ failwith "fourier can't proove it")
else
(
match res with (*match res*)
(* 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);
-
- 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;
+ debug "inizio a costruire tac1\n";
+ Fourier.print_rational(c1);
- 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 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");
- 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) *)
+ 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);;
-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
-
-;;