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