X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Fmultiple%2Flleq.ma;h=1f57f73be1e756d31c002e9d49d856cd6b3dbd57;hb=e258362c37ec6d9132ec57bd5e4987d148c10799;hp=7be12035eb0dc0aca78ff5eb167b6916628c22b9;hpb=7e06d9d148ae04a21943377debd933a742d0c2fa;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma index 7be12035e..1f57f73be 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/multiple/lleq.ma @@ -23,7 +23,7 @@ definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq. interpretation "lazy equivalence (local environment)" - 'LazyEq T d L1 L2 = (lleq d T L1 L2). + 'LazyEq T l L1 L2 = (lleq l T L1 L2). definition lleq_transitive: predicate (relation3 lenv term term) ≝ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R L1 T1 T2. @@ -31,122 +31,122 @@ definition lleq_transitive: predicate (relation3 lenv term term) ≝ (* Basic inversion lemmas ***************************************************) lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( - ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2 + ∀L1,L2,l,k. |L1| = |L2| → R l (⋆k) L1 L2 ) → ( - ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#i) L1 L2 + ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → R l (#i) L1 L2 ) → ( - ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i → - ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → - K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R d (#i) L1 L2 + ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i → + ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V → + K1 ≡[V, yinj O] K2 → R (yinj O) V K1 K2 → R l (#i) L1 L2 ) → ( - ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2 + ∀L1,L2,l,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R l (#i) L1 L2 ) → ( - ∀L1,L2,d,p. |L1| = |L2| → R d (§p) L1 L2 + ∀L1,L2,l,p. |L1| = |L2| → R l (§p) L1 L2 ) → ( - ∀a,I,L1,L2,V,T,d. - L1 ≡[V, d]L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V → - R d V L1 L2 → R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R d (ⓑ{a,I}V.T) L1 L2 + ∀a,I,L1,L2,V,T,l. + L1 ≡[V, l]L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → + R l V L1 L2 → R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → R l (ⓑ{a,I}V.T) L1 L2 ) → ( - ∀I,L1,L2,V,T,d. - L1 ≡[V, d]L2 → L1 ≡[T, d] L2 → - R d V L1 L2 → R d T L1 L2 → R d (ⓕ{I}V.T) L1 L2 + ∀I,L1,L2,V,T,l. + L1 ≡[V, l]L2 → L1 ≡[T, l] L2 → + R l V L1 L2 → R l T L1 L2 → R l (ⓕ{I}V.T) L1 L2 ) → - ∀d,T,L1,L2. L1 ≡[T, d] L2 → R d T L1 L2. -#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #d #T #L1 #L2 #H elim H -L1 -L2 -T -d /2 width=8 by/ + ∀l,T,L1,L2. L1 ≡[T, l] L2 → R l T L1 L2. +#R #H1 #H2 #H3 #H4 #H5 #H6 #H7 #l #T #L1 #L2 #H elim H -L1 -L2 -T -l /2 width=8 by/ qed-. -lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ≡[ⓑ{a,I}V.T, d] L2 → - L1 ≡[V, d] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V. +lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,l. L1 ≡[ⓑ{a,I}V.T, l] L2 → + L1 ≡[V, l] L2 ∧ L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V. /2 width=2 by llpx_sn_inv_bind/ qed-. -lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ≡[ⓕ{I}V.T, d] L2 → - L1 ≡[V, d] L2 ∧ L1 ≡[T, d] L2. +lemma lleq_inv_flat: ∀I,L1,L2,V,T,l. L1 ≡[ⓕ{I}V.T, l] L2 → + L1 ≡[V, l] L2 ∧ L1 ≡[T, l] L2. /2 width=2 by llpx_sn_inv_flat/ qed-. (* Basic forward lemmas *****************************************************) -lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ≡[T, d] L2 → |L1| = |L2|. +lemma lleq_fwd_length: ∀L1,L2,T,l. L1 ≡[T, l] L2 → |L1| = |L2|. /2 width=4 by llpx_sn_fwd_length/ qed-. -lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ≡[#i, d] L2 → +lemma lleq_fwd_lref: ∀L1,L2,l,i. L1 ≡[#i, l] L2 → ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | yinj i < d - | ∃∃I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V & - ⇩[i] L2 ≡ K2.ⓑ{I}V & - K1 ≡[V, yinj 0] K2 & d ≤ yinj i. -#L1 #L2 #d #i #H elim (llpx_sn_fwd_lref … H) /2 width=1/ + | yinj i < l + | ∃∃I,K1,K2,V. ⬇[i] L1 ≡ K1.ⓑ{I}V & + ⬇[i] L2 ≡ K2.ⓑ{I}V & + K1 ≡[V, yinj 0] K2 & l ≤ yinj i. +#L1 #L2 #l #i #H elim (llpx_sn_fwd_lref … H) /2 width=1 by or3_intro0, or3_intro1/ * /3 width=7 by or3_intro2, ex4_4_intro/ qed-. -lemma lleq_fwd_drop_sn: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 → - ∃K2. ⇩[i] L2 ≡ K2. +lemma lleq_fwd_drop_sn: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K1,i. ⬇[i] L1 ≡ K1 → + ∃K2. ⬇[i] L2 ≡ K2. /2 width=7 by llpx_sn_fwd_drop_sn/ qed-. -lemma lleq_fwd_drop_dx: ∀L1,L2,T,d. L1 ≡[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 → - ∃K1. ⇩[i] L1 ≡ K1. +lemma lleq_fwd_drop_dx: ∀L1,L2,T,l. L1 ≡[l, T] L2 → ∀K2,i. ⬇[i] L2 ≡ K2 → + ∃K1. ⬇[i] L1 ≡ K1. /2 width=7 by llpx_sn_fwd_drop_dx/ qed-. -lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d. - L1 ≡[ⓑ{a,I}V.T, d] L2 → L1 ≡[V, d] L2. +lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,l. + L1 ≡[ⓑ{a,I}V.T, l] L2 → L1 ≡[V, l] L2. /2 width=4 by llpx_sn_fwd_bind_sn/ qed-. -lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,d. - L1 ≡[ⓑ{a,I}V.T, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V. +lemma lleq_fwd_bind_dx: ∀a,I,L1,L2,V,T,l. + L1 ≡[ⓑ{a,I}V.T, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V. /2 width=2 by llpx_sn_fwd_bind_dx/ qed-. -lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,d. - L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[V, d] L2. +lemma lleq_fwd_flat_sn: ∀I,L1,L2,V,T,l. + L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[V, l] L2. /2 width=3 by llpx_sn_fwd_flat_sn/ qed-. -lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,d. - L1 ≡[ⓕ{I}V.T, d] L2 → L1 ≡[T, d] L2. +lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,l. + L1 ≡[ⓕ{I}V.T, l] L2 → L1 ≡[T, l] L2. /2 width=3 by llpx_sn_fwd_flat_dx/ qed-. (* Basic properties *********************************************************) -lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ≡[⋆k, d] L2. +lemma lleq_sort: ∀L1,L2,l,k. |L1| = |L2| → L1 ≡[⋆k, l] L2. /2 width=1 by llpx_sn_sort/ qed. -lemma lleq_skip: ∀L1,L2,d,i. yinj i < d → |L1| = |L2| → L1 ≡[#i, d] L2. +lemma lleq_skip: ∀L1,L2,l,i. yinj i < l → |L1| = |L2| → L1 ≡[#i, l] L2. /2 width=1 by llpx_sn_skip/ qed. -lemma lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ yinj i → - ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → - K1 ≡[V, 0] K2 → L1 ≡[#i, d] L2. +lemma lleq_lref: ∀I,L1,L2,K1,K2,V,l,i. l ≤ yinj i → + ⬇[i] L1 ≡ K1.ⓑ{I}V → ⬇[i] L2 ≡ K2.ⓑ{I}V → + K1 ≡[V, 0] K2 → L1 ≡[#i, l] L2. /2 width=9 by llpx_sn_lref/ qed. -lemma lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, d] L2. +lemma lleq_free: ∀L1,L2,l,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → L1 ≡[#i, l] L2. /2 width=1 by llpx_sn_free/ qed. -lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ≡[§p, d] L2. +lemma lleq_gref: ∀L1,L2,l,p. |L1| = |L2| → L1 ≡[§p, l] L2. /2 width=1 by llpx_sn_gref/ qed. -lemma lleq_bind: ∀a,I,L1,L2,V,T,d. - L1 ≡[V, d] L2 → L1.ⓑ{I}V ≡[T, ⫯d] L2.ⓑ{I}V → - L1 ≡[ⓑ{a,I}V.T, d] L2. +lemma lleq_bind: ∀a,I,L1,L2,V,T,l. + L1 ≡[V, l] L2 → L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → + L1 ≡[ⓑ{a,I}V.T, l] L2. /2 width=1 by llpx_sn_bind/ qed. -lemma lleq_flat: ∀I,L1,L2,V,T,d. - L1 ≡[V, d] L2 → L1 ≡[T, d] L2 → L1 ≡[ⓕ{I}V.T, d] L2. +lemma lleq_flat: ∀I,L1,L2,V,T,l. + L1 ≡[V, l] L2 → L1 ≡[T, l] L2 → L1 ≡[ⓕ{I}V.T, l] L2. /2 width=1 by llpx_sn_flat/ qed. -lemma lleq_refl: ∀d,T. reflexive … (lleq d T). +lemma lleq_refl: ∀l,T. reflexive … (lleq l T). /2 width=1 by llpx_sn_refl/ qed. lemma lleq_Y: ∀L1,L2,T. |L1| = |L2| → L1 ≡[T, ∞] L2. /2 width=1 by llpx_sn_Y/ qed. -lemma lleq_sym: ∀d,T. symmetric … (lleq d T). -#d #T #L1 #L2 #H @(lleq_ind … H) -d -T -L1 -L2 +lemma lleq_sym: ∀l,T. symmetric … (lleq l T). +#l #T #L1 #L2 #H @(lleq_ind … H) -l -T -L1 -L2 /2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ qed-. -lemma lleq_ge_up: ∀L1,L2,U,dt. L1 ≡[U, dt] L2 → - ∀T,d,e. ⇧[d, e] T ≡ U → - dt ≤ d + e → L1 ≡[U, d] L2. +lemma lleq_ge_up: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → + ∀T,l,m. ⬆[l, m] T ≡ U → + lt ≤ l + m → L1 ≡[U, l] L2. /2 width=6 by llpx_sn_ge_up/ qed-. -lemma lleq_ge: ∀L1,L2,T,d1. L1 ≡[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ≡[T, d2] L2. +lemma lleq_ge: ∀L1,L2,T,l1. L1 ≡[T, l1] L2 → ∀l2. l1 ≤ l2 → L1 ≡[T, l2] L2. /2 width=3 by llpx_sn_ge/ qed-. lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2.ⓑ{I}V → @@ -156,5 +156,5 @@ lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2 (* Advanceded properties on lazy pointwise extensions ************************) lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2. + ∀L1,L2,T,l. L1 ≡[T, l] L2 → llpx_sn R l T L1 L2. /2 width=3 by llpx_sn_co/ qed-.