matita/matita/contribs/lambdadelta/basic_2/etc/cpt/cpt.etc

   1 (* Advanced inversion lemmas ************************************************)
   2
   3 lemma cpt_inv_sort_sn (h) (n) (G) (L) (s):
   4       ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
   5       ∨∨ ∧∧ X2 = ⋆s & n = 0
   6        | ∧∧ X2 = ⋆(⫯[h]s) & n =1.
   7 #h #n #G #L #s #X2 * #c #Hc #H
   8 elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct
   9 /3 width=1 by or_introl, or_intror, conj/
  10 qed-.
  11
  12 lemma cpt_inv_zero_sn (h) (n) (G) (L):
  13       ∀X2. ⦃G,L⦄ ⊢ #0 ⬆[h,n] X2 →
  14       ∨∨ ∧∧ X2 = #0 & n = 0
  15        | ∃∃K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,n] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓓV1
  16        | ∃∃m,K,V1,V2. ⦃G,K⦄ ⊢ V1 ⬆[h,m] V2 & ⇧*[1] V2 ≘ X2 & L = K.ⓛV1 & n = ↑m.
  17 #h #n #G #L #X2 * #c #Hc #H
  18 elim (cpg_inv_zero1 … H) -H *
  19 [ #H1 #H2 destruct /3 width=1 by or3_intro0, conj/
  20 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
  21   /4 width=8 by or3_intro1, ex3_3_intro, ex2_intro/
  22 | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 destruct
  23   elim (ist_inv_plus_SO_dx … H2) -H2 [| // ] #m #Hc #H destruct
  24   /4 width=8 by or3_intro2, ex4_4_intro, ex2_intro/
  25 ]
  26 qed-.
  27
  28 lemma cpt_inv_lref_sn (h) (n) (G) (L) (i):
  29       ∀X2. ⦃G,L⦄ ⊢ #↑i ⬆[h,n] X2 →
  30       ∨∨ ∧∧ X2 = #(↑i) & n = 0
  31        | ∃∃I,K,T. ⦃G,K⦄ ⊢ #i ⬆[h,n] T & ⇧*[1] T ≘ X2 & L = K.ⓘ{I}.
  32 #h #n #G #L #i #X2 * #c #Hc #H
  33 elim (cpg_inv_lref1 … H) -H *
  34 [ #H1 #H2 destruct /3 width=1 by or_introl, conj/
  35 | #I #K #V2 #HV2 #HVT2 #H destruct
  36  /4 width=6 by ex3_3_intro, ex2_intro, or_intror/
  37 ]
  38 qed-.
  39
  40 lemma cpt_inv_gref_sn (h) (n) (G) (L) (l):
  41       ∀X2. ⦃G,L⦄ ⊢ §l ⬆[h,n] X2 → ∧∧ X2 = §l & n = 0.
  42 #h #n #G #L #l #X2 * #c #Hc #H
  43 elim (cpg_inv_gref1 … H) -H #H1 #H2 destruct
  44 /2 width=1 by conj/
  45 qed-.
  46
  47
  48 lemma cpt_inv_sort_sn_iter (h) (n) (G) (L) (s):
  49       ∀X2. ⦃G,L⦄ ⊢ ⋆s ⬆[h,n] X2 →
  50       ∧∧ X2 = ⋆(((next h)^n) s) & n ≤ 1.
  51 #h #n #G #L #s #X2 #H
  52 elim (cpt_inv_sort_sn … H) -H * #H1 #H2 destruct
  53 /2 width=1 by conj/
  54 qed-.