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 (T0 a0 T1 a1 T2 a2);
  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   ∀a3:T3 a0 (refl_eq ? a0) a1 (refl_eq ? a1) a2 (refl_eq ? a2).
  98   ∀b0:T0.
  99   ∀e0:a0 = b0.
 100   ∀b1: T1 b0 e0.
 101   ∀e1:R1 ??? a1 ? e0 = b1.
 102   ∀b2: T2 b0 e0 b1 e1.
 103   ∀e2:R2 T0 a0 T1 a1 T2 a2 ? e0 ? e1 = b2.
 104   T3 b0 e0 b1 e1 b2 e2.
 105 intros (T0 a0 T1 a1 T2 a2 T3 a3);
 106 apply (eq_rect' ????? e2);
 107 apply (R2 ?? ? ???? e0 ? e1);
 108 simplify;assumption;
 109 qed.
 110
 111 (*let rec iter_type n (l1 : lista dei nomi fin qui creati) (l2: lista dei tipi dipendenti da applicare) ≝
 112   match n with
 113   [ O ⇒ Type
 114   | S p ⇒ match l2 with
 115     [ nil ⇒ Type (* dummy *)
 116     | cons T tl ⇒ ∀t:app_type_list l1 T.iter_type p (l1@[t]) tl ]].
 117
 118 lemma app_type_list : ∀l:list Type.∀T:iter_type l.Type.
 119 intro;
 120 elim l
 121 [apply i
 122 |simplify in i;apply F;apply i;apply a]
 123 qed.
 124
 125 definition type_list_cons : ∀l:list Type.iter_type l → list Type ≝
 126   λl,T.app_type_list l T :: l.
 127
 128 let rec build_dep_type n T acc ≝
 129   match n with
 130   [ O ⇒ acc
 131   | S p ⇒
 132 Type → list Type → Type.
 133   λta,l.match l *)
 134
 135 inductive II : nat → Type ≝
 136 | k1 : ∀n.II n
 137 | k2 : ∀n.II n
 138 | k3 : ∀n,m. II n → II m → II O.
 139
 140 inductive JJ : nat → Type ≝
 141 | h1 : JJ O
 142 | h2 : JJ (S O)
 143 | h3 : ∀n,m. JJ n → JJ m → JJ O.
 144
 145 (*
 146
 147 lemma test: h3 ?? h1 h2 = h3 ?? h2 h1 → True.
 148 intro;
 149 letin f ≝ (λx.S (S x));
 150 cut (∃a,b.S a = f b);
 151 [decompose;cut (S (S a) = S (f a1))
 152  [|clear H;destruct;
 153 cut (∀→ True)
 154 [elim Hcut;
 155 qed.
 156 *)
 157
 158 definition IId : ∀n,m.II m → II n → Type ≝
 159  λa,b,x,y.match x with
 160  [ k1 n ⇒ match y with
 161    [ k1 n' ⇒ ∀P:Type.(n = n' → P) → P
 162    | k2 n' ⇒ ∀P:Type.P
 163    | k3 m n p' q' ⇒ ∀P:Type.P ]
 164  | k2 n ⇒ match y with
 165    [ k1 n' ⇒ ∀P:Type.P
 166    | k2 n' ⇒ ∀P:Type.(n = n' → P) → P
 167    | k3 m' n' p' q' ⇒ ∀P:Type.P ]
 168  | k3 m n p q ⇒ match y with
 169    [ k1 n' ⇒ ∀P:Type.P
 170    | k2 n' ⇒ ∀P:Type.P
 171    | k3 m' n' p' q' ⇒ ∀P:Type.(∀e1:m = m'.∀e2:n = n'. (eq_rect ??? p ? e1) = p'
 172      → (eq_rect ??? q ? e2) = q' → P) → P ]].
 173
 174 lemma IInc : ∀n,x,y.x = y → IId n n x y.
 175 intros;rewrite > H;elim y;simplify;intros;
 176 [apply f;reflexivity
 177 |apply f;reflexivity
 178 |apply f;reflexivity]
 179 qed.
 180
 181 axiom daemon:False.
 182
 183 lemma IIconflict: ∀c,d.
 184   k3 c d (k1 c) (k2 d) = k3 d c (k2 d) (k1 c) → False.
 185 intros;apply (IInc ??? H);clear H;intro;
 186 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);
 187 simplify;intros;apply (IInc ??? H);
 188
 189 inductive I1 : nat → Type ≝
 190 | kI1 : ∀n.I1 n.
 191
 192 inductive I2 : ∀n:nat.I1 n → Type ≝
 193 | kI2 : ∀n,i.I2 n i.
 194
 195 inductive I3 : Type ≝
 196 | kI3 : ∀x1:nat.∀x2:I1 x1.∀x3:I2 x1 x2.I3.
 197
 198 (* lemma idfof : (∀t1,t2,t3,u1,u2,u3.((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.
 199        λy3:I2 y1 y2.λp3:R2 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 (λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1 =y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t3 y1 p1 y2 p2 =y3.
 200                     kI3 y1 y2 y3 =kI3 u1 u2 u3)
 201 t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)
 202    t3 (refl_eq ((λy1:ℕ.λp1:t1=y1.λy2:I1 y1.λp2:R1 ℕ t1 (λy1:ℕ.λp1:t1=y1.I1 y1) t2 y1 p1 =y2.I2 y1 y2) t1 (refl_eq ℕ t1) t2 (refl_eq ((λy1:ℕ.λp1:t1=y1.I1 y1) t1 (refl_eq ℕ t1)) t2)) t3)
 203    )
 204     → True).
 205 simplify; *)
 206
 207 definition I3d : ∀x,y:I3.x = y → Type ≝
 208 λx,y.match x return (λx:I3.x = y → Type) with
 209 [ kI3 x1 x2 x3 ⇒ match y return (λy:I3.kI3 x1 x2 x3 = y → Type) with
 210   [ kI3 y1 y2 y3 ⇒
 211     λe:kI3 x1 x2 x3 = kI3 y1 y2 y3.
 212        ∀P:Prop.(∀e1: x1 = y1.
 213                 ∀e2: R1 ?? (λz1,p1.I1 z1) ?? e1 = y2.
 214                 ∀e3: R2 ???? (λz1,p1,z2,p2.I2 z1 z2) x3 ? e1 ? e2 = y3.
 215                 R3 ??????
 216                 (λz1,p1,z2,p2,z3,p3.
 217                   eq ? (kI3 z1 z2 z3) (kI3 y1 y2 y3)) e y1 e1 y2 e2 y3 e3
 218                 = refl_eq ? (kI3 y1 y2 y3)
 219                 → P) → P]].
 220
 221 definition I3d : ∀x,y:I3.x=y → Type.
 222 intros 2;cases x;cases y;intro;
 223 apply (∀P:Prop.(∀e1: x1 = x3.
 224                 ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = x4.
 225                 ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) i ? e1 ? e2 = i1.
 226                 R3 ??????
 227                 (λy1,p1,y2,p2,y3,p3.
 228                   eq ? (kI3 y1 y2 y3) (kI3 x3 x4 i1)) H x3 e1 x4 e2 i1 e3
 229                 = refl_eq ? (kI3 x3 x4 i1)
 230                 → P) → P);
 231 qed.
 232
 233 (* definition I3d : ∀x,y:nat. x = y → Type ≝
 234 λx,y.
 235 match x
 236  return (λx.x = y → Type)
 237  with
 238 [ O ⇒ match y return (λy.O = y → Type) with
 239   [ O ⇒ λe:O = O.∀P.P → P
 240   | S q ⇒ λe: O = S q. ∀P.P]
 241 | S p ⇒ match y return (λy.S p = y → Type) with
 242   [ O ⇒ λe:S p = O.∀P.P
 243   | S q ⇒ λe: S p = S q. ∀P.(p = q → P) → P]].
 244
 245 definition I3d:
 246   ∀x,y:I3. x = y → Type
 247   ≝
 248 λx,y.
 249 match x with
 250 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
 251   [ kI3 u1 u2 u3 ⇒ λe:kI3 t1 t2 t3 = kI3 u1 u2 u3.∀P:Type.
 252     (∀e1: t1 = u1.
 253      ∀e2: R1 nat t1 (λy1:nat.λp1:y1 = u1.I1 y1) t2 ? e1 = u2.
 254      ∀e3: R2 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3.
 255      (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
 256      R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3
 257         (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) e u1 e1 u2 e2 u3 e3 = refl_eq I3 (kI3 u1 u2 u3)
 258      → P)
 259     → P]].
 260
 261 definition I3d:
 262   ∀x,y:I3.
 263     (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
 264       match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]) → Type
 265   ≝
 266 λx,y.λe:
 267    (∀x,y.match x with [ kI3 t1 t2 t3 ⇒
 268       match y with [ kI3 u1 u2 u3 ⇒ kI3 t1 t2 t3 = kI3 u1 u2 u3]]).
 269 match x with
 270 [ kI3 t1 t2 (t3:I2 t1 t2) ⇒ match y with
 271   [ kI3 u1 u2 u3 ⇒ ∀P:Type.
 272     (∀e1: t1 = u1.
 273      ∀e2: R1 ?? (λy1,p1.I1 y1) ?? e1 = u2.
 274      ∀e3: R2 ???? (λy1,p1,y2,p2.I2 y1 y2) t3 ? e1 ? e2 = u3.
 275      (* ∀e:  kI3 t1 t2 t3 = kI3 u1 u2 u3.*)
 276      R3 nat t1 (λy1,p1.I1 y1) t2 (λy1,p1,y2,p2.I2 y1 y2) t3
 277         (λy1,p1,y2,p2,y3,p3.eq I3 (kI3 y1 y2 y3) (kI3 u1 u2 u3)) (e (kI3 t1 t2 t3) (kI3 u1 u2 u3)) u1 e1 u2 e2 u3 e3 = refl_eq ? (kI3 u1 u2 u3)
 278      → P)
 279     → P]].*)
 280
 281 lemma I3nc : ∀a,b.∀e:a = b. I3d a b e.
 282 intros;apply (R1 ????? e);elim a;whd;intros;apply H;reflexivity;
 283 qed.
 284
 285 (*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.
 286 intros;lapply (eq_rect' A x P p y (sym_eq A y x p1));
 287 generalize in match Hletin;
 288 cut (∀p1:y = x.sym_eq ??? (sym_eq ??? p1) = p1)
 289 [rewrite > Hcut;intro;assumption
 290 |intro;apply (eq_rect' ????? p2);simplify;reflexivity]
 291 qed.
 292
 293 definition R2_r :
 294   ∀T0:Type.
 295   ∀a0:T0.
 296   ∀T1:∀x0:T0. x0=a0 → Type.
 297   ∀a1:T1 a0 (refl_eq ? a0).
 298   ∀T2:∀x0:T0. ∀p0:x0=a0. ∀x1:T1 x0 p0. x1 = R1_r ??? a1 ? p0 → Type.
 299   ∀b0:T0.
 300   ∀e0:b0 = a0.
 301   ∀b1: T1 b0 e0.
 302   ∀e1:b1 = R1_r ??? a1 ? e0.
 303   ∀so:T2 a0 (refl_eq ? a0) a1 (refl_eq ? a1).T2 b0 e0 b1 e1.
 304 intros 8;intros 2 (e1 H);
 305 apply (R1_r ????? e1);
 306 apply (R1_r ?? ? ?? e0);
 307 simplify;assumption;
 308 qed.*)
 309
 310 definition I3prova : ∀a,b,c,d,e,f.∀Heq:kI3 a b c = kI3 d e f.
 311   ∀P:? → ? → ? → ? → Prop.
 312   P d e f Heq →
 313   P a b c (refl_eq ??).
 314 intros;apply (I3nc ?? Heq);
 315 simplify;intro;
 316 generalize in match H as H;generalize in match Heq as Heq;
 317 generalize in match f as f;generalize in match e as e;
 318 clear H Heq f e;
 319 apply (R1 ????? e1);intros 5;simplify in e2;
 320 generalize in match H as H;generalize in match Heq as Heq;
 321 generalize in match f as f;
 322 clear H Heq f;
 323 apply (R1 ????? e2);intros 4;simplify in e3;
 324 generalize in match H as H;generalize in match Heq as Heq;
 325 clear H Heq;
 326 apply (R1 ????? e3);intros;simplify in H1;
 327 apply (R1 ????? H1);
 328 assumption;
 329 qed.
 330
 331
 332 definition KKd : ∀m,n,p,q.KK m n → KK p q → Type ≝
 333  λa,b,c,d,x,y.match x with
 334  [ c1 n ⇒ match y with
 335    [ c1 n' ⇒ ∀P:Type.(n = n' → P) → P
 336    | c2 n' ⇒ ∀P:Type.P
 337    | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
 338  | c2 n ⇒ match y with
 339    [ c1 n' ⇒ ∀P:Type.P
 340    | c2 n' ⇒ ∀P:Type.(n = n' → P) → P
 341    | c3 m' n' p' q' h' i' ⇒ ∀P:Type.P ]
 342  | c3 m n p q h i ⇒ match y with
 343    [ c1 n' ⇒ ∀P:Type.P
 344    | c2 n' ⇒ ∀P:Type.P
 345    | c3 m' n' p' q' h' i' ⇒
 346      ∀P:Type.(∀e1:m = m'.∀e2:n = n'. ∀e3:p = p'. ∀e4:q = q'.
 347      (eq_rect ?? (λm.KK m n') (eq_rect ?? (λn.KK m n) h n' e2) m' e1) = h'
 348      → (eq_rect ?? (λp.KK p q') (eq_rect ?? (λq.KK p q) i ? e4) ? e3) = i' → P) → P ]].
 349
 350 lemma KKnc : ∀a,b,e,f.e = f → KKd a b a b e f.
 351 intros;rewrite > H;elim f;simplify;intros;apply f1;reflexivity;
 352 qed.
 353