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

   1 include "basic_2/grammar/lenv_length.ma".
   2
   3 lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
   4                       s = Ⓣ ∧ K = ⋆.
   5 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
   6 [ elim (drop_inv_atom1 … H) -H elim s -s /2 width=1 by conj/
   7   #_ #Hs lapply (Hs ?) // -Hs #H destruct elim (ylt_yle_false … H1m) -H1m //
   8 | elim (drop_inv_O1_pair1 … H) -H * #H2m #HLK destruct
   9   [ elim (ylt_yle_false … H1m) -H1m //
  10   | elim (IHL … HLK) -IHL -HLK /2 width=1 by ylt_pred, conj/
  11   ]
  12 ]
  13 qed-.
  14
  15 lemma drop_O1_le: ∀s,m,L. m ≤ |L| → ∃K. ⬇[s, 0, m] L ≡ K.
  16 #s #m @(ynat_ind … m) -m /2 width=2 by ex_intro/
  17 [ #m #IHm *
  18   [ #H elim (ylt_yle_false … H) -H //
  19   | #L #I #V #H elim (IHm L) -IHm /3 width=2 by drop_drop, yle_inv_succ, ex_intro/
  20   ]
  21 | #L #H elim (ylt_yle_false … H) -H //
  22 ]
  23 qed-.
  24
  25 lemma drop_O1_lt: ∀s,L,m. m < |L| → ∃∃I,K,V. ⬇[s, 0, m] L ≡ K.ⓑ{I}V.
  26 #s #L elim L -L
  27 [ #m #H elim (ylt_yle_false … H) -H //
  28 | #L #I #V #IHL #m @(ynat_ind … m) -m /2 width=4 by drop_pair, ex1_3_intro/
  29   [ #m #_#H elim (IHL m) -IHL /3 width=4 by drop_drop, ylt_inv_succ, ex1_3_intro/
  30   | #H elim (ylt_yle_false … H) -H //
  31   ]
  32 ]
  33 qed-.
  34
  35 lemma drop_O1_pair: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → m ≤ |L| → ∀I,V.
  36                     ∃∃J,W. ⬇[s, 0, m] L.ⓑ{I}V ≡ K.ⓑ{J}W.
  37 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H #Hm #I #V
  38 [ elim (drop_inv_atom1 … H) -H #H >(yle_inv_O2 … Hm) -m
  39   #Hs destruct /2 width=3 by ex1_2_intro/
  40 | elim (drop_inv_O1_pair1 … H) -H * #Hm #HLK destruct /2 width=3 by ex1_2_intro/
  41   elim (IHL … HLK … Z X) -IHL -HLK
  42   /3 width=3 by yle_pred, drop_drop_lt, ex1_2_intro/
  43 ]
  44 qed-.
  45
  46 lemma drop_O1_ge: ∀L,m. |L| ≤ m → ⬇[Ⓣ, 0, m] L ≡ ⋆.
  47 #L elim L -L [ #m #_ @drop_atom #H destruct ]
  48 #L #I #V #IHL #m @(ynat_ind … m) -m //
  49 [ #H elim (ylt_yle_false … H) -H /2 width=1 by ylt_inj/
  50 | /4 width=1 by drop_drop, yle_inv_succ/
  51 ]
  52 qed.
  53
  54 lemma drop_O1_eq: ∀L,s. ⬇[s, 0, |L|] L ≡ ⋆.
  55 #L elim L -L /2 width=1 by drop_drop/
  56 qed.
  57
  58 lemma drop_fwd_length_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → |L1| ≤ l → |L2| = |L1|.
  59 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
  60 [ #I #L1 #L2 #V #m #_ #_ #H elim (ylt_yle_false … H) -H //
  61 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IH #H
  62   lapply (yle_inv_succ … H) -H #H
  63   >length_pair >length_pair /3 width=1 by eq_f/
  64 ]
  65 qed-.
  66
  67 lemma drop_fwd_length_le_le: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 →
  68                              ∀l0. l + m + l0 = |L1| → |L2| = l + l0.
  69 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m //
  70 [ #l #m #Hm #l0 #H elim (yplus_inv_O … H) -H
  71   #H #H0 elim (yplus_inv_O … H) -H
  72   #H1 #_ destruct //
  73 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1 #IH #l0
  74   /3 width=1 by ysucc_inv_inj/
  75 | #I #L1 #L2 #V1 #V2 #l #m #_ #_ #IHL12 #l0 >yplus_succ1 >yplus_succ1 #H
  76   lapply (ysucc_inv_inj … H) -H #Hl1
  77   >yplus_succ1 /3 width=1 by eq_f/
  78 ]
  79 qed-.
  80
  81 lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L1| → |L1| ≤ l + m → |L2| = l.
  82 #L1 #L2 #l #m #s #H elim H -L1 -L2 -l -m
  83 [ #l #m #_ #H #_ /2 width=1 by yle_inv_O2/
  84 | #I #L #V #_ #H elim (ylt_yle_false … H) -H //
  85 | #I #L1 #L2 #V #m #_ >yplus_O1 >yplus_O1
  86   /3 width=1 by yle_inv_succ/
  87 | #I #L1 #L2 #V1 #v2 #l #m #_ #_ #IH
  88   >yplus_SO2 >yplus_SO2
  89   /4 width=1 by yle_inv_succ, eq_f/
  90 ]
  91 qed-.
  92
  93 lemma drop_fwd_length: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L1| = |L2| + m.
  94 #L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
  95 #l #m #H >H -m //
  96 qed-.
  97
  98 lemma drop_fwd_length_le2: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → m ≤ |L1|.
  99 #L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
 100 qed-.
 101
 102 lemma drop_fwd_length_le4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L2| ≤ |L1|.
 103 #L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
 104 qed-.
 105
 106 lemma drop_fwd_length_lt2: ∀L1,I2,K2,V2,l,m.
 107                            ⬇[Ⓕ, l, m] L1 ≡ K2. ⓑ{I2} V2 → m < |L1|.
 108 #L1 #I2 #K2 #V2 #l #m #H
 109 lapply (drop_fwd_Y2 … H) #Hm
 110 lapply (drop_fwd_length … H) -l #H <(yplus_O2 m) >H -L1
 111 /2 width=1 by monotonic_ylt_plus_sn/
 112 qed-.
 113
 114 lemma drop_fwd_length_lt4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → 0 < m → |L2| < |L1|.
 115 #L1 #L2 #l #m #H
 116 lapply (drop_fwd_Y2 … H) #Hm
 117 lapply (drop_fwd_length … H) -l
 118 /2 width=1 by monotonic_ylt_plus_sn/
 119 qed-.
 120
 121 lemma drop_fwd_length_eq1: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
 122                            |L1| = |L2| → |K1| = |K2|.
 123 #L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
 124 lapply (drop_fwd_Y2 … HLK1) #Hm
 125 lapply (drop_fwd_length … HLK1) -HLK1
 126 lapply (drop_fwd_length … HLK2) -HLK2
 127 #H #H0 >H in HL12; -H >H0 -H0 #H
 128 @(yplus_inv_monotonic_dx … H) -H // (**) (* auto fails *)
 129 qed-.
 130
 131 lemma drop_fwd_length_eq2: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
 132                            |K1| = |K2| → |L1| = |L2|.
 133 #L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
 134 lapply (drop_fwd_length … HLK1) -HLK1
 135 lapply (drop_fwd_length … HLK2) -HLK2 //
 136 qed-.
 137
 138 lemma drop_inv_length_eq: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 →
 139                           |L1| = |L2| → m = 0.
 140 #L1 #L2 #l #m #H #HL12 lapply (drop_fwd_length … H) -H
 141 >HL12 -L1 #H elim (discr_yplus_x_xy … H) -H //
 142 #H elim (ylt_yle_false (|L2|) (∞)) //
 143 qed-.
 144
 145 lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
 146 #L #K #s #l #m #i #HLK #HK #Hl elim (ylt_split i (|L|)) //
 147 #HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
 148 elim (ylt_inv_plus_sn … Hl) -Hl #l0 #H0
 149 elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0
 150 #K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1
 151 #H elim (ylt_yle_false … H) -H //
 152 qed-.
 153
 154 lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
 155 |t1| + ∥t2∥ = ∥t1∥ + |t2|.
 156 #L1 #L2 #t1 #H elim H -L1 -L2 -t1
 157 [ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
 158   #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
 159 | #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize
 160
 161 lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
 162                   ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
 163 #K2 #i @(ynat_ind … i) -i
 164 [ /3 width=3 by lreq_O2, ex2_intro/
 165 | #i #IHi #Y >yplus_succ2 #Hi
 166   elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
 167   #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
 168   >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
 169   #HL1K2 elim (IHi L1) -IHi // -HL1K2
 170   /3 width=5 by lreq_pair, drop_drop, ex2_intro/
 171 | #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //
 172 ]
 173 qed-.