matita/matita/tests/destruct.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 "logic/equality.ma".
  18 include "nat/nat.ma".
  19 include "datatypes/constructors.ma".
  20
  21 theorem stupid:
  22   (S O) = O \to (\forall p:Prop. p \to Not p).
  23   intros.
  24   generalize in match I.
  25   destruct H.
  26 qed.
  27
  28 inductive bar_list (A:Set): Set \def
  29   | bar_nil: bar_list A
  30   | bar_cons: A \to bar_list A \to bar_list A.
  31
  32 theorem stupid2:
  33   \forall A:Set.\forall x:A.\forall l:bar_list A.
  34   bar_nil A = bar_cons A x l \to False.
  35   intros.
  36   destruct H.
  37 qed.
  38
  39 inductive dt (A:Type): Type \to Type \def
  40  | k1: \forall T:Type. dt A T
  41  | k2: \forall T:Type. \forall T':Type. dt A (T \to T').
  42
  43 theorem stupid3:
  44  k1 False (False → True) = k2 False False True → False.
  45  intros;
  46  destruct H.
  47 qed.
  48
  49 inductive dddt (A:Type): Type \to Type \def
  50  | kkk1: dddt A nat
  51  | kkk2: dddt A nat.
  52
  53 theorem stupid4: kkk1 False = kkk2 False \to False.
  54  intros;
  55  destruct H.
  56 qed.
  57
  58 theorem recursive: S (S (S O)) = S (S O) \to False.
  59  intros;
  60  destruct H.
  61 qed.
  62
  63 inductive complex (A,B : Type) : B → A → Type ≝
  64 | C1 : ∀x:nat.∀a:A.∀b:B. complex A B b a
  65 | C2 : ∀a,a1:A.∀b,b1:B.∀x:nat. complex A B b1 a1 → complex A B b a.
  66
  67 theorem recursive1: ∀ x,y : nat.
  68   (C1 ? ? O     (Some ? x) y) =
  69   (C1 ? ? (S O) (Some ? x) y) → False.
  70 intros; destruct H.
  71 qed.
  72
  73 theorem recursive2: ∀ x,y,z,t : nat.
  74   (C1 ? ? t (Some ? x) y) =
  75   (C1 ? ? z (Some ? x) y) → t=z.
  76 intros; destruct H; reflexivity.
  77 qed.
  78
  79 theorem recursive3: ∀ x,y,z,t : nat.
  80   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) =
  81   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
  82 intros; destruct H; reflexivity.
  83 qed.
  84
  85 theorem recursive4: ∀ x,y,z,t : nat.
  86   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) =
  87   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
  88 intros; destruct H; reflexivity.
  89 qed.
  90
  91 theorem recursive2: ∀ x,y : nat.
  92   C2 ? ? (None ?) ? (S O) ? O (C1 ? ? O     (Some ? x) y) =
  93   C2 ? ? (None ?) ? (S O) ? O (C1 ? ? (S O) (Some ? x) y) → False.
  94 intros; destruct H.
  95 qed.