helm/software/matita/tests/destruct_bb.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 include "logic/equality.ma".
  16
  17 include "nat/nat.ma".
  18 include "list/list.ma".
  19
  20 inductive list_x : Type ≝
  21 | nil_x  : list_x
  22 | cons_x : ∀T:Type.∀x:T.list_x → list_x.
  23
  24 let rec mk_prod (l:list_x) ≝
  25   match l with
  26   [ nil_x ⇒ Type
  27   | cons_x T x tl ⇒ ∀y0:T.∀p0:x = y0. mk_prod tl ].
  28
  29 let rec appl (l:list_x) : mk_prod l →  Type ≝
  30  match l return λl:list_x.mk_prod l →Type
  31  with
  32  [ nil_x ⇒ λT:mk_prod nil_x.T
  33  | cons_x Ty hd tl ⇒ λT:mk_prod (cons_x Ty hd tl).appl tl (T hd (refl_eq Ty hd)) ].
  34
  35 inductive list_xyp : list_x → Type ≝
  36 | nil_xyp  : ∀l.list_xyp l
  37 | cons_xyp : ∀l.∀T:mk_prod l.∀x:appl l T.list_xyp (cons_x ? x l) → list_xyp l.
  38
  39 (* let rec tau (l:list_x) (w:list_xyp l) on w: Type ≝
  40  match w with
  41  [ nil_xyp _ ⇒ Type
  42  | cons_xyp l' T' x' w' ⇒
  43      ∀y:appl l' T'.∀p:x' = y.
  44      tau (cons_x ? y l') w' ].
  45
  46 eval normalize on (
  47   ∀T0:Type.
  48   ∀a0:T0.
  49   ∀T1:∀x0:T0. a0=x0 → Type.
  50   ∀a1:T1 a0 (refl_eq ? a0).
  51 tau ? (cons_xyp nil_x T0 a0 (cons_xyp (cons_x T0 a0 nil_x) T1 a1 (nil_xyp ?))) Type).
  52
  53 inductive index_list (T: nat → Type): ∀m,n:nat.Type ≝
  54 | il_s : ∀n.T n → index_list T n n
  55 | il_c : ∀m,n. T m → index_list T (S m) n → index_list T m n.
  56
  57 lemma down_il : ∀T:nat → Type.∀m,n.∀l: index_list T m n.∀f:(∀p. T (S p) → T p).
  58                 ∀m',n'.S m' = m → S n' = n → index_list T m' n'.
  59 intros 5;elim i
  60 [destruct;apply il_s;apply f;assumption
  61 |apply il_c
  62  [apply f;rewrite > H;assumption
  63  |apply f1
  64   [rewrite > H;reflexivity
  65   |assumption]]]
  66 qed. *)
  67
  68 definition R1 ≝ eq_rect'.
  69
  70 definition R2 :
  71   ∀T0:Type.
  72   ∀a0:T0.
  73   ∀T1:∀x0:T0. a0=x0 → Type.
  74   ∀a1:T1 a0 (refl_eq ? a0).
  75   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
  76   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
  77   ∀b0:T0.
  78   ∀e0:a0 = b0.
  79   ∀b1: T1 b0 e0.
  80   ∀e1:R1 ??? a1 ? e0 = b1.
  81   T2 b0 e0 b1 e1.
  82 intros 9;intro e1;
  83 apply (eq_rect' ????? e1);
  84 apply (R1 ?? ? ?? e0);
  85 simplify;assumption;
  86 qed.
  87
  88 definition R3 :
  89   ∀T0:Type.
  90   ∀a0:T0.
  91   ∀T1:∀x0:T0. a0=x0 → Type.
  92   ∀a1:T1 a0 (refl_eq ? a0).
  93   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ??? a1 ? p0 = x1 → Type.
  94   ∀a2:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).
  95   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ??? a1 ? p0 = x1.
  96       ∀x2:T2 x0 p0 x1 p1.R2 T0 a0 T1 a1 T2 a2 ? p0 ? p1 = x2→ Type.
  97   ∀b0:T0.
  98   ∀e0:a0 = b0.
  99   ∀b1: T1 b0 e0.
 100   ∀e1:R1 ??? a1 ? e0 = b1.
 101   ∀b2: T2 b0 e0 b1 e1.
 102   ∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
 103   ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).T3 b0 e0 b1 e1 b2 e2.
 104 intros 12;intros 2 (e2 H);
 105 apply (eq_rect' ????? e2);
 106 apply (R2 ?? ? ???? e0 ? e1);
 107 simplify;assumption;
 108 qed.
 109
 110 (*let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
 111   match n with
 112   [ O ⇒ Type
 113   | S p ⇒ match l2 with
 114     [ nil ⇒ Type (* dummy *)
 115     | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]].
 116
 117 lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type.
 118 intro;
 119 elim l
 120 [apply i
 121 |simplify in i;apply F;apply i;apply a]
 122 qed.
 123
 124 definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝
 125   λl,T.app_type_list l T :: l.
 126
 127 let rec build_dep_type n T acc ≝
 128   match n with
 129   [ O ⇒ acc
 130   | S p ⇒
 131 Type → list Type → Type.
 132   λta,l.match l *)
 133
 134 inductive II : nat → Type ≝
 135 | k1 : ∀n.II n
 136 | k2 : ∀n.II n
 137 | k3 : ∀n,m. II n → II m → II O.
 138
 139 inductive JJ : nat → Type ≝
 140 | h1 : JJ O
 141 | h2 : JJ (S O)
 142 | h3 : ∀n,m. JJ n → JJ m → JJ O.
 143
 144 (*
 145
 146 lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True.
 147 intro;
 148 letin f ≝ (λx.S (S x));
 149 cut (∃a,b.S a = f b);
 150 [decompose;cut (S (S a) = S (f a1))
 151  [|clear H;destruct;
 152 cut (∀→ True)
 153 [elim Hcut;
 154 qed.
 155 *)
 156
 157 definition IId : ∀n,m.II m → II n → Type ≝
 158  λa,b,x,y.match x with
 159  [ k1 n ⇒ match y with
 160    [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P
 161    | k2 n' ⇒ ∀P:Type.P
 162    | k3 m n p' q' ⇒ ∀P:Type.P ]
 163  | k2 n ⇒ match y with
 164    [ k1 n' ⇒ ∀P:Type.P
 165    | k2 n' ⇒ ∀P:Type.(n = n' → P) → P
 166    | k3 m' n' p' q' ⇒ ∀P:Type.P ]
 167  | k3 m n p q ⇒ match y with
 168    [ k1 n' ⇒ ∀P:Type.P
 169    | k2 n' ⇒ ∀P:Type.P
 170    | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p'
 171      → (eq_rect ??? q ? e2) = q' → P) → P ]].
 172
 173 lemma IInc : ∀n,x,y.x = y → IId n n x y.
 174 intros;rewrite > H;elim y;simplify;intros;
 175 [apply f;reflexivity
 176 |apply f;reflexivity
 177 |apply f;reflexivity]
 178 qed.
 179
 180 axiom daemon:False.
 181
 182 lemma IIconflict: ∀c,d.
 183   k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
 184 intros;apply (IInc ??? H);clear H;intro;
 185 apply (eq_rect' ?? (λx.λp.∀e2:x=c.eq_rect ℕ c II (k1 c) x p=k2 x→eq_rect nat x II (k2 x) c e2 = k1 c → False) ?? e1);
 186 simplify;intros;apply (IInc ??? H);
 187
 188 inductive I1 : nat → Type ≝
 189 | kI1 : ∀n.I1 n.
 190
 191 inductive I2 : ∀n:nat.I1 n → Type ≝
 192 | kI2 : ∀n,i.I2 n i.
 193
 194 inductive I3 : Type ≝
 195 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
 196
 197 definition I3d: I3 → I3 → Type ≝
 198 λx,y.match x with
 199 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
 200   [ kI3 u1 u2 u3 ⇒ ∀P:Type.
 201     (∀e1: t1 = u1.
 202      ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
 203      ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) ? e1 ? e2 t3 = u3.P) → P]].
 204
 205 lemma I3nc : ∀a,b.a = b → I3d a b.
 206 intros;rewrite > H;elim b;simplify;intros;apply f;reflexivity;
 207 qed.
 208
 209 (*lemma R1_r : ΠA:Type.Πx:A.ΠP:Πy:A.y=x→Type.P x (refl_eq A x)→Πy:A.Πp:y=x.P y p.
 210 intros;lapply (eq_rect' A x P p y (sym_eq A y x p1));
 211 generalize in match Hletin;
 212 cut (∀p1:y = x.sym_eq ??? (sym_eq ??? p1) = p1)
 213 [rewrite > Hcut;intro;assumption
 214 |intro;apply (eq_rect' ????? p2);simplify;reflexivity]
 215 qed.
 216
 217 definition R2_r :
 218   ∀T0:Type.
 219   ∀a0:T0.
 220   ∀T1:∀x0:T0. x0=a0 → Type.
 221   ∀a1:T1 a0 (refl_eq ? a0).
 222   ∀T2:∀x0:T0. ∀p0:x0=a0. ∀x1:T1 x0 p0. x1 = R1_r ??? a1 ? p0 → Type.
 223   ∀b0:T0.
 224   ∀e0:b0 = a0.
 225   ∀b1: T1 b0 e0.
 226   ∀e1:b1 = R1_r ??? a1 ? e0.
 227   ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
 228 intros 8;intros 2 (e1 H);
 229 apply (R1_r ????? e1);
 230 apply (R1_r ?? ? ?? e0);
 231 simplify;assumption;
 232 qed.*)
 233
 234 definition I3prova : ∀a,b,c,d,e,f.kI3 a b c = kI3 d e f → ∃P.P d e f.
 235 intros;apply (I3nc ?? H);clear H;
 236 simplify;intro;
 237 generalize in match f as f;generalize in match e as e;
 238 generalize in match c as c;generalize in match b as b;
 239 clear f e c b;
 240 apply (R1 ????? e1);intros 5;simplify in e2;
 241 generalize in match f as f;generalize in match c as c;
 242 clear f c;
 243 apply (R1 ????? e2);intros;simplify in H;
 244 elim daemon;
 245 qed.
 246
 247
 248 definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
 249  λa,b,c,d,x,y.match x with
 250  [ c1 n ⇒ match y with
 251    [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P
 252    | c2 n' ⇒ ∀P:Type.P
 253    | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
 254  | c2 n ⇒ match y with
 255    [ c1 n' ⇒ ∀P:Type.P
 256    | c2 n' ⇒ ∀P:Type.(n = n' → P) → P
 257    | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
 258  | c3 m n p q h i ⇒ match y with
 259    [ c1 n' ⇒ ∀P:Type.P
 260    | c2 n' ⇒ ∀P:Type.P
 261    | c3 m' n' p' q' h' i' ⇒
 262      ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'.
 263      (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h'
 264      → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]].
 265
 266 lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
 267 intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;
 268 qed.
 269