- 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) *)