From: Claudio Sacerdoti Coen Date: Mon, 25 Sep 2006 16:52:53 +0000 (+0000) Subject: injection_tac and discriminate_tac now replaced by destruct_tac that X-Git-Tag: 0.4.95@7852~1001 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=070e79b6e7ec986dd5fcdee24857956f6a4a9221;p=helm.git injection_tac and discriminate_tac now replaced by destruct_tac that performs either injection or discrimination. In Coq destruct is called "analyze equality". --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index b516d393e..6bde8baee 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -57,7 +57,7 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Cut of loc * 'ident option * 'term | Decompose of loc * ('term, 'ident) type_spec list * 'ident option * 'ident list | Demodulate of loc - | Discriminate of loc * 'term + | Destruct of loc * 'term | Elim of loc * 'term * 'term option * int option * 'ident list | ElimType of loc * 'term * 'term option * int option * 'ident list | Exact of loc * 'term @@ -69,7 +69,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option | Goal of loc * int (* change current goal, argument is goal number 1-based *) | IdTac of loc - | Injection of loc * 'term | Intros of loc * int option * 'ident list | Inversion of loc * 'term | LApply of loc * bool * int option * 'term list * 'term * 'ident option diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index b78f6d90b..365bc9375 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -99,7 +99,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = let types = List.rev_map to_ident types in sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names)) | Demodulate _ -> "demodulate" - | Discriminate (_, term) -> "discriminate " ^ term_pp term + | Destruct (_, term) -> "destruct " ^ term_pp term | Elim (_, term, using, num, idents) -> sprintf "elim " ^ term_pp term ^ (match using with None -> "" | Some term -> " using " ^ term_pp term) @@ -123,7 +123,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Fail _ -> "fail" | Fourier _ -> "fourier" | IdTac _ -> "id" - | Injection (_, term) -> "injection " ^ term_pp term | Intros (_, None, []) -> "intros" | Inversion (_, term) -> "inversion " ^ term_pp term | Intros (_, num, idents) -> diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 2de83bc40..7f342b392 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -87,7 +87,7 @@ let tactic_of_ast ast = let mk_fresh_name_callback = namer_of names in Tactics.decompose ~mk_fresh_name_callback ~dbd ~user_types ?what | GrafiteAst.Demodulate _ -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) - | GrafiteAst.Discriminate (_,term) -> Tactics.discriminate term + | GrafiteAst.Destruct (_,term) -> Tactics.destruct term | GrafiteAst.Elim (_, what, using, depth, names) -> Tactics.elim_intros ?using ?depth ~mk_fresh_name_callback:(namer_of names) what @@ -124,7 +124,6 @@ let tactic_of_ast ast = Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern | GrafiteAst.Goal (_, n) -> Tactics.set_goal n | GrafiteAst.IdTac _ -> Tactics.id - | GrafiteAst.Injection (_,term) -> Tactics.injection term | GrafiteAst.Intros (_, None, names) -> PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () | GrafiteAst.Intros (_, Some num, names) -> @@ -183,7 +182,6 @@ let classify_tactic tactic = | GrafiteAst.Split _ | GrafiteAst.Replace _ | GrafiteAst.Reduce _ - | GrafiteAst.Injection _ | GrafiteAst.IdTac _ | GrafiteAst.Generalize _ | GrafiteAst.Elim _ diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index cdf01febd..6df39bfc4 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -165,9 +165,9 @@ let disambiguate_tactic metasenv,GrafiteAst.Decompose (loc, types, what, names) | GrafiteAst.Demodulate loc -> metasenv,GrafiteAst.Demodulate loc - | GrafiteAst.Discriminate (loc,term) -> + | GrafiteAst.Destruct (loc,term) -> let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Discriminate(loc,term) + metasenv,GrafiteAst.Destruct(loc,term) | GrafiteAst.Exact (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Exact (loc, cic) @@ -205,9 +205,6 @@ let disambiguate_tactic metasenv,GrafiteAst.Goal (loc, g) | GrafiteAst.IdTac loc -> metasenv,GrafiteAst.IdTac loc - | GrafiteAst.Injection (loc, term) -> - let metasenv,term = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Injection (loc,term) | GrafiteAst.Intros (loc, num, names) -> metasenv,GrafiteAst.Intros (loc, num, names) | GrafiteAst.Inversion (loc, term) -> diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 9373e54b4..ab15311df 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -160,8 +160,8 @@ EXTEND let to_spec id = GrafiteAst.Ident id in GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents) | IDENT "demodulate" -> GrafiteAst.Demodulate loc - | IDENT "discriminate"; t = tactic_term -> - GrafiteAst.Discriminate (loc, t) + | IDENT "destruct"; t = tactic_term -> + GrafiteAst.Destruct (loc, t) | IDENT "elim"; what = tactic_term; using = using; (num, idents) = intros_spec -> GrafiteAst.Elim (loc, what, using, num, idents) @@ -191,8 +191,6 @@ EXTEND | IDENT "goal"; n = int -> GrafiteAst.Goal (loc, n) | IDENT "id" -> GrafiteAst.IdTac loc - | IDENT "injection"; t = tactic_term -> - GrafiteAst.Injection (loc, t) | IDENT "intro"; ident = OPT IDENT -> let idents = match ident with None -> [] | Some id -> [id] in GrafiteAst.Intros (loc, Some 1, idents) diff --git a/matita/help/C/sec_tactics.xml b/matita/help/C/sec_tactics.xml index cd26700ab..468a27695 100644 --- a/matita/help/C/sec_tactics.xml +++ b/matita/help/C/sec_tactics.xml @@ -536,30 +536,35 @@ - - discriminate - discriminate - discriminate p + + destruct + destruct + destruct p Synopsis: - discriminate &sterm; + destruct &sterm; Pre-conditions: - p must have type K t1 ... tn = K' t'1 ... t'm where K and K' must be different constructors of the same inductive type and each argument list can be empty if -its constructor takes no arguments. + p must have type E1 = E2 where the two sides of the equality are possibly applied constructors of an inductive type. Action: - It closes the current sequent by proving the absurdity of - p. + The tactic recursively compare the two sides of the equality + looking for different constructors in corresponding position. + If two of them are found, the tactic closes the current sequent + by proving the absurdity of p. Otherwise + it adds a new hypothesis for each leaf of the formula that + states the equality of the subformulae in the corresponding + positions on the two sides of the equality. + @@ -950,43 +955,6 @@ its constructor takes no arguments. - - injection - injection - injection p - - - - Synopsis: - - injection &sterm; - - - - Pre-conditions: - - p must have type K t1 ... tn = K t'1 ... t'n where both argument lists are empty if -K takes no arguments. - - - - Action: - - It derives new hypotheses by injectivity of - K. - - - - New sequents to prove: - - The new sequent to prove is equal to the current sequent - with the additional hypotheses - t1=t'1 ... tn=t'n. - - - - - intro intro diff --git a/matita/help/C/tactic_quickref.xml b/matita/help/C/tactic_quickref.xml index 2709769ba..1549d3794 100644 --- a/matita/help/C/tactic_quickref.xml +++ b/matita/help/C/tactic_quickref.xml @@ -92,7 +92,7 @@ | - discriminate sterm + destruct sterm @@ -160,11 +160,6 @@ - - - | - injection sterm - | diff --git a/matita/matita.lang b/matita/matita.lang index 4074041bb..2258e1229 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -92,7 +92,7 @@ contradiction cut decompose - discriminate + destruct elim elimType exact @@ -104,7 +104,6 @@ generalize goal id - injection intro intros inversion diff --git a/matita/tests/dependent_injection.ma b/matita/tests/dependent_injection.ma new file mode 100644 index 000000000..ebadd3c2e --- /dev/null +++ b/matita/tests/dependent_injection.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/dependent_injection/". + +include "legacy/coq.ma". + +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". + +inductive ttree : Type → Type := + tempty: ttree nat + | tnode : ∀A. ttree A → ttree A → ttree A. + +(* CSC: there is an undecidable unification problem here: + consider a constructor k : \forall x. f x -> i (g x) + The head of the outtype of the injection MutCase should be (f ?1) + such that (f ?1) unifies with (g d) [ where d is the Rel that binds + the corresponding right parameter in the outtype ] + Coq dodges the problem by generating an equality between sigma-types + (that state the existence of a ?1 such that ...) *) +theorem injection_test3: + ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'. + intros; + destruct H; + assumption. +qed. + +theorem injection_test3: + ∀t,t'. + tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty → + t = t'. + intros; + destruct H; + assumption. +qed. diff --git a/matita/tests/discriminate.ma b/matita/tests/discriminate.ma index f25061245..8b655de87 100644 --- a/matita/tests/discriminate.ma +++ b/matita/tests/discriminate.ma @@ -21,6 +21,8 @@ alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". +alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". inductive foo: Prop \def I_foo: foo. @@ -29,7 +31,7 @@ theorem stupid: 1 = 0 \to (\forall p:Prop. p \to not p). intros. generalize in match I_foo. - discriminate H. + destruct H. qed. inductive bar_list (A:Set): Set \def @@ -41,7 +43,7 @@ theorem stupid2: \forall A:Set.\forall x:A.\forall l:bar_list A. bar_nil A = bar_cons A x l \to False. intros. - discriminate H. + destruct H. qed. inductive dt (A:Type): Type \to Type \def @@ -51,7 +53,7 @@ inductive dt (A:Type): Type \to Type \def theorem stupid3: k1 False (False → True) = k2 False False True → False. intros; - discriminate H. + destruct H. qed. inductive dddt (A:Type): Type \to Type \def @@ -60,5 +62,10 @@ inductive dddt (A:Type): Type \to Type \def theorem stupid4: kkk1 False = kkk2 False \to False. intros; - discriminate H. + destruct H. +qed. + +theorem recursive: S (S (S O)) = S (S O) \to False. + intros; + destruct H. qed. \ No newline at end of file diff --git a/matita/tests/injection.ma b/matita/tests/injection.ma index 7d9586fd1..b8ddeaa17 100644 --- a/matita/tests/injection.ma +++ b/matita/tests/injection.ma @@ -26,7 +26,7 @@ inductive t0 : Type := theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'. intros; - injection H; + destruct H; assumption. qed. @@ -36,7 +36,7 @@ inductive t : Type → Type := theorem injection_test1: ∀n,n'. k n = k n' → n = n'. intros; - injection H; + destruct H; assumption. qed. @@ -46,7 +46,7 @@ inductive tt (A:Type) : Type -> Type := theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'. intros; - injection H; + destruct H; assumption. qed. @@ -54,31 +54,9 @@ inductive ttree : Type → Type := tempty: ttree nat | tnode : ∀A. ttree A → ttree A → ttree A. -(* CSC: there is an undecidable unification problem here: - consider a constructor k : \forall x. f x -> i (g x) - The head of the outtype of the injection MutCase should be (f ?1) - such that (f ?1) unifies with (g d) [ where d is the Rel that binds - the corresponding right parameter in the outtype ] - Coq dodges the problem by generating an equality between sigma-types - (that state the existence of a ?1 such that ...) -theorem injection_test3: - ∀t,t'. tnode nat t tempty = tnode nat t' tempty → t = t'. - intros; - injection H; - assumption. -qed. - -theorem injection_test3: - ∀t,t'. - tnode nat (tnode nat t t') tempty = tnode nat (tnode nat t' tempty) tempty → - t = t'. - intros; - injection H; -*) - theorem injection_test4: ∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'. intros; - injection H; + destruct H; assumption. -qed. \ No newline at end of file +qed.