- 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.id_tac;Tacticals.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
+ 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 ->
+ debug("t1 ="^CicPp.ppterm !t1 ^"t2 ="^CicPp.ppterm !t2 ^"tc="^ CicPp.ppterm tc^"\n");
+ 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:
+ [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?
+ CODICE NEL COMMENTO NON PORTATO. ORA ESISTE ANCHE LA TATTICA symmetry_tac
+ ~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)