helm/software/matita/tests/discriminate.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 set "baseuri" "cic:/matita/tests/discriminate".
  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
  68 theorem recursive1: ∀ x,y : nat.
  69   (C1 ? ? O     (Some ? x) y) =
  70   (C1 ? ? (S O) (Some ? x) y) → False.
  71 intros; destruct H;
  72 qed.
  73
  74 theorem recursive2: ∀ x,y,z,t : nat.
  75   (C1 ? ? t (Some ? x) y) =
  76   (C1 ? ? z (Some ? x) y) → t=z.
  77 intros; destruct H;assumption.
  78 qed.
  79
  80 theorem recursive3: ∀ x,y,z,t : nat.
  81   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? x) y) =
  82   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
  83 intros; destruct H;assumption.
  84 qed.
  85
  86 theorem recursive4: ∀ x,y,z,t : nat.
  87   C2 ? ? (None ?) ? (S O) ? z (C1 ? ? (S O) (Some ? z) y) =
  88   C2 ? ? (None ?) ? (S O) ? t (C1 ? ? (S O) (Some ? x) y) → z=t.
  89 intros;
  90
  91
  92
  93
  94  (λHH  : ((C1 (option nat) nat (S O) (Some nat -7) -8) = (C1 (option nat) nat (S O) (Some nat -9) -8))
  95   eq_elim_r
  96     (complex (option nat) nat -8 (Some nat -7))
  97     (C1 (option nat) nat (S O) (Some nat -9) -8)
  98     (λc:(complex (option nat) nat -8 (Some nat -7)).
  99       (eq (option nat)
 100         ((λx:(complex (option nat) nat -8 (Some nat -7)).
 101            match x return (λy1:nat.(λy2:(option nat).(λ x:(complex (option nat) nat y1 y2).(option nat)))) with
 102            [ (C1 (y1:nat) (a:(option nat)) (b:nat)) => a
 103            | (C2 (a:(option nat)) (a1:(option nat)) (b:nat) (b1:nat) (y2:nat) (y3:(complex (option nat) nat b1 a1))) ⇒
 104               (Some nat -7)
 105            ]) c)
 106         (Some nat -9)))
 107      ?
 108      (C1 (option nat) nat (S O) (Some nat -7) -8)
 109      HH)
 110
 111
 112
 113
 114 destruct H;assumption.
 115 qed.
 116
 117 theorem recursive2: ∀ x,y : nat.
 118   C2 ? ? (None ?) ? (S O) ? O (C1 ? ? O     (Some ? x) y) =
 119   C2 ? ? (None ?) ? (S O) ? O (C1 ? ? (S O) (Some ? x) y) → False.
 120 intros; destruct H;
 121
 122