From 50fd7ca0b4e54ee341517ea653b3862b9655d4c5 Mon Sep 17 00:00:00 2001 From: maiorino Date: Tue, 11 Jul 2006 15:44:46 +0000 Subject: [PATCH] First experimental version of the declarative proof language for Matita. Supported commands so far: assume id: term suppose term (id) by term done by term we proved term (id) we need to prove term (id) --- .../software/components/grafite/grafiteAst.ml | 6 ++ .../components/grafite/grafiteAstPp.ml | 4 +- .../grafite_engine/grafiteEngine.ml | 7 ++ .../grafite_parser/grafiteDisambiguate.ml | 17 +++++ .../grafite_parser/grafiteParser.ml | 11 +++ helm/software/components/tactics/.depend | 18 +++-- helm/software/components/tactics/Makefile | 2 +- .../components/tactics/declarative.ml | 51 +++++++++++++ .../components/tactics/declarative.mli | 5 ++ helm/software/matita/tests/decl.ma | 74 +++++++++++++++++++ 10 files changed, 186 insertions(+), 9 deletions(-) create mode 100644 helm/software/components/tactics/declarative.ml create mode 100644 helm/software/components/tactics/declarative.mli create mode 100644 helm/software/matita/tests/decl.ma diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 5896e116f..73ae34584 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -85,6 +85,12 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Split of loc | Symmetry of loc | Transitivity of loc * 'term + (* Costruttori Aggiunti *) + | Assume of loc * 'ident * 'term + | Suppose of loc * 'term *'ident + | By_term_we_proved of loc * 'term * 'term * 'ident + | We_need_to_prove of loc * 'term * 'ident + | Bydone of loc * 'term type search_kind = [ `Locate | `Hint | `Match | `Elim ] diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 941f75d9d..b95df8d36 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -154,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Split _ -> "split" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ term_pp term - -let pp_search_kind = function + + let pp_search_kind = function | `Locate -> "locate" | `Hint -> "hint" | `Match -> "match" diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index ebe7df369..ab43c6cc1 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -154,6 +154,13 @@ let tactic_of_ast ast = | GrafiteAst.Split _ -> Tactics.split | GrafiteAst.Symmetry _ -> Tactics.symmetry | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term + (* Implementazioni Aggiunte *) + | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t + | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id + | GrafiteAst.By_term_we_proved (_, t, ty, id) -> + Declarative.by_term_we_proved t ty id + | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id + | GrafiteAst.Bydone (_, t) -> Declarative.bydone t (* maybe we only need special cases for apply and goal *) let classify_tactic tactic = diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 6b7dd076b..b02d57e67 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -251,6 +251,23 @@ let disambiguate_tactic | GrafiteAst.Transitivity (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Transitivity (loc, cic) + (* Nuovi casi *) + | GrafiteAst.Assume (loc, id, term) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Assume (loc, id, cic) + | GrafiteAst.Suppose (loc, term, id) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Suppose (loc, cic, id) + | GrafiteAst.Bydone (loc,term) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Bydone (loc, cic) + | GrafiteAst.We_need_to_prove (loc,term,id) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.We_need_to_prove (loc,cic,id) + | GrafiteAst.By_term_we_proved (loc,term,term',id) -> + let metasenv,cic = disambiguate_term context metasenv term in + let metasenv,cic' = disambiguate_term context metasenv term' in + metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id) let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = let uri = diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 1a11ec62f..1c85b567d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -231,6 +231,17 @@ EXTEND GrafiteAst.Symmetry loc | IDENT "transitivity"; t = tactic_term -> GrafiteAst.Transitivity (loc, t) + (* Produzioni Aggiunte *) + | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> + GrafiteAst.Assume (loc, id, t) + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + GrafiteAst.Suppose (loc, t, id) + | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + GrafiteAst.By_term_we_proved (loc, t, ty, id) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + GrafiteAst.We_need_to_prove (loc, t, id) + | IDENT "by" ; t = tactic_term ; IDENT "done" -> + GrafiteAst.Bydone (loc, t) ] ]; atomic_tactical: diff --git a/helm/software/components/tactics/.depend b/helm/software/components/tactics/.depend index 500838027..43ed94aa9 100644 --- a/helm/software/components/tactics/.depend +++ b/helm/software/components/tactics/.depend @@ -24,10 +24,12 @@ autoTactic.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi ring.cmi: proofEngineTypes.cmi +setoids.cmi: proofEngineTypes.cmi fourierR.cmi: proofEngineTypes.cmi fwdSimplTactic.cmi: proofEngineTypes.cmi statefulProofEngine.cmi: proofEngineTypes.cmi tactics.cmi: proofEngineTypes.cmi +declarative.cmi: proofEngineTypes.cmi proofEngineTypes.cmo: proofEngineTypes.cmi proofEngineTypes.cmx: proofEngineTypes.cmi proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi @@ -63,17 +65,19 @@ paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/subst.cmo: paramodulation/subst.cmi paramodulation/subst.cmx: paramodulation/subst.cmi paramodulation/equality.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineReduction.cmi \ + paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \ paramodulation/equality.cmi paramodulation/equality.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx proofEngineReduction.cmx \ + paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \ paramodulation/equality.cmi paramodulation/inference.cmo: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineHelpers.cmi metadataQuery.cmi \ - paramodulation/equality.cmi paramodulation/inference.cmi + paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ + metadataQuery.cmi paramodulation/equality.cmi \ + paramodulation/inference.cmi paramodulation/inference.cmx: paramodulation/utils.cmx \ - paramodulation/subst.cmx proofEngineHelpers.cmx metadataQuery.cmx \ - paramodulation/equality.cmx paramodulation/inference.cmi + paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ + metadataQuery.cmx paramodulation/equality.cmx \ + paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \ @@ -186,3 +190,5 @@ tactics.cmx: variousTactics.cmx tacticals.cmx paramodulation/saturation.cmx \ introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \ equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \ autoTactic.cmx tactics.cmi +declarative.cmo: tactics.cmi tacticals.cmi declarative.cmi +declarative.cmx: tactics.cmx tacticals.cmx declarative.cmi diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile index e75a8f3ab..aa1606997 100644 --- a/helm/software/components/tactics/Makefile +++ b/helm/software/components/tactics/Makefile @@ -18,7 +18,7 @@ INTERFACE_FILES = \ equalityTactics.mli autoTactic.mli discriminationTactics.mli \ inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ - statefulProofEngine.mli tactics.mli + statefulProofEngine.mli tactics.mli declarative.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml new file mode 100644 index 000000000..c22d51af2 --- /dev/null +++ b/helm/software/components/tactics/declarative.ml @@ -0,0 +1,51 @@ +let assume id t = + Tacticals.then_ + ~start: + (Tactics.intros ~howmany:1 + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) + ~continuation: + (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> t,metasenv,ugraph)) +;; + +let suppose t id = + Tacticals.then_ + ~start: + (Tactics.intros ~howmany:1 + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) + ~continuation: + (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> t,metasenv,ugraph)) +;; + +let by_term_we_proved t ty id = + Tacticals.thens + ~start: + (Tactics.cut ty + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) + ~continuations: + [ Tacticals.id_tac ; Tactics.apply t ] +;; + +let bydone t = + (Tactics.apply ~term:t) + +;; + +let we_need_to_prove t id = + let aux status = + let proof,goals = + ProofEngineTypes.apply_tactic + (Tactics.cut t + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) + status + in + let goals' = + match goals with + [fst; snd] -> [snd; fst] + | _ -> assert false + in + proof,goals' + in + ProofEngineTypes.mk_tactic aux +;; diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli new file mode 100644 index 000000000..b745ef5a1 --- /dev/null +++ b/helm/software/components/tactics/declarative.mli @@ -0,0 +1,5 @@ +val assume : string -> Cic.term -> ProofEngineTypes.tactic +val suppose : Cic.term -> string -> ProofEngineTypes.tactic +val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic +val bydone : Cic.term -> ProofEngineTypes.tactic +val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic diff --git a/helm/software/matita/tests/decl.ma b/helm/software/matita/tests/decl.ma new file mode 100644 index 000000000..285d07c23 --- /dev/null +++ b/helm/software/matita/tests/decl.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/test/decl". + +include "nat/times.ma". +include "nat/orders.ma". + +theorem easy: ∀n,m. n * m = O → n = O ∨ m = O. + assume n: nat. + assume m: nat. + (* base case *) + by (refl_eq ? O) we proved (O = O) (trivial). + by (or_introl ? ? trivial) we proved (O = O ∨ m = O) (trivial2). + by (λ_.trivial2) we proved (O*m=O → O=O ∨ m=O) (base_case). + (* inductive case *) + we need to prove + (∀n1. (n1 * m = O → n1 = O ∨ m = O) → (S n1) * m = O → (S n1) = O ∨ m = O) + (inductive_case). + assume n1: nat. + suppose (n1 * m = O → n1 = O ∨ m = O) (inductive_hyp). + (* base case *) + by (or_intror ? ? trivial) we proved (S n1 = O ∨ O = O) (pre_base_case2). + by (λ_.pre_base_case2) we proved (S n1*O = O → S n1 = O ∨ O = O) (base_case2). + (* inductive case *) + we need to prove + (∀m1. (S n1 * m1 = O → S n1 = O ∨ m1 = O) → + (S n1 * S m1 = O → S n1 = O ∨ S m1 = O)) (inductive_hyp2). + assume m1: nat. + suppose (S n1 * m1 = O → S n1 = O ∨ m1 = O) (useless). + suppose (S n1 * S m1 = O) (absurd_hyp). + simplify in absurd_hyp. + by (sym_eq ? ? ? absurd_hyp) we proved (O = S (m1+n1*S m1)) (absurd_hyp'). + by (not_eq_O_S ? absurd_hyp') we proved False (the_absurd). + by (False_ind ? the_absurd) + done. + (* the induction *) + by (nat_ind (λm.S n1 * m = O → S n1 = O ∨ m = O) base_case2 inductive_hyp2 m) + done. + (* the induction *) + by (nat_ind (λn.n*m=O → n=O ∨ m=O) base_case inductive_case n) +done. +qed. + +theorem easy2: ∀n,m. n * m = O → n = O ∨ m = O. + intros 2. + elim n 0 + [ intro; + left; + reflexivity + | intro; + elim m 0 + [ intros; + right; + reflexivity + | intros; + simplify in H2; + lapply (sym_eq ? ? ? H2); + elim (not_eq_O_S ? Hletin) + ] + ] +qed. + \ No newline at end of file -- 2.39.2