let (_,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
match (R.whd context ty) with
- (C.MutInd (uri,typeno,exp_named_subst))
- | (C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::_)) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
+ (C.MutInd (uri, typeno, exp_named_subst))
+ | (C.Appl ((C.MutInd (uri, typeno, exp_named_subst))::_)) ->
+ PrimitiveTactics.apply_tac ~status:(proof, goal)
~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
| _ -> raise (ProofEngineTypes.Fail "Constructor failed")
;;
let module C = Cic in
let module R = CicReduction in
let module U = UriManager in
- let module Tl = Tacticals in
+ let module T = Tacticals in
let (_,metasenv,_,_) = proof in
let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
- Tl.thens
+ T.thens
~start:(PrimitiveTactics.apply_tac
~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
~continuations:
- [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
+ [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
~status
| (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- Tl.thens
+ T.thens
~start:(PrimitiveTactics.apply_tac
~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
~continuations:
- [Tl.id_tac ; Tl.id_tac ; PrimitiveTactics.exact_tac ~term]
+ [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
~status
| _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
let assumption_tac ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
- let module T = CicTypeChecker in
let module S = CicSubstitution in
let _,metasenv,_,_ = proof in
let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
let rec find n = function
hd::tl ->
-(* (let hdd = hd in
- match hdd with
- Some (name, termine) -> prerr_endline("####" ^ name ^ CicPp.ppterm termine)
- | None -> prerr_endline("#### None")
- );
-*) (match hd with
+ (match hd with
(Some (_, C.Decl t)) when
(R.are_convertible context (S.lift n t) ty) -> n
| (Some (_, C.Def t)) when
(R.are_convertible context
- (T.type_of_aux' metasenv context (S.lift n t)) ty) -> n
+ (CicTypeChecker.type_of_aux' metasenv context (S.lift n t)) ty) -> n
| _ -> find (n+1) tl
)
- | [] -> raise (ProofEngineTypes.Fail "No such assumption")
+ | [] -> raise (ProofEngineTypes.Fail "Assumption: No such assumption")
in PrimitiveTactics.apply_tac ~status ~term:(C.Rel (find 1 context))
;;
-(*
+(* Questa invece era in fourierR.ml
+let assumption_tac ~status:(proof,goal)=
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ 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)
+ )
+ context
+ in
+ Tacticals.try_tactics ~tactics:tac_list ~status:(proof,goal)
+;;
+*)
+
+
+(* ANCORA DA DEBUGGARE *)
+
+
+let elim_type_tac ~term ~status =
+ let module C = Cic in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ T.thens
+ ~start: (P.cut_tac ~term)
+ ~continuations:[ P.elim_simpl_intros_tac ~term:(C.Rel 1) ; T.id_tac ]
+ ~status
+;;
+
+(* Questa era gia' in ring.ml!!!! NB: adesso in ring non c'e' piu' :-)
+let elim_type_tac ~term ~status =
+ warn "in Ring.elim_type_tac";
+ Tacticals.thens ~start:(cut_tac ~term)
+ ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status
+*)
+
+
+let absurd_tac ~term ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module U = UriManager in
+ let module P = PrimitiveTactics in
+ let _,metasenv,_,_ = proof in
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ if ((CicTypeChecker.type_of_aux' metasenv context term) = (C.Sort C.Prop))
+ then P.apply_tac ~term:(C.Appl [(C.Const ((U.uri_of_string "cic:/Coq/Init/Logic/absurd.con") , [] )) ; term ; ty]) ~status
+ else raise (ProofEngineTypes.Fail "Absurd: Not a Proposition")
+;;
+
+
+let contradiction_tac ~status =
+ let module C = Cic in
+ let module U = UriManager in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ T.then_
+ ~start: (P.intros_tac ~name:"FOO")
+ ~continuation:(
+ T.then_
+ ~start: (elim_type_tac ~term:(C.MutInd (U.uri_of_string "cic:/Coq/Init/Logic/False.ind") 0 [] ))
+ ~continuation: assumption_tac)
+ ~status
+;;
+
+(* Questa era in fourierR.ml
+(* !!!!! fix !!!!!!!!!! *)
+let contradiction_tac ~status:(proof,goal)=
+ Tacticals.then_
+ ~start:(PrimitiveTactics.intros_tac ~name:"bo?" ) (*inutile sia questo che quello prima della chiamata*)
+ ~continuation:(Tacticals.then_
+ ~start:(VariousTactics.elim_type_tac ~term:_False)
+ ~continuation:(assumption_tac))
+ ~status:(proof,goal)
+;;
+*)
+
+
+(* IN FASE DI IMPLEMENTAZIONE *)
+
+
let generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
- let module R = CicReduction in
- let module T = CicTypeChecker in
let module P = PrimitiveTactics in
- let module Tl = Tacticals in
+ let module T = Tacticals in
+ let struct_equality t a = (t == a) in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
- Tl.thens
- ~start:(P.cut_tac ~term:(C.Lambda ("dummy_for_gen", (T.type_of_aux' metasenv context term), (R.replace ?????? (C.Name "dummy_for_gen") term )))
- ~continuations: [(P.apply_tac (C.Appl [(C.Rel 1); term])); Tl.id_tac] (* in quest'ordine o viceversa? provare *)
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ T.thens
+ ~start:(P.cut_tac
+ ~term:(
+ C.Lambda (
+ (C.Name "dummy_for_gen"),
+ (CicTypeChecker.type_of_aux' metasenv context term),
+ (ProofEngineReduction.replace
+ ~equality:(==)
+ ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
+ ~what:term
+ ~where:ty)))) (* dove?? nel goal va bene?*)
+ ~continuations:
+ [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)
~status
;;
+(* PROVE DI DECOMPOSE
-let absurd_tac ~term ~status:((proof,goal) as status) =
- PrimitiveTactics.cut_tac
+(* in realta' non so bene cosa contiene la lista what, io ho supposto contenga dei term (Const uri) *)
+let decompose_tac ~what ~where ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let module S = ProofEngineStructuralRules in
+
+ let rec decomposing ty what =
+ match (what) with
+ [] -> C.Implicit (* qui mi servirebbe un termine per cui elim_simpl_intros fallisce *)
+ | hd::tl as what ->
+ match ty with
+ (C.Appl (hd::_)) -> hd
+ | _ -> decomposing ty tl
+ in
+
+ let (_,metasenv,_,_) = proof in
+ let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ T.repeat_tactic
+ ~tactic:(T.then_
+ ~start:(P.elim_simpl_intros_tac ~term:(decomposing (R.whd context where) what))
+ ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl where)))) (* ma che ipotesi sto cancellando??? *)
+ )
+ ~status
+;;
+
+
+let decompose_tac ~clist ~status:((proof,goal) as status) =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let module S = ProofEngineStructuralRules in
+ let (_,metasenv,_,_) = proof in
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+
+ let rec repeat_elim ~term ~status = (* term -> status -> proof * (goal list) *)
+ try
+ let (proof, goallist) =
+ T.then_
+ ~start:(P.elim_simpl_intros_tac ~term)
+ ~continuation:(S.clear ~hyp:(Some ((C.Name "name"), (C.Decl ty)))) (* non so che ipotesi sto cancellando??? *)
+ ~status
+ in
+ let rec step proof goallist =
+ match goallist with
+ [] -> (proof, [])
+ | hd::tl ->
+ let (proof', goallist') = repeat_elim ~term ~status:(proof, hd) in
+ let (proof'', goallist'') = step proof' tl in
+ proof'', goallist'@goallist''
+ in
+ step proof goallist
+ with
+ (Fail _) -> T.id_tac
+
+ in
+ let rec decomposing ty clist = (* term -> (term list) -> bool *)
+ match (clist) with
+ [] -> false
+ | hd::tl as clist ->
+ match ty with
+ (C.Appl (hd::_)) -> true
+ | _ -> decomposing ty tl
+
+ in
+ let term = decomposing (R.whd context ty) clist in
+ if (term == C.Implicit)
+ then (Fail "Decompose: nothing to decompose or no application")
+ else repeat_elim ~term ~status
+;;
+*)
+
+let decompose_tac ~clist ~status =
+ let module C = Cic in
+ let module R = CicReduction in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let module S = ProofEngineStructuralRules in
+
+ let rec choose ty =
+ function
+ [] -> C.Implicit (* a cosa serve? *)
+ | hd::tl ->
+ match ty with
+ (C.Appl (hd::_)) -> hd
+ | _ -> choose ty tl
+ in
+
+ let decompose_one_tac ~clist ~status:((proof,goal) as status) =
+ let (_,metasenv,_,_) = proof in
+ let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let term = choose (R.whd context ty) clist in
+ if (term == C.Implicit)
+ then raise (ProofEngineTypes.Fail "Decompose: nothing to decompose or no application")
+ else T.then_
+ ~start:(P.elim_simpl_intros_tac ~term)
+ ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)
+ ~status
+ in
+ T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
+;;
+
+
+let decide_equality_tac =
+ Tacticals.id_tac
+;;
+
+(*
+let compare_tac ~term1 ~term2 ~status:((proof, goal) as status) =
+ let module C = Cic in
+ let module U = UriManager in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let _,metasenv,_,_ = proof in
+ let _,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ if ((CicTypeChecker.type_of_aux' metasenv context term1) = (CicTypeChecker.type_of_aux' metasenv context term2))
+ (* controllo che i due termini siano comparabili *)
+ then
+ T.thens
+ ~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
+ ~continuations:[split_tac ; intros_tac ~name:"FOO"]
+ else raise (ProofEngineTypes.Fail "Compare: Comparing terms of different types")
;;
*)
+
+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/eq.ind") ->
+ let eq_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind_r.con",[])
+ 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",[])
+ 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.alpha_equivalence
+ ~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
+
+ let (proof',goals) =
+ PrimitiveTactics.exact_tac
+ ~term:(C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ assert (List.length goals = 0) ;
+ (proof',[fresh_meta])
+;;
+
+
+let rewrite_simpl_tac ~term ~status =
+ Tacticals.then_ ~start:(rewrite_tac ~term)
+ ~continuation:
+ (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None)
+ ~status
+;;
+
+
+let rewrite_back_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/eq.ind") ->
+ let eq_ind_r =
+ C.Const
+ (U.uri_of_string "cic:/Coq/Init/Logic/eq_ind.con",[])
+ 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.con",[])
+ 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.alpha_equivalence
+ ~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
+
+ let (proof',goals) =
+ PrimitiveTactics.exact_tac
+ ~term:(C.Appl
+ [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality])
+ ~status:((curi,metasenv',pbo,pty),goal)
+ in
+ assert (List.length goals = 0) ;
+ (proof',[fresh_meta])
+
+;;
+
+
+let replace_tac ~what ~with_what ~status:((proof, goal) as status) =
+ let module C = Cic in
+ let module U = UriManager in
+ let module P = PrimitiveTactics in
+ let module T = Tacticals in
+ let _,metasenv,_,_ = proof in
+ let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let wty = CicTypeChecker.type_of_aux' metasenv context what in
+ if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
+ then T.thens
+ ~start:(P.cut_tac ~term:(C.Appl [(C.MutInd ((U.uri_of_string "cic:/Coq/Init/Logic/eq.ind"), 0, [])) ; wty ; what ; with_what]))
+ (* quale uguaglianza usare, eq o eqT ? *)
+ ~continuations:[
+ T.then_
+ ~start:(P.intros_tac ~name:"dummy_for_replace")
+ ~continuation:(T.then_
+ ~start:(rewrite_back_tac ~term:(C.Rel 1)) (* C.Name "dummy_for_replace" *)
+ ~continuation:(ProofEngineStructuralRules.clear
+ ~hyp:(Some((C.Name "dummy_for_replace") , (C.Def C.Implicit) (* NO!! tipo di dummy *) ))
+ )
+ ) ;
+ T.id_tac]
+ ~status
+ else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
+;;
+
projects / helm.git / blobdiff