*)
+(******************** OTHER USEFUL TACTICS **********************)
+
+let rewrite_tac ~term:equality ~status:(proof,goal) =
+ let module C = Cic in
+ 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 =
+ 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") ->
+ let eq_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic/Logic_lemmas/eq_ind_r.con",0)
+ in
+ eq_ind_r,ty,t1,t2
+ | C.Appl [C.MutInd (uri,_,0) ; ty ; t1 ; t2]
+ when U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") ->
+ let eqT_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind_r.con",0)
+ in
+ eqT_ind_r,ty,t1,t2
+ | _ ->
+ raise
+ (ProofEngineTypes.Fail
+ "Rewrite: the argument is not a proof of an equality")
+ in
+ let pred =
+ let gty' = CicSubstitution.lift 1 gty in
+ let t1' = CicSubstitution.lift 1 t1 in
+ let gty'' =
+ ProofEngineReduction.replace_lifting
+ ~equality:
+ (ProofEngineReduction.syntactic_equality ~alpha_equivalence:true)
+ ~what:t1' ~with_what:(C.Rel 1) ~where:gty'
+ in
+ C.Lambda (C.Name "dummy_for_rewrite", ty, gty'')
+ in
+prerr_endline ("#### Sintetizzato: " ^ CicPp.ppterm pred);
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,C.Appl [pred ; t2])::metasenv in
+ PrimitiveTactics.exact_tac
+ (C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ((curi,metasenv',pbo,pty),goal)
+;;
+
+(******************** THE FOURIER TACTIC ***********************)
(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
des inéquations et équations sont entiers. En attendant la tactique Field.
*)
+let _eqT = Cic.MutInd(UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind") 0 0 ;;
let _False = Cic.MutInd (UriManager.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 0 ;;
let _not = Cic.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con") 0;;
let _R0 = Cic.Const (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con") 0 ;;
let rec int_to_real_aux n =
match n with
0 -> _R0 (* o forse R0 + R0 ????? *)
+ | 1 -> _R1
| _ -> Cic.Appl [ _Rplus ; _R1 ; int_to_real_aux (n-1) ]
;;
;;
-(* fix !!!!!!!!!! this may not work *)
let equality_replace a b ~status =
+ let module C = Cic in
let proof,goal = status in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
-prerr_endline ("<MY_CUT: " ^ CicPp.ppterm a ^ " <=> " ^ CicPp.ppterm b) ;
-prerr_endline ("### IN MY_CUT: ") ;
-prerr_endline ("@ " ^ CicPp.ppterm ty) ;
-List.iter (function Some (n,Cic.Decl t) -> prerr_endline ("# " ^ CicPp.ppterm t)) context ;
-prerr_endline ("##- IN MY_CUT ") ;
-let res =
- let _eqT_ind = Cic.Const( UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT_ind.con" ) 0 in
-(*CSC: codice ad-hoc per questo caso!!! Non funge in generale *)
- PrimitiveTactics.apply_tac ~term:(Cic.Appl [_eqT_ind;_R;b;Cic.Lambda(Cic.Name "pippo",_R,Cic.Appl [_not; Cic.Appl [_Rlt;_R0;Cic.Rel 1]])]) ~status
-in
-prerr_endline "EUREKA" ;
-res
+ let a_eq_b = C.Appl [ _eqT ; _R ; a ; b ] in
+ let fresh_meta = ProofEngineHelpers.new_meta proof in
+ let irl =
+ ProofEngineHelpers.identity_relocation_list_for_metavariable context in
+ let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in
+ let (proof,goals) =
+ rewrite_tac ~term:(C.Meta (fresh_meta,irl))
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ (proof,fresh_meta::goals)
;;
let tcl_fail a ~status:(proof,goal) =
PrimitiveTactics.apply_tac ~term:_Rfourier_lt ~status)
~continuations:[tac_use h1;
- Ring.id_tac] ~status
-
- (*tac_zero_inf_pos (rational_to_fraction c1)] ~status*)
+ tac_zero_inf_pos (rational_to_fraction c1)] ~status
)
else
)
~continuations:[!tac1;tac_use h;
- Ring.id_tac
- (*tac_zero_inf_pos
- (rational_to_fraction c)*)
+ tac_zero_inf_pos (rational_to_fraction c)
]))
)
~continuation:(Tacticals.then_
~start:(PrimitiveTactics.apply_tac
~term:(if sres then _Rnot_lt_lt else _Rnot_le_le))
- ~continuation:Ring.id_tac
-(*CSC
~continuation:(Tacticals.thens
~start:(equality_replace (Cic.Appl [_Rminus;!t2;!t1] ) tc)
~continuations:[tac2;(Tacticals.thens
)
] (* end continuations before comment *)
- ) *)
+ )
);
!tac1]
);(*end tac:=*)
;;
let fourier_tac ~status:(proof,goal) = fourier ~status:(proof,goal);;
-