*)
-let constructor_tac ~n ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- 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)
- ~term: (C.MutConstruct (uri, typeno, n, exp_named_subst))
- | _ -> raise (ProofEngineTypes.Fail "Constructor failed")
-;;
-
-
-let exists_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let split_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let left_tac ~status =
- constructor_tac ~n:1 ~status
-;;
-
-
-let right_tac ~status =
- constructor_tac ~n:2 ~status
-;;
-
-
-let reflexivity_tac =
- constructor_tac ~n:1
-;;
-
-
-let symmetry_tac ~status:(proof, goal) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager 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 (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con", []))
-
- | (C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind")) ->
- PrimitiveTactics.apply_tac ~status:(proof,goal)
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con", []))
-
- | _ -> raise (ProofEngineTypes.Fail "Symmetry failed")
-;;
-
-
-let transitivity_tac ~term ~status:((proof, goal) as status) =
- let module C = Cic in
- let module R = CicReduction in
- let module U = UriManager 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")) ->
- T.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con", [])))
- ~continuations:
- [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")) ->
- T.thens
- ~start:(PrimitiveTactics.apply_tac
- ~term: (C.Const (U.uri_of_string "cic:/Coq/Init/Logic_Type/trans_eqT.con", [])))
- ~continuations:
- [T.id_tac ; T.id_tac ; PrimitiveTactics.exact_tac ~term]
- ~status
-
- | _ -> raise (ProofEngineTypes.Fail "Transitivity failed")
-;;
-
-
(* TODO se ce n'e' piu' di una, prende la prima che trova... sarebbe meglio chiedere *)
-
let assumption_tac ~status:((proof,goal) as status) =
let module C = Cic in
let module R = CicReduction in
(* 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_intros_simpl_tac ~term:(C.Rel 1) ; T.id_tac ]
- ~status
-;;
+(* IN FASE DI IMPLEMENTAZIONE *)
-let absurd_tac ~term ~status:((proof,goal) as status) =
+let generalize_tac ~term ~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,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
- ~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)
-;;
+(*
+let uno = (C.Appl [
+ C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 2, []) ;
+ C.MutConstruct (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind", 0, 1, [])]) in
+ let tuno = CicTypeChecker.type_of_aux' metasenv context uno in
+prerr_endline ("#### uno: " ^ CicPp.ppterm uno);
+prerr_endline ("#### tuno: " ^ CicPp.ppterm tuno);
*)
+prerr_endline ("#### dummy: " ^ (CicPp.ppterm (CicTypeChecker.type_of_aux' metasenv context term)));
+prerr_endline ("#### with_what: " ^ CicPp.ppterm (C.Rel 1));
+prerr_endline ("#### term: " ^ CicPp.ppterm term);
+prerr_endline ("#### ty: " ^ CicPp.ppterm ty);
-(* IN FASE DI IMPLEMENTAZIONE *)
-
-
-let generalize_tac ~term ~status:((proof,goal) as status) =
- let module C = Cic in
- let module P = PrimitiveTactics in
- let module T = Tacticals in
- let struct_equality t a = (t == a) in
- let _,metasenv,_,_ = proof in
- let _,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
T.thens
~start:(P.cut_tac
~term:(
- C.Lambda (
+ C.Prod (
(C.Name "dummy_for_gen"),
(CicTypeChecker.type_of_aux' metasenv context term),
- (ProofEngineReduction.replace
+ (ProofEngineReduction.replace_lifting
~equality:(==)
- ~with_what:(C.Rel 1)(* (C.Name "dummy_for_gen") *)
+ ~with_what:(C.Rel 1) (* C.Name "dummy_for_gen" *)
~what:term
- ~where:ty)))) (* dove?? nel goal va bene?*)
+ ~where:ty))))
~continuations:
- [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)
+ [T.id_tac ; (P.apply_tac ~term:(C.Appl [(C.Rel 1); term]))] (* in quest'ordine o viceversa? provare *)
+(* [(P.apply_tac ~term:(C.Appl [(C.Rel 1); term])) ; T.id_tac] (* in quest'ordine o viceversa? provare *)*)
~status
;;
-(* PROVE DI DECOMPOSE
-
-(* 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 generalize_tac ~term ~status:((proof,goal) as status) =
let module C = Cic in
- let module R = CicReduction in
+ let module H = ProofEngineHelpers in
let module P = PrimitiveTactics in
let module T = Tacticals in
- let module S = ProofEngineStructuralRules in
- let (_,metasenv,_,_) = proof 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_intros_simpl_tac ~term)
- ~continuation:(S.clear ~hyp:(Some ((C.Name "FOO") , (C.Decl ty)))) (* ma che ipotesi sto cancellando??? *)
- ~status
+ let add_decl_tac ~term ~status:(proof, goal) =
+ let module C = Cic in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _ = CicTypeChecker.type_of_aux' metasenv context term in
+ let newmeta = H.new_meta ~proof in
+ let context_for_newmeta = (Some (C.Name "dummy_for_gen",C.Decl term))::context in
+ let irl = H.identity_relocation_list_for_metavariable context_for_newmeta in
+ let newmetaty = CicSubstitution.lift 1 ty in
+ let bo' = C.LetIn (C.Name "dummy_for_gen" , term , C.Meta (newmeta,irl)) in
+ let (newproof, _) = H.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty]
+ in
+ (newproof, [newmeta])
+
in
- T.repeat_tactic ~tactic:(decompose_one_tac ~clist) ~status
+ T.then_
+ ~start:(add_decl_tac ~term:(CicTypeChecker.type_of_aux' metasenv context term))
+ ~continuation:(
+T.id_tac) (* T.thens
+ ~start:(P.cut_tac ~term:(ProofEngineReduction.replace
+ ~equality:(==)
+ ~with_what:(C.Rel 1) (* dummy_for_gen *)
+ ~what:term
+ ~where:ty))
+ ~continuations:
+ [T.id_tac ; (P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)]))]) (* in quest'ordine o viceversa? provare *)
+(* [(P.apply_tac ~term:(C.Appl [term ; (C.Rel 1)])) ; T.id_tac]) in quest'ordine o viceversa? provare *)
+*) ~status
;;
+*)
+
let decide_equality_tac =
then
T.thens
~start:P.cut_tac ~term:(* term1=term2->gty/\~term1=term2->gty *)
- ~continuations:[split_tac ; intros_tac ~name:"FOO"]
+ ~continuations:[split_tac ; P.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])
-
-;;
+(*** DOMANDE ***
+- come faccio clear di un ipotesi di cui non so il nome?
+- differenza tra elim e induction ...e inversion?
+- come passo a decompose la lista di termini?
+- ma la rewrite funzionava?
+- come implemento la generalize?
-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
- ~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