matita/matita/lib/finite_lambda/finite_lambda.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   | rbeta: ∀P,M,N. red O D (App O D (Lambda O D P M) N) (subst O D M 0 N)
 211   | riota: ∀ty,v,a,M.
 212       assoc (FinSet_of_FType O D ty) ? a (enum (FinSet_of_FType O D ty)) v = Some ? M →
 213       red O D (App O D (Vec O D ty v) (to_T O D ty a)) M
 214   | rappl: ∀M,M1,N. red O D M M1 → red O D (App O D M N) (App O D M1 N)
 215   | rappr: ∀M,N,N1. red O D N N1 → red O D (App O D M N) (App O D M N1)
 216   | rmem: ∀ty,M. red O D (Lambda O D ty M)
 217       (Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 218       (enum (FinSet_of_FType O D ty))))
 219   | rvec: ∀ty,N,N1,v,v1. red O D N N1 →
 220       red O D (Vec O D ty (v@N::v1)) (Vec O D ty (v@N1::v1)).
 221
 222 (* some inversion cases *)
 223 lemma red_vec: ∀O,D,ty,v,M.
 224   red O D (Vec O D ty v) M → ∃N,N1,v1,v2.
 225       red O D N N1 ∧ v = v1@N::v2 ∧ M = Vec O D ty (v1@N1::v2).
 226 #O #D #ty #v #M #Hred inversion Hred
 227   [#ty1 #M0 #N #H destruct
 228   |#ty1 #v1 #a #M0 #_ #H destruct
 229   |#M0 #M1 #N #_ #_ #H destruct
 230   |#M0 #M1 #N #_ #_ #H destruct
 231   |#ty1 #M0 #H destruct
 232   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct #_ %{N} %{N1} %{v1} %{v2} /3/
 233   ]
 234 qed.
 235
 236 lemma red_lambda: ∀O,D,ty,M,N.
 237   red O D (Lambda O D ty M) N →
 238       N = Vec O D ty (map ?? (λa. subst O D M 0 (to_T O D ty a))
 239       (enum (FinSet_of_FType O D ty))).
 240 #O #D #ty #M #N #Hred inversion Hred
 241   [#ty1 #M0 #N #H destruct
 242   |#ty1 #v1 #a #M0 #_ #H destruct
 243   |#M0 #M1 #N #_ #_ #H destruct
 244   |#M0 #M1 #N #_ #_ #H destruct
 245   |#ty1 #M0 #H destruct #_ //
 246   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 247   ]
 248 qed.
 249
 250 lemma red_val: ∀O,D,ty,a,N.
 251   red O D (Val O D ty a) N → False.
 252 #O #D #ty #M #N #Hred inversion Hred
 253   [#ty1 #M0 #N #H destruct
 254   |#ty1 #v1 #a #M0 #_ #H destruct
 255   |#M0 #M1 #N #_ #_ #H destruct
 256   |#M0 #M1 #N #_ #_ #H destruct
 257   |#ty1 #M0 #H destruct #_
 258   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 259   ]
 260 qed.
 261
 262 lemma red_rel: ∀O,D,n,N.
 263   red O D (Rel O D n) N → False.
 264 #O #D #n #N #Hred inversion Hred
 265   [#ty1 #M0 #N #H destruct
 266   |#ty1 #v1 #a #M0 #_ #H destruct
 267   |#M0 #M1 #N #_ #_ #H destruct
 268   |#M0 #M1 #N #_ #_ #H destruct
 269   |#ty1 #M0 #H destruct #_
 270   |#ty1 #N #N1 #v1 #v2 #Hred1 #_ #H destruct
 271   ]
 272 qed.
 273
 274 lemma star_red_appl: ∀O,D,M,M1,N. star ? (red O D) M M1 →
 275   star ? (red O D) (App O D M N) (App O D M1 N).
 276 #O #D #M #N #N1 #H elim H //
 277 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappl @HPQ
 278 qed.
 279
 280 lemma star_red_appr: ∀O,D,M,N,N1. star ? (red O D) N N1 →
 281   star ? (red O D) (App O D M N) (App O D M N1).
 282 #O #D #M #N #N1 #H elim H //
 283 #P #Q #Hind #HPQ #Happ %1[|@Happ] @rappr @HPQ
 284 qed.
 285
 286 lemma star_red_vec: ∀O,D,ty,N,N1,v1,v2. star ? (red O D) N N1 →
 287   star ? (red O D) (Vec O D ty (v1@N::v2)) (Vec O D ty (v1@N1::v2)).
 288 #O #D #ty #N #N1 #v1 #v2 #H elim H //
 289 #P #Q #Hind #HPQ #Hvec %1[|@Hvec] @rvec @HPQ
 290 qed.
 291
 292 axiom red_subst : ∀O,D,M,N,N1,i.
 293   red O D N N1 → red O D (subst O D M i N) (subst O D M i N1).
 294
 295 axiom red_star_subst : ∀O,D,M,N,N1,i.
 296   star ? (red O D) N N1 → star ? (red O D) (subst O D M i N) (subst O D M i N1).
 297
 298 axiom canonical_to_T: ∀O,D.∀M:T O D.∀ty.(* type_of M ty → *)
 299   ∃a:FinSet_of_FType O D ty. star ? (red O D) M (to_T O D ty a).
 300
 301 axiom normal_to_T: ∀O,D,M,ty,a. red O D (to_T O D ty a) M → False.
 302
 303 lemma critical: ∀O,D,ty,M,N.
 304   ∃M3:T O D
 305   .star (T O D) (red O D) (subst O D M 0 N) M3
 306    ∧star (T O D) (red O D)
 307     (App O D
 308      (Vec O D ty
 309       (map (FinSet_of_FType O D ty) (T O D)
 310        (λa0:FinSet_of_FType O D ty.subst O D M 0 (to_T O D ty a0))
 311        (enum (FinSet_of_FType O D ty)))) N) M3.
 312 #O #D #ty #M #N
 313 lapply (canonical_to_T O D N ty) * #a #Ha
 314 %{(subst O D M 0 (to_T O D ty a))} (* CR-term *)
 315 %[@red_star_subst @Ha
 316  |@trans_star [|@(star_red_appr … Ha)] @R_to_star @riota
 317   lapply (enum_complete (FinSet_of_FType O D ty) a)
 318   elim (enum (FinSet_of_FType O D ty))
 319    [normalize #H1 destruct (H1)
 320    |#hd #tl #Hind #H cases (orb_true_l … H) -H #Hcase
 321      [normalize >Hcase >(\P Hcase) //
 322      |normalize cases (true_or_false (a==hd)) #Hcase1
 323        [normalize >Hcase1 >(\P Hcase1) // |>Hcase1 @Hind @Hcase]
 324      ]
 325    ]
 326  ]
 327 qed.
 328
 329 lemma critical2: ∀O,D,ty,a,M,M1,M2,v.
 330   red O D (Vec O D ty v) M →
 331   red O D (App O D (Vec O D ty v) (to_T O D ty a)) M1 →
 332   assoc (FinSet_of_FType O D ty) (T O D) a (enum (FinSet_of_FType O D ty)) v
 333     =Some (T O D) M2 →
 334   ∃M3:T O D
 335   .star (T O D) (red O D) M2 M3
 336    ∧star (T O D) (red O D) (App O D M (to_T O D ty a)) M3.
 337 #O #D #ty #a #M #M1 #M2 #v #redM #redM1 #Ha lapply (red_vec … redM) -redM
 338 * #N * #N1 * #v1 * #v2 * * #Hred1 #Hv #HM0 >HM0 -HM0 >Hv in Ha; #Ha
 339 cases (same_assoc … a (enum (FinSet_of_FType O D ty)) v1 v2 N N1)
 340   [* >Ha -Ha #H1 destruct (H1) #Ha
 341    %{N1} (* CR-term *) % [@R_to_star //|@R_to_star @(riota … Ha)]
 342   |#Ha1 %{M2} (* CR-term *) % [// | @R_to_star @riota <Ha1 @Ha]
 343   ]
 344 qed.
 345
 346 (* we need to proceed by structural induction on the term and then
 347 by inversion on the two redexes. The problem are the moves in a
 348 same subterm, since we need an induction hypothesis, there *)
 349
 350 lemma local_confluence: ∀O,D,M,M1,M2. red O D M M1 → red O D M M2 →
 351 ∃M3. star ? (red O D) M1 M3 ∧ star ? (red O D) M2 M3.
 352 #O #D #M @(T_elim … M)
 353   [#o #a #M1 #M2 #H elim(red_val ????? H)
 354   |#n #M1 #M2 #H elim(red_rel ???? H)
 355   |(* app : this is the interesting case *)
 356    #P #Q #HindP #HindQ
 357    #M1 #M2 #H1 inversion H1 -H1
 358     [(* right redex is beta *)
 359      #ty #Q #N #HM >HM -HM #HM1 >HM1 - HM1 #Hl inversion Hl
 360       [#P1 #M1 #N1 #H1 destruct (H1) #H_ %{(subst O D M1 0 N1)} (* CR-term *) /2/
 361       |#ty #v #a #M0 #_ #H1 destruct (H1) (* vacuous *)
 362       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #_ inversion redM0
 363         [#P0 #M0 #N #H destruct
 364         |#ty #v #a #M0 #_ #H1 destruct (H1)
 365         |#M0 #M1 #N #_ #_ #H1 destruct (H1)
 366         |#M0 #M1 #N #_ #_ #H1 destruct (H1)
 367         |#ty1 #M0 #H1 destruct (H1) #HM1 @critical
 368         |#ty #N #N1 #v #v1 #_ #_ #H1 destruct (H1)
 369         ]
 370       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #HM2
 371        %{(subst O D Q 0 N1)} (* CR-term *)
 372        %[@red_star_subst @R_to_star //|@R_to_star @rbeta]
 373       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 374       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 375       ]
 376     |(* right redex is iota *)#ty #v #a #M3 #Ha #_ #_ #Hl inversion Hl
 377       [#P1 #M1 #N1 #H1 destruct (H1) (* vacuous *)
 378       |#ty1 #v1 #a1 #M4 #Ha1 #H1 destruct (H1) -H1 #HM4 >(inj_to_T … e0) in Ha;
 379        >Ha1 #H1 destruct (H1) %{M3} (* CR-term *) /2/
 380       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2 @(critical2 … redM0 Hl Ha)
 381       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) elim (normal_to_T … redN0N1)
 382       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 383       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 384       ]
 385     |(* right redex is appl *)#M3 #M4 #N #redM3M4 #_ #H1 destruct (H1) #_
 386       #Hl inversion Hl
 387       [#ty1 #M1 #N1 #H1 destruct (H1) #HM2 lapply (red_lambda … redM3M4)
 388        #H >H -H lapply (critical O D ty1 M1 N1) * #M3 * #H1 #H2
 389        %{M3} /2/
 390       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct
 391        lapply (critical2 … redM3M4 Hl Ha1) * #M3 * #H1 #H2 %{M3} /2/
 392       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 393        lapply (HindP … redM0 redM3M4) * #M3 * #H1 #H2
 394        %{(App O D M3 N0)} (* CR-term *) % [@star_red_appl //|@star_red_appl //]
 395       |#M0 #N0 #N1 #redN0N1 #_ #H1 destruct (H1) #_
 396        %{(App O D M4 N1)} % @R_to_star [@rappr //|@rappl //]
 397       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 398       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 399       ]
 400     |(* right redex is appr *)#M3 #N #N1 #redN #_ #H1 destruct (H1) #_
 401       #Hl inversion Hl
 402       [#ty1 #M0 #N0 #H1 destruct (H1) #HM2
 403        %{(subst O D M0 0 N1)} (* CR-term *) %
 404         [@R_to_star @rbeta | @red_star_subst @R_to_star //]
 405       |#ty1 #v1 #a1 #M4 #Ha1 #H1 #H2 destruct (H1) elim (normal_to_T … redN)
 406       |#M0 #M10 #N0 #redM0 #_ #H1 destruct (H1) #HM2
 407        %{(App O D M10 N1)} (* CR-term *) % @R_to_star [@rappl //|@rappr //]
 408       |#M0 #N0 #N10 #redN0 #_ #H1 destruct (H1) #_
 409        lapply (HindQ … redN0 redN) * #M3 * #H1 #H2
 410        %{(App O D M0 M3)} (* CR-term *) % [@star_red_appr //|@star_red_appr //]
 411       |#ty1 #M0 #H1 destruct (H1) (* vacuous *)
 412       |#ty1 #N0 #N1 #v #v1 #_ #_ #H1 destruct (H1) (* vacuous *)
 413       ]
 414     |(* right redex is rmem *) #ty #M0 #H1 destruct (H1) (* vacuous *)
 415     |(* right redex is vec *) #ty #N #N1 #v #v1 #_ #_
 416      #H1 destruct (H1) (* vacuous *)
 417     ]
 418   |#ty #M1 #Hind #M2 #M3 #H1 #H2
 419    lapply (red_lambda … H1) #HM2 lapply (red_lambda … H2) #HM3
 420    %{M2} (* CR-term *) % //
 421   |#ty #v1 #Hind #M1 #M2 #H1 #H2
 422    lapply (red_vec … H1) * #N11 * #N12 * #v11 * #v12 * * #redN11 #Hv1 #HM1
 423    lapply (red_vec … H2) * #N21* #N22 * #v21 * #v22 * * #redN21 #Hv2 #HM2
 424    >Hv1 in Hv2; #Hvv lapply (compare_append … Hvv) -Hvv *
 425    (* we must proceed by cases on the list *) * normalize
 426     [(* N11 = N21 *) *
 427       [>append_nil * #Hl1 #Hl2 destruct lapply(Hind N11 … redN11 redN21)
 428         [@mem_append_l2 %1 //]
 429        * #M3 * #HM31 #HM32
 430        %{(Vec O D ty (v21@M3::v12))} (* CR-term *)
 431        % [@star_red_vec //|@star_red_vec //]
 432       |>append_nil * #Hl1 #Hl2 destruct lapply(Hind N21 … redN21 redN11)
 433         [@mem_append_l2 %1 //]
 434        * #M3 * #HM31 #HM32
 435        %{(Vec O D ty (v11@M3::v22))} (* CR-term *)
 436        % [@star_red_vec //|@star_red_vec //]
 437       ]
 438     |(* N11 ≠  N21 *) -Hind #P #l *
 439       [* #Hv11 #Hv22 destruct
 440        %{((Vec O D ty ((v21@N22::l)@N12::v12)))} (* CR-term *) % @R_to_star
 441         [>associative_append >associative_append normalize @rvec //
 442         |>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 443         ]
 444       |* #Hv11 #Hv22 destruct
 445        %{((Vec O D ty ((v11@N12::l)@N22::v22)))} (* CR-term *) % @R_to_star
 446         [>append_cons <associative_append <append_cons in ⊢ (???%?); @rvec //
 447         |>associative_append >associative_append normalize @rvec //
 448         ]
 449       ]
 450     ]
 451   ]
 452 qed.
 453
 454
 455
 456