From 17d5498ae78a00bc81aaa8d87a925a2d6a2cf050 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Michele=20Galat=C3=A0?= Date: Tue, 3 Dec 2002 11:02:33 +0000 Subject: [PATCH] Added new tactics: Exists, Split, Assumption, Absurd, Generalize (doesn't work) Moved ElimType from ring.ml to variousTactics.ml Moved Contradiction from fourierR.ml to variousTactics.ml --- helm/gTopLevel/fourierR.ml | 6 +- helm/gTopLevel/fourierR.mli | 3 + helm/gTopLevel/gTopLevel.ml | 58 +++-- helm/gTopLevel/proofEngine.ml | 19 +- helm/gTopLevel/proofEngine.mli | 14 ++ helm/gTopLevel/ring.ml | 6 +- helm/gTopLevel/ring.mli | 2 + helm/gTopLevel/variousTactics.ml | 402 ++++++++++++++++++++++++++++-- helm/gTopLevel/variousTactics.mli | 19 +- 9 files changed, 478 insertions(+), 51 deletions(-) diff --git a/helm/gTopLevel/fourierR.ml b/helm/gTopLevel/fourierR.ml index f6f44e950..07a94a9b1 100644 --- a/helm/gTopLevel/fourierR.ml +++ b/helm/gTopLevel/fourierR.ml @@ -25,6 +25,7 @@ (******************** OTHER USEFUL TACTICS **********************) +(* Galla: moved in variousTactics.ml let rewrite_tac ~term:equality ~status:(proof,goal) = let module C = Cic in @@ -85,6 +86,7 @@ let rewrite_simpl_tac ~term ~status = (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~term:None) ~status ;; +*) (******************** THE FOURIER TACTIC ***********************) @@ -966,7 +968,7 @@ debug("inizio EQ\n"); let metasenv' = (fresh_meta,context,a_eq_b)::metasenv in debug("chamo rewrite tac su"^CicPp.ppterm (C.Meta (fresh_meta,irl))); let (proof,goals) = - rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) + VariousTactics.rewrite_simpl_tac ~term:(C.Meta (fresh_meta,irl)) ~status:((curi,metasenv',pbo,pty),goal) in let new_goals = fresh_meta::goals in @@ -1002,7 +1004,7 @@ 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:(Ring.elim_type_tac ~term:_False) + ~start:(VariousTactics.elim_type_tac ~term:_False) ~continuation:(assumption_tac)) ~status:(proof,goal) ;; diff --git a/helm/gTopLevel/fourierR.mli b/helm/gTopLevel/fourierR.mli index fbd55e685..e5790ec0f 100644 --- a/helm/gTopLevel/fourierR.mli +++ b/helm/gTopLevel/fourierR.mli @@ -1,2 +1,5 @@ +(* +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +*) val fourier_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index ce2af709a..9bab1ff9b 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -60,26 +60,14 @@ let htmlfooter = "" ;; -(* TASSI *) -let prooffile = "/home/tassi/miohelm/tmp/currentproof";; -let prooffiletype = "/home/tassi/miohelm/tmp/currentprooftype";; - -(* -let prooffile = "/public/sacerdot/currentproof";; -let prooffiletype = "/public/sacerdot/currentprooftype";; -*) +let prooffile = "/home/galata/miohelm/currentproof";; +let prooffiletype = "/home/galata/miohelm/currentprooftype";; (*CSC: the getter should handle the innertypes, not the FS *) -(* TASSI *) -let innertypesfile = "/home/tassi/miohelm/tmp/innertypes";; -let constanttypefile = "/home/tassi/miohelm/tmp/constanttype";; - -(* -let innertypesfile = "/public/sacerdot/innertypes";; -let constanttypefile = "/public/sacerdot/constanttype";; -*) +let innertypesfile = "/home/galata/miohelm/innertypes";; +let constanttypefile = "/home/galata/miohelm/constanttype";; let empty_id_to_uris = ([],function _ -> None);; @@ -1909,9 +1897,17 @@ let rewritesimpl = call_tactic_with_input ProofEngine.rewrite_simpl;; let reflexivity = call_tactic ProofEngine.reflexivity;; let symmetry = call_tactic ProofEngine.symmetry;; let transitivity = call_tactic_with_input ProofEngine.transitivity;; +let exists = call_tactic ProofEngine.exists;; +let split = call_tactic ProofEngine.split;; let left = call_tactic ProofEngine.left;; let right = call_tactic ProofEngine.right;; let assumption = call_tactic ProofEngine.assumption;; +let generalize = call_tactic_with_goal_input ProofEngine.generalize;; +let absurd = call_tactic_with_input ProofEngine.absurd;; +let contradiction = call_tactic ProofEngine.contradiction;; +(* Galla: come dare alla tattica la lista di termini da decomporre? +let decompose = call_tactic_with_input_and_goal_input ProofEngine.decompose;; +*) let whd_in_scratch scratch_window = call_tactic_with_goal_input_in_scratch ProofEngine.whd_in_scratch @@ -2355,6 +2351,12 @@ object(self) let transitivityb = GButton.button ~label:"Transitivity" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let existsb = + GButton.button ~label:"Exists" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let splitb = + GButton.button ~label:"Split" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in let leftb = GButton.button ~label:"Left" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in @@ -2364,9 +2366,21 @@ object(self) let assumptionb = GButton.button ~label:"Assumption" ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let generalizeb = + GButton.button ~label:"Generalize" + ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + let hbox6 = + GPack.hbox ~packing:(vbox1#pack ~expand:false ~fill:false ~padding:5) () in + let absurdb = + GButton.button ~label:"Absurd" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + let contradictionb = + GButton.button ~label:"Contradiction" + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in let searchpatternb = GButton.button ~label:"SearchPattern_Apply" - ~packing:(hbox5#pack ~expand:false ~fill:false ~padding:5) () in + ~packing:(hbox6#pack ~expand:false ~fill:false ~padding:5) () in + ignore(exactb#connect#clicked exact) ; ignore(applyb#connect#clicked apply) ; ignore(elimsimplintrosb#connect#clicked elimsimplintros) ; @@ -2386,9 +2400,14 @@ object(self) ignore(reflexivityb#connect#clicked reflexivity) ; ignore(symmetryb#connect#clicked symmetry) ; ignore(transitivityb#connect#clicked transitivity) ; + ignore(existsb#connect#clicked exists) ; + ignore(splitb#connect#clicked split) ; ignore(leftb#connect#clicked left) ; ignore(rightb#connect#clicked right) ; ignore(assumptionb#connect#clicked assumption) ; + ignore(generalizeb#connect#clicked generalize) ; + ignore(absurdb#connect#clicked absurd) ; + ignore(contradictionb#connect#clicked contradiction) ; ignore(introsb#connect#clicked intros) ; ignore(searchpatternb#connect#clicked searchPattern) ; ignore(proofw#connect#selection_changed (choose_selection proofw)) ; @@ -2638,12 +2657,17 @@ let initialize_everything () = let _ = if !usedb then +(*<<<<<<< gTopLevel.ml +(* Mqint.init "dbname=helm_mowgli" ; *) +Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; +=======*) begin Mqint.set_database Mqint.postgres_db ; (* Mqint.init "dbname=helm_mowgli" ; *) (* Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli user=helm" ; *) Mqint.init "host=mowgli.cs.unibo.it dbname=helm_mowgli_new_schema user=helm" ; end ; +(*>>>>>>> 1.35.2.34*) ignore (GtkMain.Main.init ()) ; initialize_everything () ; if !usedb then Mqint.close (); diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml index 55531c2aa..dbf04c393 100644 --- a/helm/gTopLevel/proofEngine.ml +++ b/helm/gTopLevel/proofEngine.ml @@ -205,19 +205,34 @@ let fold term = (* other tactics *) -let elim_type term = apply_tactic (Ring.elim_type_tac ~term) +let elim_type term = apply_tactic (VariousTactics.elim_type_tac ~term) let ring () = apply_tactic Ring.ring_tac let fourier () = apply_tactic FourierR.fourier_tac -let rewrite_simpl term = apply_tactic (FourierR.rewrite_simpl_tac ~term) +let rewrite_simpl term = apply_tactic (VariousTactics.rewrite_simpl_tac ~term) let reflexivity () = apply_tactic VariousTactics.reflexivity_tac let symmetry () = apply_tactic VariousTactics.symmetry_tac let transitivity term = apply_tactic (VariousTactics.transitivity_tac ~term) +let exists () = apply_tactic VariousTactics.exists_tac +let split () = apply_tactic VariousTactics.split_tac let left () = apply_tactic VariousTactics.left_tac let right () = apply_tactic VariousTactics.right_tac let assumption () = apply_tactic VariousTactics.assumption_tac + +let generalize term = apply_tactic (VariousTactics.generalize_tac ~term) + +let absurd term = apply_tactic (VariousTactics.absurd_tac ~term) +let contradiction () = apply_tactic VariousTactics.contradiction_tac + +let decompose ~clist = apply_tactic (VariousTactics.decompose_tac ~clist) + +(* +let decide_equality () = apply_tactic VariousTactics.decide_equality_tac +let compare term1 term2 = apply_tactic (VariousTactics.compare_tac ~term1 ~term2) +*) + (* let prova_tatticali () = apply_tactic Tacticals.prova_tac *) diff --git a/helm/gTopLevel/proofEngine.mli b/helm/gTopLevel/proofEngine.mli index cbe4c8bc5..006471e9a 100644 --- a/helm/gTopLevel/proofEngine.mli +++ b/helm/gTopLevel/proofEngine.mli @@ -65,11 +65,25 @@ val reflexivity : unit -> unit val symmetry : unit -> unit val transitivity : Cic.term -> unit +val exists : unit -> unit +val split : unit -> unit val left : unit -> unit val right : unit -> unit val assumption : unit -> unit +val generalize : Cic.term -> unit + +val absurd : Cic.term -> unit +val contradiction : unit -> unit + +val decompose : clist:(Cic.term list) -> unit + +(* +val decide_equality : unit -> unit +val compare : Cic.term -> Cic.term -> unit +*) + (* val prova_tatticali : unit -> unit *) diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 399d2c289..66541d1b0 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -404,6 +404,7 @@ let status_of_single_goal_tactic_result = | _ -> raise (Fail "status_of_single_goal_tactic_result: the tactic did not produce exactly a new goal") +(* Galla: spostata in variousTactics.ml (** auxiliary tactic "elim_type" @param status current proof engine status @@ -413,6 +414,7 @@ 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 +*) (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof @@ -422,10 +424,10 @@ let elim_type_tac ~term ~status = *) let elim_type2_tac ~term ~proof ~status = warn "in Ring.elim_type2"; - Tacticals.thens ~start:(elim_type_tac ~term) + Tacticals.thens ~start:(VariousTactics.elim_type_tac ~term) ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status -(* spostata in variousTactics.ml +(* Galla: spostata in variousTactics.ml (** Reflexivity tactic, try to solve current goal using "refl_eqT" Warning: this isn't equale to the coq's Reflexivity because this one tries diff --git a/helm/gTopLevel/ring.mli b/helm/gTopLevel/ring.mli index 79cb6f559..b6eb34b69 100644 --- a/helm/gTopLevel/ring.mli +++ b/helm/gTopLevel/ring.mli @@ -2,8 +2,10 @@ (* ring tactics *) val ring_tac: ProofEngineTypes.tactic +(*Galla: spostata in variuosTactics.ml (* auxiliary tactics *) val elim_type_tac: term: Cic.term -> ProofEngineTypes.tactic +*) (* spostata in variousTactics.ml val reflexivity_tac: ProofEngineTypes.tactic diff --git a/helm/gTopLevel/variousTactics.ml b/helm/gTopLevel/variousTactics.ml index 53a1347ad..35122025c 100644 --- a/helm/gTopLevel/variousTactics.ml +++ b/helm/gTopLevel/variousTactics.ml @@ -30,9 +30,9 @@ let constructor_tac ~n ~status:(proof, goal) = 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") ;; @@ -86,24 +86,24 @@ 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 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") @@ -115,47 +115,395 @@ let transitivity_tac ~term ~status:((proof, goal) as status) = 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") +;; + diff --git a/helm/gTopLevel/variousTactics.mli b/helm/gTopLevel/variousTactics.mli index 660ac17f5..30887a60a 100644 --- a/helm/gTopLevel/variousTactics.mli +++ b/helm/gTopLevel/variousTactics.mli @@ -27,7 +27,9 @@ val reflexivity_tac: ProofEngineTypes.tactic val symmetry_tac: ProofEngineTypes.tactic val transitivity_tac: term:Cic.term -> ProofEngineTypes.tactic +(* val constructor_tac: n:int -> ProofEngineTypes.tactic +*) val exists_tac: ProofEngineTypes.tactic val split_tac: ProofEngineTypes.tactic val left_tac: ProofEngineTypes.tactic @@ -35,6 +37,21 @@ val right_tac: ProofEngineTypes.tactic val assumption_tac: ProofEngineTypes.tactic +val generalize_tac: term:Cic.term -> ProofEngineTypes.tactic + +val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic + +val absurd_tac: term:Cic.term -> ProofEngineTypes.tactic +val contradiction_tac: ProofEngineTypes.tactic + +val decompose_tac: clist:(Cic.term list) -> ProofEngineTypes.tactic + (* -val generalize_tac: Cic.term -> ProofEnginrTypes.tactic +val decide_equality_tac: ProofEngineTypes.tactic +val compare_tac: term1:Cic.term -> term2:Cic.term -> ProofEngineTypes.tactic *) + +val rewrite_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_simpl_tac: term:Cic.term -> ProofEngineTypes.tactic +val rewrite_back_tac: term:Cic.term -> ProofEngineTypes.tactic +val replace_tac: what:Cic.term -> with_what:Cic.term -> ProofEngineTypes.tactic -- 2.39.2