matita/tests/injection.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15
  16
  17 include "coq.ma".
  18
  19 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  20 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
  21 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
  22
  23 inductive t0 : Type :=
  24    k0 : nat → nat → t0
  25  | k0' : bool → bool → t0.
  26
  27 theorem injection_test0: ∀n,n',m,m'. k0 n m = k0 n' m' → m = m'.
  28  intros;
  29  destruct H;
  30  reflexivity.
  31 qed.
  32
  33 inductive t : Type → Type :=
  34    k : nat → t nat
  35  | k': bool → t bool.
  36
  37 theorem injection_test1: ∀n,n'. k n = k n' → n = n'.
  38  intros;
  39  destruct H;
  40  reflexivity.
  41 qed.
  42
  43 inductive tt (A:Type) : Type -> Type :=
  44    k1: nat → nat → tt A nat
  45  | k2: bool → bool → tt A bool.
  46
  47 theorem injection_test2: ∀n,n',m,m'. k1 bool n n' = k1 bool m m' → n' = m'.
  48  intros;
  49  destruct H;
  50  reflexivity.
  51 qed.
  52
  53 inductive ttree : Type → Type :=
  54    tempty: ttree nat
  55  | tnode : ∀A. ttree A → ttree A → ttree A.
  56
  57 theorem injection_test4:
  58  ∀n,n',m,m'. k1 bool (S n) (S (S m)) = k1 bool (S n') (S (S (S m'))) → m = S m'.
  59  intros;
  60  destruct H;
  61  reflexivity.
  62 qed.