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

   1 lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
   2                       s = Ⓣ ∧ K = ⋆.
   3 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
   4 [ elim (drop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
   5   #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (ylt_yle_false … H1m) -H1m //
   6 | elim (drop_inv_O1_pair1 … H) -H * #H2m #HLK destruct
   7   [ elim (ylt_yle_false … H1m) -H1m //
   8   | elim (IHL … HLK) -IHL -HLK /2 width=1 by ylt_pred, conj/
   9   ]
  10 ]
  11 qed-.
  12
  13 lemma drop_O1_le: ∀s,m,L. m ≤ |L| → ∃K. ⬇[s, 0, m] L ≡ K.
  14 #s #m @(ynat_ind … m) -m /2 width=2 by ex_intro/
  15 [ #m #IHm *
  16   [ #H elim (ylt_yle_false … H) -H //
  17   | #L #I #V #H elim (IHm L) -IHm /3 width=2 by drop_drop, yle_inv_succ, ex_intro/
  18   ]
  19 | #L #H elim (ylt_yle_false … H) -H //
  20 ]
  21 qed-.
  22
  23 lemma drop_O1_lt: ∀s,L,m. m < |L| → ∃∃I,K,V. ⬇[s, 0, m] L ≡ K.ⓑ{I}V.
  24 #s #L elim L -L
  25 [ #m #H elim (ylt_yle_false … H) -H //
  26 | #L #I #V #IHL #m @(ynat_ind … m) -m /2 width=4 by drop_pair, ex1_3_intro/
  27   [ #m #_#H elim (IHL m) -IHL /3 width=4 by drop_drop, ylt_inv_succ, ex1_3_intro/
  28   | #H elim (ylt_yle_false … H) -H //
  29   ]
  30 ]
  31 qed-.
  32
  33 lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → m ≤ |L| → ∀I,V.
  34                     ∃∃J,W. ⬇[s, 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W.
  35 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H #Hm #I #V
  36 [ elim (drop_inv_atom1 … H) -H #H >(yle_inv_O2 … Hm) -m
  37   #Hs destruct /2 width=3 by ex1_2_intro/
  38 | elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK destruct /2 width=3 by ex1_2_intro/
  39   elim (IHL … HLK … Z X) -IHL -HLK
  40   /3 width=3 by yle_pred, drop_drop_lt, ex1_2_intro/
  41 ]
  42 qed-.
  43
  44 lemma drop_O1_ge: ∀L,m. |L| ≤ m → ⬇[Ⓣ, 0, m] L ≡ ⋆.
  45 #L elim L -L [ #m #_ @drop_atom #H destruct ]
  46 #L #I #V #IHL #m @(ynat_ind … m) -m //
  47 [ #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/
  48 | /4 width=1 by drop_drop, yle_inv_succ/
  49 ]
  50 qed.
  51
  52 lemma drop_O1_eq: ∀L,s. ⬇[s, 0, |L|] L ≡ ⋆.
  53 #L elim L -L /2 width=1 by drop_drop/
  54 qed.
  55
  56 lemma drop_fwd_length_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → |L1| ≤ l → |L2| = |L1|.
  57 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
  58 [ #I #L1 #L2 #V #m #_ #_ #H elim (ylt_yle_false … H) -H //
  59 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IH #H
  60   lapply (yle_inv_succ … H) -H #H
  61   >length_pair >length_pair /3 width=1 by eq_f/
  62 ]
  63 qed-.
  64
  65 lemma drop_fwd_length_le_le: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 →
  66                              ∀l0. l + m + l0 = |L1| → |L2| = l + l0.
  67 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
  68 [ #l #m #Hm #l0 #H elim (yplus_inv_O … H) -H
  69   #H #H0 elim (yplus_inv_O … H) -H
  70   #H1 #_ destruct //
  71 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1 #IH #l0
  72   /3 width=1 by ysucc_inv_inj/
  73 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 #l0 >yplus_succ1 >yplus_succ1 #H
  74   lapply (ysucc_inv_inj … H) -H #Hl1
  75   >yplus_succ1 /3 width=1 by eq_f/
  76 ]
  77 qed-.
  78
  79 lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| ≤ l + m → |L2| = l.
  80 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m
  81 [ #l #m #_ #H #_ /2 width=1 by yle_inv_O2/
  82 | #I #L #V #_ #H elim (ylt_yle_false … H) -H //
  83 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1
  84   /3 width=1 by yle_inv_succ/
  85 | #I #L1 #L2 #V1 #v2 #l #m #_ #_ #IH
  86   >yplus_SO2 >yplus_SO2
  87   /4 width=1 by yle_inv_succ, eq_f/
  88 ]
  89 qed-.
  90
  91 lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
  92 #L #K #s #l #m #i #HLK #HK #Hl elim (ylt_split i (|L|)) //
  93 #HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
  94 elim (ylt_inv_plus_sn … Hl) -Hl #l0 #H0
  95 elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0
  96 #K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1
  97 #H elim (ylt_yle_false … H) -H //
  98 qed-.
  99
 100 lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
 101                   ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
 102 #K2 #i @(ynat_ind … i) -i
 103 [ /3 width=3 by lreq_O2, ex2_intro/
 104 | #i #IHi #Y >yplus_succ2 #Hi
 105   elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
 106   #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
 107   >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
 108   #HL1K2 elim (IHi L1) -IHi // -HL1K2
 109   /3 width=5 by lreq_pair, drop_drop, ex2_intro/
 110 | #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //
 111 ]
 112 qed-.