matita/matita/lib/finite_lambda/finite_lambda_deep.ma

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department of the University of Bologna, Italy.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "basics/finset.ma".
  13 include "basics/star.ma".
  14
  15
  16 inductive FType (O:Type[0]): Type[0] ≝
  17   | atom : O → FType O
  18   | arrow : FType O → FType O → FType O.
  19
  20 inductive T (O:Type[0]) (D:O → FinSet): Type[0] ≝
  21   | Val: ∀o:O.carr (D o) → T O D        (* a value in a finset *)
  22   | Rel: nat → T O D                    (* DB index, base is 0 *)
  23   | App: T O D → T O D → T O D          (* function, argument *)
  24   | Lambda: FType O → T O D → T O D     (* type, body *)
  25   | Vec: FType O → list (T O D) → T O D (* type, body *)
  26 .
  27
  28 let rec FinSet_of_FType O (D:O→FinSet) (ty:FType O) on ty : FinSet ≝
  29   match ty with
  30   [atom o ⇒ D o
  31   |arrow ty1 ty2 ⇒ FinFun (FinSet_of_FType O D ty1) (FinSet_of_FType O D ty2)
  32   ].
  33
  34 (* size *)
  35
  36 let rec size O D (M:T O D) on M ≝
  37 match M with
  38   [Val o a ⇒ 1
  39   |Rel n ⇒ 1
  40   |App P Q ⇒ size O D P + size O D Q + 1
  41   |Lambda Ty P ⇒ size O D P + 1
  42   |Vec Ty v ⇒ foldr ?? (λx,a. size O D x + a) 0 v +1
  43   ]
  44 .
  45
  46 (* axiom pos_size: ∀M. 1 ≤ size M. *)
  47
  48 theorem Telim_size: ∀O,D.∀P: T O D → Prop.
  49  (∀M. (∀N. size O D N < size O D M → P N) → P M) → ∀M. P M.
  50 #O #D #P #H #M (cut (∀p,N. size O D N = p → P N))
  51   [2: /2/]
  52 #p @(nat_elim1 p) #m #H1 #N #sizeN @H #N0 #Hlt @(H1 (size O D N0)) //
  53 qed.
  54
  55 lemma T_elim:
  56   ∀O: Type[0].∀D:O→FinSet.∀P:T O D→Prop.
  57   (∀o:O.∀x:D o.P (Val O D o x)) →
  58   (∀n:ℕ.P(Rel O D n)) →
  59   (∀m,n:T O D.P m→P n→P (App O D m n)) →
  60   (∀Ty:FType O.∀m:T O D.P m→P(Lambda O D Ty m)) →
  61   (∀Ty:FType O.∀v:list (T O D).
  62      (∀x:T O D. mem ? x v → P x) → P(Vec O D Ty v)) →
  63   ∀x:T O D.P x.
  64 #O #D #P #Hval #Hrel #Happ #Hlam #Hvec @Telim_size #x cases x //
  65   [ (* app *) #m #n #Hind @Happ @Hind // /2 by le_minus_to_plus/
  66   | (* lam *) #ty #m #Hind @Hlam @Hind normalize //
  67   | (* vec *) #ty #v #Hind @Hvec #x lapply Hind elim v
  68     [#Hind normalize *
  69     |#hd #tl #Hind1 #Hind2 *
  70       [#Hx >Hx @Hind2 normalize //
  71       |@Hind1 #N #H @Hind2 @(lt_to_le_to_lt … H) normalize //
  72       ]
  73     ]
  74   ]
  75 qed.
  76
  77
  78 (* arguments: k is the nesting depth (starts from 0), p is the lift *)
  79 let rec lift O D t k p on t ≝
  80   match t with
  81     [ Val o a ⇒ Val O D o a
  82     | Rel n ⇒ if (leb k n) then Rel O D (n+p) else Rel O D n
  83     | App m n ⇒ App O D (lift O D m k p) (lift O D n k p)
  84     | Lambda Ty n ⇒ Lambda O D Ty (lift O D n (S k) p)
  85     | Vec Ty v ⇒ Vec O D Ty (map ?? (λx. lift O D x k p) v)
  86     ].
  87
  88 notation "↑ ^ n ( M )" non associative with precedence 40 for @{'Lift 0 $n $M}.
  89 notation "↑ _ k ^ n ( M )" non associative with precedence 40 for @{'Lift $n $k $M}.
  90
  91 interpretation "Lift" 'Lift n k M = (lift ?? M k n).
  92
  93 let rec subst O D t k s on t ≝
  94   match t with
  95     [ Val o a ⇒ Val O D o a
  96     | Rel n ⇒ if (leb k n) then
  97         (if (eqb k n) then lift O D s 0 n else Rel O D (n-1))
  98         else(Rel O D n)
  99     | App m n ⇒ App O D (subst O D m k s) (subst O D n k s)
 100     | Lambda T n ⇒ Lambda O D T (subst O D n (S k) s)
 101     | Vec T v ⇒ Vec O D T (map ?? (λx. subst O D x k s) v)
 102     ].
 103
 104 (* notation "hvbox(M break [ k ≝ N ])"
 105    non associative with precedence 90
 106    for @{'Subst1 $M $k $N}. *)
 107
 108 interpretation "Subst" 'Subst1 M k N = (subst M k N).
 109
 110 (* closed terms ????
 111 let rec closed_k O D (t: T O D) k on t ≝
 112   match t with
 113     [ Val o a ⇒ True
 114     | Rel n ⇒ n < k
 115     | App m n ⇒ (closed_k O D m k) ∧ (closed_k O D n k)
 116     | Lambda T n ⇒ closed_k O D n (k+1)
 117     | Vec T v ⇒ closed_list O D v k
 118     ]
 119
 120 and closed_list O D (l: list (T O D)) k on l ≝
 121   match l with
 122     [ nil ⇒ True
 123     | cons hd tl ⇒ closed_k O D hd k ∧ closed_list O D tl k
 124     ]
 125 . *)
 126
 127 inductive is_closed (O:Type[0]) (D:O→FinSet): nat → T O D → Prop ≝
 128 | cval : ∀k,o,a.is_closed O D k (Val O D o a)
 129 | cval : ∀k,n. n < k → is_closed O D k (Rel O D n)
 130 | capp : ∀k,n,m. is_closed O D k m → is_closed O D k n →
 131            is_closed O D k (App O D m n)
 132 | clam : ∀T,k,m. is_closed O D (k+1) m → is_closed O D k (Lambda O D T m)
 133 | cvec:  ∀T,k,v. (∀m. mem ? m v → is_closed O D k m) →
 134            is_closed O D k (Vec O D T v).
 135
 136 lemma is_closed_rel: ∀O,D,n,k.
 137   is_closed O D k (Rel O D n) → n < k.
 138 #O #D #n #k #H inversion H
 139   [#k0 #o #a #eqk #H destruct
 140   |#k0 #n0 #ltn0 #eqk #H destruct //
 141   |#k0 #M #N #_ #_ #_ #H destruct
 142   |#T #k0 #M #_ #_ #H destruct
 143   |#T #k0 #v #_ #_ #H destruct
 144   ]
 145 qed.
 146
 147
 148 (*** properties of lift and subst ***)
 149
 150 lemma lift_0: ∀O,D.∀t:T O D.∀k. lift O D t k 0 = t.
 151 #O #D #t @(T_elim … t) normalize //
 152   [#n #k cases (leb k n) normalize //
 153   |#o #v #Hind #k @eq_f lapply Hind -Hind elim v //
 154    #hd #tl #Hind #Hind1 normalize @eq_f2
 155     [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
 156   ]
 157 qed.
 158
 159 axiom lift_closed: ∀O,D.∀t:T O D.∀k,p.
 160   is_closed O D 0 t → lift O D t k p = t.
 161 (*
 162 #O #D #t @(T_elim … t) normalize //
 163   [#n #k normalize //
 164   |#o #v #Hind #k @eq_f lapply Hind -Hind elim v //
 165    #hd #tl #Hind #Hind1 normalize @eq_f2
 166     [@Hind1 %1 //|@Hind #x #Hx @Hind1 %2 //]
 167   ]
 168 qed. *)
 169
 170 let rec to_T O D ty on ty: FinSet_of_FType O D ty → T O D ≝
 171   match ty return (λty.FinSet_of_FType O D ty → T O D) with
 172   [atom o ⇒ λa.Val O D o a
 173   |arrow ty1 ty2 ⇒ λa:FinFun ??.Vec O D ty1
 174     (map ((FinSet_of_FType O D ty1)×(FinSet_of_FType O D ty2))
 175      (T O D) (λp.to_T O D ty2 (snd … p)) (pi1 … a))
 176   ]
 177 .
 178
 179 axiom inj_to_T: ∀O,D,ty,a1,a2. to_T O D ty a1 = to_T O D ty a2 → a1 = a2.
 180
 181 let rec assoc (A:FinSet) (B:Type[0]) (a:A) l1 l2 on l1 : option B ≝
 182   match l1 with
 183   [ nil ⇒  None ?
 184   | cons hd1 tl1 ⇒ match l2 with
 185     [ nil ⇒ None ?
 186     | cons hd2 tl2 ⇒ if a==hd1 then Some ? hd2 else assoc A B a tl1 tl2
 187     ]
 188   ].
 189
 190 lemma same_assoc: ∀A,B,a,l1,v1,v2,N,N1.
 191   assoc A B a l1 (v1@N::v2) = Some ? N ∧ assoc A B a l1 (v1@N1::v2) = Some ? N1
 192    ∨ assoc A B a l1 (v1@N::v2) = assoc A B a l1 (v1@N1::v2).
 193 #A #B #a #l1 #v1 #v2 #N #N1 lapply v1 -v1 elim l1
 194   [#v1 %2 // |#hd #tl #Hind * normalize cases (a==hd) normalize /3/]
 195 qed.
 196
 197 lemma assoc_to_mem: ∀A,B,a,l1,l2,b.
 198   assoc A B a l1 l2 = Some ? b → mem ? b l2.
 199 #A #B #a #l1 elim l1
 200   [#l2 #b normalize #H destruct
 201   |#hd1 #tl1 #Hind *
 202     [#b normalize #H destruct
 203     |#hd2 #tl2 #b normalize cases (a==hd1) normalize
 204       [#H %1 destruct //|#H %2 @Hind @H]
 205     ]
 206   ]
 207 qed.
 208
 209 inductive red (O:Type[0]) (D:O→FinSet) : T O D  →T O D → Prop ≝
 210   | (* we only allow beta on closed arguments *)
 211     rbeta: ∀P,M,N. is_closed O D 0 N →
 212       red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
 213   | riota: ∀ty,v,a,M.
 214       assoc (FinSet_of_FType O D ty) ? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
 215       red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
 216   | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
 217   | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
 218   | rlam: ∀ty,N,N1. red O D N N1 → red O D (Lambda O D ty N) (Lambda O D ty N1)
 219   | rmem: ∀ty,M. red O D (Lambda O D ty M)
 220       (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 221       (enum (FinSet_of_FType O D ty))))
 222   | rvec: ∀ty,N,N1,v,v1. red O D N N1 →
 223       red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
 224
 225 (* some inversion cases *)
 226 lemma red_vec: ∀O,D,ty,v,M.
 227   red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
 228       red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
 229 #O #D #ty #v #M #Hred inversion Hred
 230   [#ty1 #M0 #N #Hc #H destruct
 231   |#ty1 #v1 #a #M0 #_ #H destruct
 232   |#M0 #M1 #N #_ #_ #H destruct
 233   |#M0 #M1 #N #_ #_ #H destruct
 234   |#ty1 #M #M1 #_ #_ #H destruct
 235   |#ty1 #M0 #H destruct
 236   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
 237   ]
 238 qed.
 239
 240 lemma red_lambda: ∀O,D,ty,M,N.
 241   red O D (Lambda O D ty M) N →
 242       (∃M1. red O D M M1 ∧ N = (Lambda O D ty M1)) ∨
 243       N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 244       (enum (FinSet_of_FType O D ty))).
 245 #O #D #ty #M #N #Hred inversion Hred
 246   [#ty1 #M0 #N #Hc #H destruct
 247   |#ty1 #v1 #a #M0 #_ #H destruct
 248   |#M0 #M1 #N #_ #_ #H destruct
 249   |#M0 #M1 #N #_ #_ #H destruct
 250   |#ty1 #P #P1 #redP #_ #H #H1 destruct %1 %{P1} % //
 251   |#ty1 #M0 #H destruct #_ %2 //
 252   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 253   ]
 254 qed.
 255
 256 lemma red_val: ∀O,D,ty,a,N.
 257   red O D (Val O D ty a) N → False.
 258 #O #D #ty #M #N #Hred inversion Hred
 259   [#ty1 #M0 #N #Hc #H destruct
 260   |#ty1 #v1 #a #M0 #_ #H destruct
 261   |#M0 #M1 #N #_ #_ #H destruct
 262   |#M0 #M1 #N #_ #_ #H destruct
 263   |#ty1 #N1 #N2 #_ #_ #H destruct
 264   |#ty1 #M0 #H destruct #_
 265   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 266   ]
 267 qed.
 268
 269 lemma red_rel: ∀O,D,n,N.
 270   red O D (Rel O D n) N → False.
 271 #O #D #n #N #Hred inversion Hred
 272   [#ty1 #M0 #N #Hc #H destruct
 273   |#ty1 #v1 #a #M0 #_ #H destruct
 274   |#M0 #M1 #N #_ #_ #H destruct
 275   |#M0 #M1 #N #_ #_ #H destruct
 276   |#ty1 #N1 #N2 #_ #_ #H destruct
 277   |#ty1 #M0 #H destruct #_
 278   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 279   ]
 280 qed.
 281
 282 lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 →
 283   star ? (red O D) (App O D M N) (App O D M1 N).
 284 #O #D #M #N #N1 #H elim H //
 285 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
 286 qed.
 287
 288 lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 →
 289   star ? (red O D) (App O D M N) (App O D M N1).
 290 #O #D #M #N #N1 #H elim H //
 291 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
 292 qed.
 293
 294 lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 →
 295   star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
 296 #O #D #ty #N #N1 #v1 #v2 #H elim H //
 297 #P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
 298 qed.
 299
 300 lemma star_red_vec1: ∀O,D,ty,v1,v2,v. |v1| = |v2| →
 301   (∀n,M. star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
 302   star ? (red O D) (Vec O D ty (v@v1)) (Vec O D ty (v@v2)).
 303 #O #D #ty #v1 elim v1
 304   [#v2 #v normalize #Hv2 >(lenght_to_nil … (sym_eq … Hv2)) normalize //
 305   |#N1 #tl1 #Hind * [normalize #v #H destruct] #N2 #tl2 #v normalize #HS
 306    #H @(trans_star … (Vec O D ty (v@N2::tl1)))
 307     [@star_red_vec @(H 0 N1)
 308     |>append_cons >(append_cons ??? tl2) @(Hind… (injective_S … HS))
 309      #n #M @(H (S n))
 310     ]
 311   ]
 312 qed.
 313
 314 lemma star_red_vec2: ∀O,D,ty,v1,v2. |v1| = |v2| →
 315   (∀n,M. star ? (red O D) (nth n ? v1 M) (nth n ? v2 M)) →
 316   star ? (red O D) (Vec O D ty v1) (Vec O D ty v2).
 317 #O #D #ty #v1 #v2 @(star_red_vec1 … [ ])
 318 qed.
 319
 320 lemma star_red_lambda: ∀O,D,ty,N,N1. star ? (red O D) N N1 →
 321   star ? (red O D) (Lambda O D ty N) (Lambda O D ty N1).
 322 #O #D #ty #N #N1 #H elim H //
 323 #P #Q #Hind #HPQ #Hlam %1[|@Hlam] @rlam @HPQ
 324 qed.
 325
 326 axiom red_subst : ∀O,D,M,N,N1,i.
 327   red O D N N1 → red O D (subst O D M i N) (subst O D M i N1).
 328
 329 axiom red_star_subst : ∀O,D,M,N,N1,i.
 330   star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
 331
 332 axiom red_star_subst2 : ∀O,D,M,M1,N,i.
 333   star ? (red O D) M M1 → star ? (red O D) (subst O D M i N) (subst O D M1 i N).
 334
 335 axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
 336   ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
 337
 338 axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
 339
 340 axiom red_closed: ∀O,D,M,M1.
 341   is_closed O D 0 M → red O D M M1 → is_closed O D 0 M1.
 342
 343 lemma critical: ∀O,D,ty,M,N.
 344   ∃M3:T O D
 345   .star (T O D) (red O D) (subst O D M 0 N) M3
 346    ∧star (T O D) (red O D)
 347     (App O D
 348      (Vec O D ty
 349       (map (FinSet_of_FType O D ty) (T O D)
 350        (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
 351        (enum (FinSet_of_FType O D ty)))) N) M3.
 352 #O #D #ty #M #N
 353 lapply (canonical_to_T O D N ty) * #a #Ha
 354 %{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
 355 %[@red_star_subst @Ha
 356  |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
 357   lapply (enum_complete (FinSet_of_FType O D ty) a)
 358   elim (enum (FinSet_of_FType O D ty))
 359    [normalize #H1 destruct (H1)
 360    |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
 361      [normalize >Hcase >(\P Hcase) //
 362      |normalize cases (true_or_false (a==hd)) #Hcase1
 363        [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
 364      ]
 365    ]
 366  ]
 367 qed.
 368
 369 lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
 370   red O D (Vec O D ty v) M →
 371   red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
 372   assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
 373     =Some (T O D) M2 →
 374   ∃M3:T O D
 375   .star (T O D) (red O D) M2 M3
 376    ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
 377 #O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
 378 * #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
 379 cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
 380   [* >Ha -Ha #H1 destruct (H1) #Ha
 381    %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
 382   |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
 383   ]
 384 qed.
 385
 386 lemma nth_to_default: ∀A,l,n,d.
 387   |l| ≤ n → nth n A l d = d.
 388 #A #l elim l [//] #a #tl #Hind #n cases n
 389   [#d normalize #H @False_ind @(absurd … H) @lt_to_not_le //
 390   |#m #d normalize #H @Hind @le_S_S_to_le @H
 391   ]
 392 qed.
 393
 394 lemma nth_map: ∀A,B,l,f,n,d1,d2.
 395   n < |l| → nth n B (map … f l) d1 = f (nth n A l d2).
 396 #n #B #l #f elim l
 397   [#m #d1 #d2 normalize #H @False_ind @(absurd … H) @lt_to_not_le //
 398   |#a #tl #Hind #m #d1 #d2 cases m normalize //
 399    #m1 #H @Hind @le_S_S_to_le @H
 400   ]
 401 qed.
 402
 403 lemma critical3: ∀O,D,ty,M1,M2. red O D M1 M2 →
 404   ∃M3:T O D.star (T O D) (red O D) (Lambda O D ty M2) M3
 405    ∧star (T O D) (red O D)
 406     (Vec O D ty
 407      (map (FinSet_of_FType O D ty) (T O D)
 408       (λa:FinSet_of_FType O D ty.subst O D M1 0 (to_T O D ty a))
 409       (enum (FinSet_of_FType O D ty)))) M3.
 410 #O #D #ty #M1 #M2 #Hred
 411  %{(Vec O D ty
 412     (map (FinSet_of_FType O D ty) (T O D)
 413     (λa:FinSet_of_FType O D ty.subst O D M2 0 (to_T O D ty a))
 414     (enum (FinSet_of_FType O D ty))))} (* CR-term *) %
 415   [@R_to_star @rmem
 416   |@star_red_vec2 [>length_map >length_map //] #n #M0
 417    cases (true_or_false (leb (|enum (FinSet_of_FType O D ty)|) n)) #Hcase
 418     [>nth_to_default [2:>length_map @(leb_true_to_le … Hcase)]
 419      >nth_to_default [2:>length_map @(leb_true_to_le … Hcase)] //
 420     |cut (n < |enum (FinSet_of_FType O D ty)|)
 421       [@not_le_to_lt @leb_false_to_not_le @Hcase] #Hlt
 422      cut (∃a:FinSet_of_FType O D ty.True)
 423       [lapply Hlt lapply (enum_complete (FinSet_of_FType O D ty))
 424        cases (enum (FinSet_of_FType O D ty))
 425         [#_ normalize #H @False_ind @(absurd … H) @lt_to_not_le //
 426         |#a #l #_ #_ %{a} //
 427         ]
 428       ] * #a #_
 429      >(nth_map ?????? a Hlt) >(nth_map ?????? a Hlt)
 430      @red_star_subst2 @R_to_star //
 431     ]
 432   ]
 433 qed.
 434
 435 (* we need to proceed by structural induction on the term and then
 436 by inversion on the two redexes. The problem are the moves in a
 437 same subterm, since we need an induction hypothesis, there *)
 438
 439 lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
 440 ∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
 441 #O #D #M @(T_elim … M)
 442   [#o #a #M1 #M2 #H elim(red_val ????? H)
 443   |#n #M1 #M2 #H elim(red_rel ???? H)
 444   |(* app : this is the interesting case *)
 445    #P #Q #HindP #HindQ
 446    #M1 #M2 #H1 inversion H1 -H1
 447     [(* right redex is beta *)
 448      #ty #Q #N #Hc #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
 449       [#ty1 #Q1 #N1 #Hc1 #H1 destruct (H1) #H_
 450        %{(subst O D Q1 0 N1)} (* CR-term *) /2/
 451       |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
 452       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ cases (red_lambda … redM0)
 453         [* #Q1 * #redQ #HM10 >HM10
 454          %{(subst O D Q1 0 N0)} (* CR-term *) %
 455           [@red_star_subst2 @R_to_star //|@R_to_star @rbeta @Hc]
 456         |#HM1 >HM1 @critical
 457         ]
 458       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
 459        %{(subst O D Q 0 N1)} (* CR-term *)
 460        %[@red_star_subst @R_to_star //|@R_to_star @rbeta @(red_closed … Hc) //]
 461       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 462       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 463       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 464       ]
 465     |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
 466       [#P1 #M1 #N1 #_ #H1 destruct (H1) (* vacuous *)
 467       |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
 468        >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
 469       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
 470       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
 471       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 472       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 473       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 474       ]
 475     |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
 476       #Hl inversion Hl
 477       [#ty1 #M1 #N1 #Hc #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4) *
 478         [* #M3 * #H1 #H2 >H2 %{(subst O D M3 0 N1)} %
 479           [@R_to_star @rbeta @Hc|@red_star_subst2 @R_to_star @H1]
 480         |#H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
 481          %{M3} /2/
 482         ]
 483       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
 484        lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
 485       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 486        lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
 487        %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
 488       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
 489        %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
 490       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 491       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 492       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 493       ]
 494     |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
 495       #Hl inversion Hl
 496       [#ty1 #M0 #N0 #Hc #H1 destruct (H1) #HM2
 497        %{(subst O D M0 0 N1)} (* CR-term *) %
 498         [@R_to_star @rbeta @(red_closed … Hc) //|@red_star_subst @R_to_star // ]
 499       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
 500       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 501        %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
 502       |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
 503        lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
 504        %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
 505       |#ty1 #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 506       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 507       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 508       ]
 509     |(* right redex is rlam *) #ty #N0 #N1 #_ #_ #H1 destruct (H1) (* vacuous *)
 510     |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
 511     |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
 512      #H1 destruct (H1) (* vacuous *)
 513     ]
 514   |#ty #M1 #Hind #M2 #M3 #H1 #H2 (* this case is not trivial any more *)
 515    lapply (red_lambda … H1) *
 516     [* #M4 * #H3 #H4 >H4 lapply (red_lambda … H2) *
 517       [* #M5 * #H5 #H6 >H6 lapply(Hind … H3 H5) * #M6 * #H7 #H8
 518        %{(Lambda O D ty M6)} (* CR-term *) % @star_red_lambda //
 519       |#H5 >H5 @critical3 //
 520       ]
 521     |#HM2 >HM2 lapply (red_lambda … H2) *
 522       [* #M4 * #Hred #HM3 >HM3 lapply (critical3 … ty ?? Hred) * #M5
 523        * #H3 #H4 %{M5} (* CR-term *) % //
 524       |#HM3 >HM3 %{M3} (* CR-term *) % //
 525       ]
 526     ]
 527   |#ty #v1 #Hind #M1 #M2 #H1 #H2
 528    lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
 529    lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
 530    >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
 531    (* we must proceed by cases on the list *) * normalize
 532     [(* N11 = N21 *) *
 533       [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
 534         [@mem_append_l2 %1 //]
 535        * #M3 * #HM31 #HM32
 536        %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
 537        % [@star_red_vec //|@star_red_vec //]
 538       |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
 539         [@mem_append_l2 %1 //]
 540        * #M3 * #HM31 #HM32
 541        %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
 542        % [@star_red_vec //|@star_red_vec //]
 543       ]
 544     |(* N11 ≠  N21 *) -Hind #P #l *
 545       [* #Hv11 #Hv22 destruct
 546        %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
 547         [>associative_append >associative_append normalize @rvec //
 548         |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 549         ]
 550       |* #Hv11 #Hv22 destruct
 551        %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
 552         [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 553         |>associative_append >associative_append normalize @rvec //
 554         ]
 555       ]
 556     ]
 557   ]
 558 qed.
 559
 560
 561
 562