X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_2%2Frelocation%2Flleq.ma;h=b431e0d1836d5e6af189f968c26bc49e235a1e6d;hb=1e414c3226307112e8289e014e2941479df7c663;hp=b5bef1116cbdc0f3d259b1b9385589611131ac58;hpb=e76eade57c0454a58b0d58e5484efe9af417847e;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
index b5bef1116..b431e0d18 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma
@@ -13,151 +13,142 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/lazyeq_4.ma".
-include "basic_2/relocation/ldrop.ma".
+include "basic_2/relocation/llpx_sn.ma".
 
 (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************)
 
-inductive lleq: nat → term → relation lenv ≝
-| lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2
-| lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d →
-             ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 →
-             lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2
-| lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i →
-             ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V →
-             lleq 0 V K1 K2 → lleq d (#i) L1 L2
-| lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2
-| lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2
-| lleq_bind: ∀a,I,L1,L2,V,T,d.
-             lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) →
-             lleq d (ⓑ{a,I}V.T) L1 L2
-| lleq_flat: ∀I,L1,L2,V,T,d.
-             lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2
-.
+definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2.
+
+definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq.
 
 interpretation
    "lazy equivalence (local environment)"
-   'LazyEq d T L1 L2 = (lleq d T L1 L2).
+   'LazyEq T d L1 L2 = (lleq d T L1 L2).
 
-(* Basic_properties *********************************************************)
+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.
 
-lemma lleq_sym: ∀d,T. symmetric … (lleq d T).
-#d #T #L1 #L2 #H elim H -d -T -L1 -L2
-/2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
-qed-.
+(* Basic inversion lemmas ***************************************************)
 
-(* Note this is: "∀d,T. reflexive … (lleq d T)" *)
-axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L.
-(*
-#T #L @(f2_ind … rfw … L T) -L -T
-#n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/
-#i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/
-#HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/
-elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/
-qed.
-*)
-
-lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2.
-#L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1
-/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/
-[ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *)
-| #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2)
-  [ -d1 /3 width=10 by lleq_skip/
-  | /3 width=7 by lleq_lref, transitive_le/
-  ]
-]
+lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. (
+                   ∀L1,L2,d,k. |L1| = |L2| → R d (⋆k) L1 L2
+                ) → (
+                   ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → R d (#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
+                ) → (
+                   ∀L1,L2,d,i. |L1| = |L2| → |L1| ≤ i → |L2| ≤ i → R d (#i) L1 L2
+                ) → (
+                   ∀L1,L2,d,p. |L1| = |L2| → R d (§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
+                ) → (
+                   ∀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
+                ) →
+                ∀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/
 qed-.
 
-lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, V] L2 → L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V →
-                   L1 ⋕[0, ⓑ{a,I}V.T] L2.
-/3 width=3 by lleq_ge, lleq_bind/ 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.
+/2 width=2 by llpx_sn_inv_bind/ qed-.
 
-(* Basic inversion lemmas ***************************************************)
+lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[ⓕ{I}V.T, d] L2 →
+                     L1 ⋕[V, d] L2 ∧ L1 ⋕[T, d] L2.
+/2 width=2 by llpx_sn_inv_flat/ qed-.
 
-fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i →
-                        ∨∨ |L1| ≤ i ∧ |L2| ≤ i
-                         | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
-                                                ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
-                                                K1 ⋕[d-i-1, V1] K2 &
-                                                K1 ⋕[d-i-1, V2] K2 &
-                                                i < d
-                         | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
-                                        ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
-                                        K1 ⋕[0, V] K2 & d ≤ i.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #j #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/
-| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/
-| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/
-| #L1 #L2 #d #p #_ #j #H destruct
-| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
-| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct
-]
-qed-.
+(* Basic forward lemmas *****************************************************)
 
-lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 →
+lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|.
+/2 width=4 by llpx_sn_fwd_length/ qed-.
+
+lemma lleq_fwd_lref: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 →
                      ∨∨ |L1| ≤ i ∧ |L2| ≤ i
-                      | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 &
-                                             ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 &
-                                             K1 ⋕[d-i-1, V1] K2 &
-                                             K1 ⋕[d-i-1, V2] K2 &
-                                             i < d
-                      | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V &
-                                     ⇩[0, i] L2 ≡ K2.ⓑ{I}V &
-                                     K1 ⋕[0, V] K2 & d ≤ i.
-/2 width=3 by lleq_inv_lref_aux/ qed-.
-
-fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T →
-                        L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct
-| #L1 #L2 #d #p #_ #b #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/
-| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct
-]
+                      | 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/
+* /3 width=7 by or3_intro2, ex4_4_intro/
 qed-.
 
-lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 →
-                     L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V.
-/2 width=4 by lleq_inv_bind_aux/ qed-.
-
-fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T →
-                        L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
-#d #X #L1 #L2 * -d -X -L1 -L2
-[ #L1 #L2 #d #k #_ #J #W #U #H destruct
-| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct
-| #L1 #L2 #d #p #_ #J #W #U #H destruct
-| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct
-| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/
-]
-qed-.
+lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[i] L1 ≡ K1 →
+                         ∃K2. ⇩[i] L2 ≡ K2.
+/2 width=7 by llpx_sn_fwd_ldrop_sn/ qed-.
 
-lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 →
-                     L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2.
-/2 width=4 by lleq_inv_flat_aux/ qed-.
+lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[i] L2 ≡ K2 →
+                         ∃K1. ⇩[i] L1 ≡ K1.
+/2 width=7 by llpx_sn_fwd_ldrop_dx/ qed-.
 
-(* Basic forward lemmas *****************************************************)
+lemma lleq_fwd_bind_sn: ∀a,I,L1,L2,V,T,d.
+                        L1 ⋕[ⓑ{a,I}V.T, d] L2 → L1 ⋕[V, d] L2.
+/2 width=4 by llpx_sn_fwd_bind_sn/ qed-.
 
-lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|.
-#L1 #L2 #T #d #H elim H -L1 -L2 -T -d //
-[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_
-| #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12
-]
-lapply (ldrop_fwd_length … HLK1) -HLK1
-lapply (ldrop_fwd_length … HLK2) -HLK2
-normalize //
-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.
+/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.
+/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.
+/2 width=3 by llpx_sn_fwd_flat_dx/ qed-.
 
-lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 →
-                         ∃K2. ⇩[0, i] L2 ≡ K2.
-#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H
-#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/
+(* Basic properties *********************************************************)
+
+lemma lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → L1 ⋕[⋆k, d] 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.
+/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.
+/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.
+/2 width=1 by llpx_sn_free/ qed.
+
+lemma lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → L1 ⋕[§p, d] 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.
+/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.
+/2 width=1 by llpx_sn_flat/ qed.
+
+lemma lleq_refl: ∀d,T. reflexive … (lleq d 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
+/2 width=7 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/
 qed-.
 
-lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 →
-                         ∃K1. ⇩[0, i] L1 ≡ K1.
-/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ 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.
+/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.
+/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 →
+                   L1 ⋕[ⓑ{a,I}V.T, 0] L2.
+/2 width=1 by llpx_sn_bind_O/ qed-.