- degree-based equivalene for terms

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / etc_new / drops / drops_length.etc

diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc
index 8953abb9a8748eee20003a1e25d1bcb1069dcc0b..667f9689dba8541451b0f584dd692e6a4c4105f7 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc
+++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops_length.etc
@@ -1,5 +1,3 @@
-include "basic_2/grammar/lenv_length.ma".
-
 lemma drop_inv_O1_gt: ∀L,K,m,s. ⬇[s, 0, m] L ≡ K → |L| < m →
                       s = Ⓣ ∧ K = ⋆.
 #L elim L -L [| #L #Z #X #IHL ] #K #m #s #H normalize in ⊢ (?%?→?); #H1m
@@ -90,58 +88,6 @@ lemma drop_fwd_length_le_ge: ∀L1,L2,l,m,s. ⬇[s, l, m] L1 ≡ L2 → l ≤ |L
 ]
 qed-.
 
-lemma drop_fwd_length: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L1| = |L2| + m.
-#L1 #L2 #l #m #H elim H -L1 -L2 -l -m //
-#l #m #H >H -m //
-qed-.
-
-lemma drop_fwd_length_le2: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → m ≤ |L1|.
-#L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
-qed-.
-
-lemma drop_fwd_length_le4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → |L2| ≤ |L1|.
-#L1 #L2 #l #m #H lapply (drop_fwd_length … H) -H //
-qed-.
-
-lemma drop_fwd_length_lt2: ∀L1,I2,K2,V2,l,m.
-                           ⬇[Ⓕ, l, m] L1 ≡ K2. ⓑ{I2} V2 → m < |L1|.
-#L1 #I2 #K2 #V2 #l #m #H
-lapply (drop_fwd_Y2 … H) #Hm
-lapply (drop_fwd_length … H) -l #H <(yplus_O2 m) >H -L1
-/2 width=1 by monotonic_ylt_plus_sn/
-qed-.
-
-lemma drop_fwd_length_lt4: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 → 0 < m → |L2| < |L1|.
-#L1 #L2 #l #m #H
-lapply (drop_fwd_Y2 … H) #Hm
-lapply (drop_fwd_length … H) -l
-/2 width=1 by monotonic_ylt_plus_sn/
-qed-.
-
-lemma drop_fwd_length_eq1: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
-                           |L1| = |L2| → |K1| = |K2|.
-#L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
-lapply (drop_fwd_Y2 … HLK1) #Hm
-lapply (drop_fwd_length … HLK1) -HLK1
-lapply (drop_fwd_length … HLK2) -HLK2
-#H #H0 >H in HL12; -H >H0 -H0 #H
-@(yplus_inv_monotonic_dx … H) -H // (**) (* auto fails *)
-qed-.
-
-lemma drop_fwd_length_eq2: ∀L1,L2,K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 →
-                           |K1| = |K2| → |L1| = |L2|.
-#L1 #L2 #K1 #K2 #l #m #HLK1 #HLK2 #HL12
-lapply (drop_fwd_length … HLK1) -HLK1
-lapply (drop_fwd_length … HLK2) -HLK2 //
-qed-.
-
-lemma drop_inv_length_eq: ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ L2 →
-                          |L1| = |L2| → m = 0.
-#L1 #L2 #l #m #H #HL12 lapply (drop_fwd_length … H) -H
->HL12 -L1 #H elim (discr_yplus_x_xy … H) -H //
-#H elim (ylt_yle_false (|L2|) (∞)) //
-qed-.
-
 lemma drop_fwd_be: ∀L,K,s,l,m,i. ⬇[s, l, m] L ≡ K → |K| ≤ i → i < l → |L| ≤ i.
 #L #K #s #l #m #i #HLK #HK #Hl elim (ylt_split i (|L|)) //
 #HL elim (drop_O1_lt (Ⓕ) … HL) #I #K0 #V #HLK0 -HL
@@ -150,3 +96,17 @@ elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0
 #K1 #V1 #HK1 #_ #_ lapply (drop_fwd_length_lt2 … HK1) -I -K1 -V1
 #H elim (ylt_yle_false … H) -H //
 qed-.
+
+lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
+                  ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
+#K2 #i @(ynat_ind … i) -i
+[ /3 width=3 by lreq_O2, ex2_intro/
+| #i #IHi #Y >yplus_succ2 #Hi
+  elim (drop_O1_lt (Ⓕ) Y 0) [2: >Hi // ]
+  #I #L1 #V #H lapply (drop_inv_O2 … H) -H #H destruct
+  >length_pair in Hi; #H lapply (ysucc_inv_inj … H) -H
+  #HL1K2 elim (IHi L1) -IHi // -HL1K2
+  /3 width=5 by lreq_pair, drop_drop, ex2_intro/
+| #L1 >yplus_Y2 #H elim (ylt_yle_false (|L1|) (∞)) //
+]
+qed-.