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