| 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
| 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
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)
| Fail _ -> "fail"
| Fourier _ -> "fourier"
| IdTac _ -> "id"
- | Injection (_, term) -> "injection " ^ term_pp term
| Intros (_, None, []) -> "intros"
| Inversion (_, term) -> "inversion " ^ term_pp term
| Intros (_, num, idents) ->
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
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) ->
| GrafiteAst.Split _
| GrafiteAst.Replace _
| GrafiteAst.Reduce _
- | GrafiteAst.Injection _
| GrafiteAst.IdTac _
| GrafiteAst.Generalize _
| GrafiteAst.Elim _
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)
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) ->
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)
| 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)
</variablelist>
</para>
</sect1>
- <sect1 id="tac_discriminate">
- <title>discriminate</title>
- <titleabbrev>discriminate</titleabbrev>
- <para><userinput>discriminate p</userinput></para>
+ <sect1 id="tac_destruct">
+ <title>destruct</title>
+ <titleabbrev>destruct</titleabbrev>
+ <para><userinput>destruct p</userinput></para>
<para>
<variablelist>
<varlistentry role="tactic.synopsis">
<term>Synopsis:</term>
<listitem>
- <para><emphasis role="bold">discriminate</emphasis> &sterm;</para>
+ <para><emphasis role="bold">destruct</emphasis> &sterm;</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Pre-conditions:</term>
<listitem>
- <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K' t'<subscript>1</subscript> ... t'<subscript>m</subscript></command> where <command>K</command> and <command>K'</command> must be different constructors of the same inductive type and each argument list can be empty if
-its constructor takes no arguments.</para>
+ <para><command>p</command> must have type <command>E<subscript>1</subscript> = E<subscript>2</subscript></command> where the two sides of the equality are possibly applied constructors of an inductive type.</para>
</listitem>
</varlistentry>
<varlistentry>
<term>Action:</term>
<listitem>
- <para>It closes the current sequent by proving the absurdity of
- <command>p</command>.</para>
+ <para>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 <command>p</command>. 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.
+ </para>
</listitem>
</varlistentry>
<varlistentry>
</variablelist>
</para>
</sect1>
- <sect1 id="tac_injection">
- <title>injection</title>
- <titleabbrev>injection</titleabbrev>
- <para><userinput>injection p</userinput></para>
- <para>
- <variablelist>
- <varlistentry role="tactic.synopsis">
- <term>Synopsis:</term>
- <listitem>
- <para><emphasis role="bold">injection</emphasis> &sterm;</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Pre-conditions:</term>
- <listitem>
- <para><command>p</command> must have type <command>K t<subscript>1</subscript> ... t<subscript>n</subscript> = K t'<subscript>1</subscript> ... t'<subscript>n</subscript></command> where both argument lists are empty if
-<command>K</command> takes no arguments.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>Action:</term>
- <listitem>
- <para>It derives new hypotheses by injectivity of
- <command>K</command>.</para>
- </listitem>
- </varlistentry>
- <varlistentry>
- <term>New sequents to prove:</term>
- <listitem>
- <para>The new sequent to prove is equal to the current sequent
- with the additional hypotheses
- <command>t<subscript>1</subscript>=t'<subscript>1</subscript></command> ... <command>t<subscript>n</subscript>=t'<subscript>n</subscript></command>.</para>
- </listitem>
- </varlistentry>
- </variablelist>
- </para>
- </sect1>
<sect1 id="tac_intro">
<title>intro</title>
<titleabbrev>intro</titleabbrev>
<row>
<entry/>
<entry>|</entry>
- <entry><link linkend="tac_discriminate"><emphasis role="bold">discriminate</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
+ <entry><link linkend="tac_destruct"><emphasis role="bold">destruct</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
</row>
<row>
<entry/>
</link>
</entry>
</row>
- <row>
- <entry/>
- <entry>|</entry>
- <entry><link linkend="tac_injection"><emphasis role="bold">injection</emphasis></link> <emphasis><link linkend="grammar.sterm">sterm</link></emphasis></entry>
- </row>
<row>
<entry/>
<entry>|</entry>
<keyword>contradiction</keyword>
<keyword>cut</keyword>
<keyword>decompose</keyword>
- <keyword>discriminate</keyword>
+ <keyword>destruct</keyword>
<keyword>elim</keyword>
<keyword>elimType</keyword>
<keyword>exact</keyword>
<keyword>generalize</keyword>
<keyword>goal</keyword>
<keyword>id</keyword>
- <keyword>injection</keyword>
<keyword>intro</keyword>
<keyword>intros</keyword>
<keyword>inversion</keyword>
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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.
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.
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
\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
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
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
theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
theorem injection_test1: ∀n,n'. k n = k n' → n = n'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'.
intros;
- injection H;
+ destruct H;
assumption.
qed.
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.
projects / helm.git / commitdiff