]> matita.cs.unibo.it Git - helm.git/commitdiff
injection_tac and discriminate_tac now replaced by destruct_tac that
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Sep 2006 16:52:53 +0000 (16:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 25 Sep 2006 16:52:53 +0000 (16:52 +0000)
performs either injection or discrimination. In Coq destruct is called
"analyze equality".

helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/matita/help/C/sec_tactics.xml
helm/software/matita/help/C/tactic_quickref.xml
helm/software/matita/matita.lang
helm/software/matita/tests/dependent_injection.ma [new file with mode: 0644]
helm/software/matita/tests/discriminate.ma
helm/software/matita/tests/injection.ma

index b516d393e12c123d3a539353fb83b62cc0ef211d..6bde8baee99f366f26dc66094544096c87f3aff3 100644 (file)
@@ -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
index b78f6d90b5999c97646f88430f01d2f3be140c7f..365bc9375f6d6a3a35ec45cb0d1da61e5e97ccfc 100644 (file)
@@ -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) ->
index 2de83bc4078b569613b2b922fc9dc0e791ba75a2..7f342b392dce3808de2c99770f767ddb55b06ae1 100644 (file)
@@ -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 _ 
index cdf01febd9da93bfc81ab797c31283033d696f8c..6df39bfc40e497a8623b1f2dd09eca1b69643305 100644 (file)
@@ -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) ->
index 9373e54b43a1de051f743a2581220677abaf4df8..ab15311dfd219c09bb7af3cc51b920724b62f071 100644 (file)
@@ -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)
index cd26700ab703a885027108ae4bd5fa217dea8830..468a27695c6e64495fd5450cc66b0eed395de912 100644 (file)
       </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>
@@ -950,43 +955,6 @@ its constructor takes no arguments.</para>
       </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>
index 2709769ba91f38b12439ea48465495daf1de079b..1549d3794a3b9e298afeca205f9e9f44ecbb7fb4 100644 (file)
@@ -92,7 +92,7 @@
       <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>
index 4074041bb5930f7b59474f52e0ac91283b450eb8..2258e1229a2a8a8ba3c1bd72ec223dcfe85ab9c0 100644 (file)
@@ -92,7 +92,7 @@
     <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>
diff --git a/helm/software/matita/tests/dependent_injection.ma b/helm/software/matita/tests/dependent_injection.ma
new file mode 100644 (file)
index 0000000..ebadd3c
--- /dev/null
@@ -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.
index f25061245e8ad7da6fc240302b9770997d0b1246..8b655de87bf8135c3494b88bea6ddcd2d5dbb682 100644 (file)
@@ -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
index 7d9586fd1badd4482f9dc88667cb01e755f42b89..b8ddeaa17f22dd077719e691e760c7fff34931a3 100644 (file)
@@ -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.