matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc

   1 lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2 →
   2                   ∃∃L. ⬇[s, l, m2 - m1] L1 ≡ L & ⬇[s, l, m1] L ≡ L2.
   3 #L1 #L2 #l #m2 #s #H elim H -L1 -L2 -l -m2
   4 [ #l #m2 #Hs #m1 #Hm12 @(ex2_intro … (⋆))
   5   @drop_atom #H lapply (Hs H) -s #H destruct /2 width=1 by le_n_O_to_eq/
   6 | #I #L1 #V #m1 #Hm1 lapply (le_n_O_to_eq … Hm1) -Hm1
   7   #H destruct /2 width=3 by ex2_intro/
   8 | #I #L1 #L2 #V #m2 #HL12 #IHL12 #m1 @(nat_ind_plus … m1) -m1
   9   [ /3 width=3 by drop_drop, ex2_intro/
  10   | -HL12 #m1 #_ #Hm12 lapply (le_plus_to_le_r … Hm12) -Hm12
  11     #Hm12 elim (IHL12 … Hm12) -IHL12 >minus_plus_plus_l
  12     #L #HL1 #HL2 elim (lt_or_ge (|L1|) (m2-m1)) #H0
  13     [ elim (drop_inv_O1_gt … HL1 H0) -HL1 #H1 #H2 destruct
  14       elim (drop_inv_atom1 … HL2) -HL2 #H #_ destruct
  15       @(ex2_intro … (⋆)) [ @drop_O1_ge normalize // ]
  16       @drop_atom #H destruct
  17     | elim (drop_O1_pair … HL1 H0 I V) -HL1 -H0 /3 width=5 by drop_drop, ex2_intro/
  18     ]
  19   ]
  20 | #I #L1 #L2 #V1 #V2 #l #m2 #_ #HV21 #IHL12 #m1 #Hm12 elim (IHL12 … Hm12) -IHL12
  21   #L #HL1 #HL2 elim (lift_split … HV21 l m1) -HV21 /3 width=5 by drop_skip, ex2_intro/
  22 ]
  23 qed-.
  24
  25 (* Basic_2A1: includes: drop_split *)
  26 lemma drops_split_trans: ∀L1,L2,f,c. ⬇*[c, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f →
  27                          ∃∃L. ⬇*[c, f1] L1 ≡ L & ⬇*[c, f2] L ≡ L2.
  28 #L1 #L2 #f #c #H elim H -L1 -L2 -f
  29 [ #f #Hc #f1 #f2 #Hf @(ex2_intro … (⋆)) @drops_atom
  30   #H lapply (Hc H) -c
  31   #H elim (after_inv_isid3 … Hf H) -f //
  32 | #I #L1 #L2 #V #f #HL12 #IHL12 #f1 #f2 #Hf elim (after_inv_xxS … Hf) -Hf *
  33   [ #g1 #g2 #Hf #H1 #H2 destruct elim (IHL12 … Hf) -f
  34     #L #HL1 #HL2 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1 by drops_drop/
  35     @drops_skip //
  36   | #g1 #Hf #H destruct elim (IHL12 … Hf) -f
  37     /3 width=5 by ex2_intro, drops_drop/
  38   ]
  39 | #I #L1 #L2 #V1 #V2 #f #_ #HV21 #IHL12 #f1 #f2 #Hf elim (after_inv_xxO … Hf) -Hf
  40   #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21
  41   elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip/
  42 ]
  43 qed-.
  44
  45 lemma drop_inv_refl: ∀L,l,m. ⬇[Ⓕ, l, m] L ≡ L → m = 0.
  46 /2 width=5 by drop_inv_length_eq/ qed-.
  47
  48 fact drop_inv_FT_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 →
  49                       ∀I,K,V. L2 = K.ⓑ{I}V → s = Ⓣ → l = 0 →
  50                       ⬇[Ⓕ, l, m] L1 ≡ K.ⓑ{I}V.
  51 #L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m
  52 [ #l #m #_ #J #K #W #H destruct
  53 | #I #L #V #J #K #W #H destruct //
  54 | #I #L1 #L2 #V #m #_ #IHL12 #J #K #W #H1 #H2 destruct
  55   /3 width=1 by drop_drop/
  56 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #_ #J #K #W #_ #_ #H
  57   elim (ysucc_inv_O_dx … H)
  58 ]
  59 qed-.
  60
  61 lemma drop_inv_FT: ∀I,L,K,V,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
  62 K.ⓑ{I}V.
  63 /2 width=5 by drop_inv_FT_aux/ qed.
  64
  65 lemma drop_inv_gen: ∀I,L,K,V,s,m. ⬇[s, 0, m] L ≡ K.ⓑ{I}V → ⬇[m] L ≡
  66 K.ⓑ{I}V.
  67 #I #L #K #V * /2 width=1 by drop_inv_FT/
  68 qed-.
  69
  70 lemma drop_inv_T: ∀I,L,K,V,s,m. ⬇[Ⓣ, 0, m] L ≡ K.ⓑ{I}V → ⬇[s, 0, m] L
  71 ≡ K.ⓑ{I}V.
  72 #I #L #K #V * /2 width=1 by drop_inv_FT/
  73 qed-.