- ng_kernel: we print the offending term when guarded_by_constructors fails

[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 a0926cad1ee17d5dad37b85510b62d5555d629d6..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
@@ -151,13 +97,6 @@ elim (drop_conf_lt … HLK … HLK0 … H0) -HLK -HLK0 -H0
 #H elim (ylt_yle_false … H) -H //
 qed-.
 
-lemma pippo: ∀L1,L2,t1. ⬇*[Ⓕ, t1] L1 ≡ L2 → ∀t2. ⬇*[Ⓕ, t2] L1 ≡ L2 →
-|t1| + ∥t2∥ = ∥t1∥ + |t2|.
-#L1 #L2 #t1 #H elim H -L1 -L2 -t1
-[ #t1 #Ht1 #t2 #H elim (drops_inv_atom1 … H) -H
-  #_ #Ht2 >Ht1 -Ht1 // >Ht2 -Ht2 //
-| #I #L1 #L2 #V #t1 #_ #IH #t2 #H normalize 
-
 lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i →
                   ∃∃L2. L1 ⩬[0, i] L2 & ⬇[i] L2 ≡ K2.
 #K2 #i @(ynat_ind … i) -i