From dffdece065d12d9961a6c3f1222f6d112030336f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sun, 25 May 2014 20:04:55 +0000 Subject: [PATCH] - theory of llor now includes (long awaited) non-recursive alternative definition - poinwise extensions downgraded (current llor does not need the improved version) - some refactoring in etc --- .../basic_2/etc/{lenv_px => lcpcs}/lcpcs.etc | 0 .../etc/{lenv_px => lcpcs}/lcpcs_ltpr.etc | 0 .../contribs/lambdadelta/basic_2/etc/llor.etc | 115 ----- .../etc/{lpx_sn => llor}/lleq_llor.etc | 0 .../etc/{lpx_sn => llor}/lpxs_llor.etc | 0 .../basic_2/etc/lpx_sn/cpr_llpx_sn.etc | 49 ++ .../basic_2/etc/lpx_sn/cpx_llpx_sn.etc | 52 +++ .../lambdadelta/basic_2/etc/lpx_sn/lleq.etc | 160 +++++++ .../basic_2/etc/lpx_sn/llpx_sn.etc | 209 +++++++++ .../basic_2/etc/lpx_sn/llpx_sn_alt.etc | 62 +++ .../basic_2/etc/lpx_sn/llpx_sn_alt_rec.etc | 250 ++++++++++ .../basic_2/etc/lpx_sn/llpx_sn_ldrop.etc | 431 ++++++++++++++++++ .../basic_2/etc/lpx_sn/llpx_sn_lpx_sn.etc | 38 ++ .../basic_2/etc/lpx_sn/llpx_sn_tc.etc | 26 ++ .../lambdadelta/basic_2/etc/lpx_sn/lpr.etc | 61 +++ .../lambdadelta/basic_2/etc/lpx_sn/lpx.etc | 65 +++ .../lenv_px_sn.etc => lpx_sn/lpx_sn.etc} | 42 +- .../basic_2/etc/lpx_sn/lpx_sn_alt.etc | 125 +++++ .../basic_2/etc/lpx_sn/lpx_sn_ldrop.etc | 104 +++++ .../basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc | 48 ++ .../basic_2/etc/lpx_sn/lpx_sn_tc.etc | 119 +++++ .../basic_2/etc/lpx_sn/ssta_llpx_sn.etc | 44 ++ .../basic_2/reduction/cpr_llpx_sn.ma | 4 +- .../basic_2/reduction/cpx_llpx_sn.ma | 4 +- .../lambdadelta/basic_2/reduction/lpr.ma | 2 +- .../lambdadelta/basic_2/reduction/lpx.ma | 2 +- .../lambdadelta/basic_2/relocation/lpx_sn.ma | 26 +- .../basic_2/relocation/lpx_sn_alt.ma | 14 +- .../basic_2/relocation/lpx_sn_ldrop.ma | 10 +- .../basic_2/relocation/lpx_sn_lpx_sn.ma | 8 +- .../basic_2/relocation/lpx_sn_tc.ma | 34 +- .../basic_2/static/ssta_llpx_sn.ma | 3 +- .../lambdadelta/basic_2/substitution/lleq.ma | 8 +- .../lambdadelta/basic_2/substitution/llor.ma | 56 +++ .../basic_2/substitution/llor_alt.ma | 66 +++ .../basic_2/substitution/llpx_sn.ma | 12 +- .../basic_2/substitution/llpx_sn_alt.ma | 4 +- .../basic_2/substitution/llpx_sn_alt_rec.ma | 24 +- .../basic_2/substitution/llpx_sn_ldrop.ma | 34 +- .../basic_2/substitution/llpx_sn_lpx_sn.ma | 2 +- .../basic_2/substitution/llpx_sn_tc.ma | 4 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../lambdadelta/ground_2/lib/arith.ma | 8 + 43 files changed, 2097 insertions(+), 230 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lenv_px => lcpcs}/lcpcs.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lenv_px => lcpcs}/lcpcs_ltpr.etc (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lpx_sn => llor}/lleq_llor.etc (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc/{lpx_sn => llor}/lpxs_llor.etc (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpr_llpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpx_llpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_alt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_alt_rec.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_ldrop.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_lpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_tc.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpr.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lenv_px/lenv_px_sn.etc => lpx_sn/lpx_sn.etc} (63%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_alt.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_ldrop.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_lpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ssta_llpx_sn.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lcpcs/lcpcs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lcpcs/lcpcs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lcpcs/lcpcs_ltpr.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lenv_px/lcpcs_ltpr.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lcpcs/lcpcs_ltpr.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc deleted file mode 100644 index 6a750a0ec..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llor.etc +++ /dev/null @@ -1,115 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "ground_2/xoa/xoa2.ma". -include "basic_2/notation/relations/lazyor_4.ma". -include "basic_2/relocation/lpx_sn_alt.ma". -include "basic_2/substitution/cofrees.ma". - -(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) - -inductive clor (T) (L2) (I) (K1) (V1): predicate term ≝ -| clor_sn: |K1| < |L2| → |L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → clor T L2 I K1 V1 V1 -| clor_dx: ∀K2,V2. |K1| < |L2| → (|L2|-|K1|-1 ~ϵ 𝐅*⦃K1, T⦄ → ⊥) → - ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 I K1 V1 V2 -. - -definition llor: relation4 term lenv lenv lenv ≝ - λT,L2. lpx_sn (clor T L2). - -interpretation - "lazy union (local environment)" - 'LazyOr L1 T L2 L = (llor T L2 L1 L). - -(* Basic properties *********************************************************) - -lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → |L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ → - L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V. -/3 width=2 by clor_sn, lpx_sn_pair/ qed. - -lemma llor_pair_dx: ∀I,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → - |L1| < |L2| → (|L2|-|L1|-1 ~ϵ 𝐅*⦃L1, T⦄ → ⊥) → - ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{I}V2 → - L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2. -/4 width=3 by clor_dx, lpx_sn_pair/ qed. -(* -lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/ -#L1 #I1 #V1 #IHL1 normalize -#H elim IHL1 -IHL1 /2 width=3 by transitive_le/ -#L #HT elim (cofrees_dec L1 T (|L2|-|L1|-1)) -[ /3 width=2 by llor_pair_sn, ex_intro/ -| elim (ldrop_O1_lt L2 (|L2|-|L1|-1)) - /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/ -| -] -qed-. -*) -(* Alternative definition ***************************************************) - -(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) -lemma plus_minus_minus_be: ∀x,y,z:nat. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. -#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // -qed-. - -fact plus_minus_minus_be_aux: ∀i,x,y,z:nat. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y. -/2 width=1 by plus_minus_minus_be/ qed-. - -lemma llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| → - (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → - (|L2|-|L1|+i ~ϵ 𝐅*⦃K1, T⦄ → I1 = I ∧ V1 = V) ∧ - (∀I2,K2,V2. (|L2|-|L1|+i ~ϵ 𝐅*⦃K1, T⦄ → ⊥) → - ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I & I2 = I & V2 = V - ) - ) → L1 ⩖[T] L2 ≡ L. -#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 -#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK -lapply (ldrop_fwd_length_minus4 … HLK1) -lapply (ldrop_fwd_length_le4 … HLK1) -normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // #H2i -lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 #HKL1 -elim (IH … HLK1 HLK) -IH -HLK1 -HLK #IH1 #IH2 -elim (cofrees_dec K1 T (|L2|-|L1|+i)) -[ -IH2 #HT elim (IH1 … HT) -IH1 - /3 width=2 by clor_sn, conj/ -| -IH1 #H elim (ldrop_O1_lt L2 (|L2|-|L1|+i)) /2 width=1 by monotonic_lt_minus_l/ - #I2 #K2 #V2 #HLK2 elim (IH2 … HLK2) -IH2 - /5 width=3 by clor_dx, ex_intro, and3_intro/ -] -qed. - -lemma llor_inv_alt: ∀T,L2,L1,L. L1 ⩖[T] L2 ≡ L → |L1| ≤ |L2| → - |L1| = |L| ∧ - (∀I1,I,K1,K,V1,V,i. - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → - (∃∃U. ⇧[|L2|-|L1|+i, 1] U ≡ T & - I1 = I & V1 = V & K1 ⩖[T] L2 ≡ K - ) ∨ - (∃∃I2,K2,V2. (∀U. ⇧[|L2|-|L1|+i, 1] U ≡ T → ⊥) & - ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 & - I1 = I & V2 = V & K1 ⩖[T] L2 ≡ K - ) - ). -#T #L2 #L1 #L #H #HL12 elim (lpx_sn_inv_alt … H) -H -#HL1 #IH @conj // -HL1 -#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK -lapply (ldrop_fwd_length_minus4 … HLK1) -lapply (ldrop_fwd_length_le4 … HLK1) -normalize #HKL1 #H1i lapply (plus_minus_minus_be_aux … HL12 H1i) // -lapply (transitive_le … HKL1 HL12) -HKL1 -HL12 -elim (IH … HLK1 HLK) -IH #H * -/4 width=5 by ex5_3_intro, ex4_intro, or_intror, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq_llor.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llor/lleq_llor.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_llor.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpxs_llor.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/llor/lpxs_llor.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpr_llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpr_llpx_sn.etc new file mode 100644 index 000000000..4db858798 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpr_llpx_sn.etc @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/llpx_sn_ldrop.ma". +include "basic_2/reduction/cpr.ma". + +(* CONTEXT-SENSITIVE PARALLEL REDUCTION FOR TERMS ***************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma cpr_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → + (∀I.l_liftable (R I)) → + (∀I.l_deliftable_sn (R I)) → + ∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0). +#R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ // +| #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ +| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // + #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) + [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/ + | /3 width=4 by llpx_sn_bind_repl_O/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpx_llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpx_llpx_sn.etc new file mode 100644 index 000000000..418106494 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/cpx_llpx_sn.etc @@ -0,0 +1,52 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/llpx_sn_ldrop.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on lazy sn pointwise extensions *******************************) + +(* Note: lemma 1000 *) +lemma cpx_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → + (∀I.l_liftable (R I)) → + (∀I.l_deliftable_sn (R I)) → + ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0). +#R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ // +| /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ +| #I #G #Ls #Ks #V1s #V2s #W2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #I #G #Ls #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #T #_ #HT2 #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /3 width=10 by llpx_sn_inv_lift_le, ldrop_drop/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +| #G #Ls #V1 #V2 #T #_ #IHV12 #Ld #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +| #a #G #Ls #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_flat, llpx_sn_bind/ +| #a #G #Ls #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + #HV1 #H elim (llpx_sn_inv_bind_O … H) -H // + #HW1 #HT1 @llpx_sn_bind_O /2 width=1 by/ @llpx_sn_flat (**) (* full auto too slow *) + [ /3 width=10 by llpx_sn_lift_le, ldrop_drop/ + | /3 width=4 by llpx_sn_bind_repl_O/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq.etc new file mode 100644 index 000000000..dc138a492 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lleq.etc @@ -0,0 +1,160 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyeq_4.ma". +include "basic_2/substitution/llpx_sn.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +definition ceq: relation4 bind2 lenv term term ≝ λI,L,T1,T2. T1 = T2. + +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). + +definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝ + λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R I L1 T1 T2. + +(* 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,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_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-. + +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-. + +(* Basic forward lemmas *****************************************************) + +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 + | 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_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_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-. + +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_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-. + +(* 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_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-. + +(* Advancded properties on lazy pointwise exyensions ************************) + +lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) → + ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2. +/2 width=3 by llpx_sn_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn.etc new file mode 100644 index 000000000..918b42605 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn.etc @@ -0,0 +1,209 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "ground_2/ynat/ynat_plus.ma". +include "basic_2/relocation/ldrop.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +inductive llpx_sn (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝ +| llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2 +| llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2 +| llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → + ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 → + llpx_sn R (yinj 0) V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d (#i) L1 L2 +| llpx_sn_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R d (#i) L1 L2 +| llpx_sn_gref: ∀L1,L2,d,p. |L1| = |L2| → llpx_sn R d (§p) L1 L2 +| llpx_sn_bind: ∀a,I,L1,L2,V,T,d. + llpx_sn R d V L1 L2 → llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → + llpx_sn R d (ⓑ{a,I}V.T) L1 L2 +| llpx_sn_flat: ∀I,L1,L2,V,T,d. + llpx_sn R d V L1 L2 → llpx_sn R d T L1 L2 → llpx_sn R d (ⓕ{I}V.T) L1 L2 +. + +(* Basic inversion lemmas ***************************************************) + +fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → + ∀a,I,V,T. X = ⓑ{a,I}V.T → + llpx_sn R d V L1 L2 ∧ llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +#R #L1 #L2 #X #d * -L1 -L2 -X -d +[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct +| #L1 #L2 #d #i #_ #_ #b #J #W #U #H destruct +| #I #L1 #L2 #K1 #K2 #V1 #V2 #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 +] +qed-. + +lemma llpx_sn_inv_bind: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → + llpx_sn R d V L1 L2 ∧ llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +/2 width=4 by llpx_sn_inv_bind_aux/ qed-. + +fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → + ∀I,V,T. X = ⓕ{I}V.T → + llpx_sn R d V L1 L2 ∧ llpx_sn R d T L1 L2. +#R #L1 #L2 #X #d * -L1 -L2 -X -d +[ #L1 #L2 #d #k #_ #J #W #U #H destruct +| #L1 #L2 #d #i #_ #_ #J #W #U #H destruct +| #I #L1 #L2 #K1 #K2 #V1 #V2 #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 llpx_sn_inv_flat: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 → + llpx_sn R d V L1 L2 ∧ llpx_sn R d T L1 L2. +/2 width=4 by llpx_sn_inv_flat_aux/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma llpx_sn_fwd_length: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → |L1| = |L2|. +#R #L1 #L2 #T #d #H elim H -L1 -L2 -T -d // +#I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 +lapply (ldrop_fwd_length … HLK1) -HLK1 +lapply (ldrop_fwd_length … HLK2) -HLK2 +normalize // +qed-. + +lemma llpx_sn_fwd_ldrop_sn: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → + ∀K1,i. ⇩[i] L1 ≡ K1 → ∃K2. ⇩[i] L2 ≡ K2. +#R #L1 #L2 #T #d #H #K1 #i #HLK1 lapply (llpx_sn_fwd_length … H) -H +#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/ +qed-. + +lemma llpx_sn_fwd_ldrop_dx: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → + ∀K2,i. ⇩[i] L2 ≡ K2 → ∃K1. ⇩[i] L1 ≡ K1. +#R #L1 #L2 #T #d #H #K2 #i #HLK2 lapply (llpx_sn_fwd_length … H) -H +#HL12 lapply (ldrop_fwd_length_le2 … HLK2) -HLK2 /2 width=1 by ldrop_O1_le/ +qed-. + +fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → ∀i. X = #i → + ∨∨ |L1| ≤ i ∧ |L2| ≤ i + | yinj i < d + | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & + ⇩[i] L2 ≡ K2.ⓑ{I}V2 & + llpx_sn R (yinj 0) V1 K1 K2 & + R I K1 V1 V2 & d ≤ yinj i. +#R #L1 #L2 #X #d * -L1 -L2 -X -d +[ #L1 #L2 #d #k #_ #j #H destruct +| #L1 #L2 #d #i #_ #Hid #j #H destruct /2 width=1 by or3_intro1/ +| #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 #j #H destruct + /3 width=9 by or3_intro2, ex5_5_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-. + +lemma llpx_sn_fwd_lref: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → + ∨∨ |L1| ≤ i ∧ |L2| ≤ i + | yinj i < d + | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & + ⇩[i] L2 ≡ K2.ⓑ{I}V2 & + llpx_sn R (yinj 0) V1 K1 K2 & + R I K1 V1 V2 & d ≤ yinj i. +/2 width=3 by llpx_sn_fwd_lref_aux/ qed-. + +lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → + llpx_sn R d V L1 L2. +#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_bind … H) -H // +qed-. + +lemma llpx_sn_fwd_bind_dx: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → + llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +#R #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_bind … H) -H // +qed-. + +lemma llpx_sn_fwd_flat_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 → + llpx_sn R d V L1 L2. +#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_flat … H) -H // +qed-. + +lemma llpx_sn_fwd_flat_dx: ∀R,I,L1,L2,V,T,d. llpx_sn R d (ⓕ{I}V.T) L1 L2 → + llpx_sn R d T L1 L2. +#R #I #L1 #L2 #V #T #d #H elim (llpx_sn_inv_flat … H) -H // +qed-. + +lemma llpx_sn_fwd_pair_sn: ∀R,I,L1,L2,V,T,d. llpx_sn R d (②{I}V.T) L1 L2 → + llpx_sn R d V L1 L2. +#R * /2 width=4 by llpx_sn_fwd_flat_sn, llpx_sn_fwd_bind_sn/ +qed-. + +(* Basic_properties *********************************************************) + +lemma llpx_sn_refl: ∀R. (∀I,L. reflexive … (R I L)) → ∀T,L,d. llpx_sn R d T L L. +#R #HR #T #L @(f2_ind … rfw … L T) -L -T +#n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ +#i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/ +#HiL #d elim (ylt_split i d) /2 width=1 by llpx_sn_skip/ +elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=9 by llpx_sn_lref, ldrop_fwd_rfw/ +qed-. + +lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2. +#R #T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * /3 width=1 by llpx_sn_sort, llpx_sn_skip, llpx_sn_gref, llpx_sn_flat/ +#a #I #V1 #T1 #Hn #L2 #HL12 +@llpx_sn_bind /2 width=1/ (**) (* explicit constructor *) +@IH -IH // normalize /2 width=1 by eq_f2/ +qed-. + +lemma llpx_sn_ge_up: ∀R,L1,L2,U,dt. llpx_sn R dt U L1 L2 → ∀T,d,e. ⇧[d, e] T ≡ U → + dt ≤ d + e → llpx_sn R d U L1 L2. +#R #L1 #L2 #U #dt #H elim H -L1 -L2 -U -dt +[ #L1 #L2 #dt #k #HL12 #X #d #e #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #dt #i #HL12 #Hidt #X #d #e #H #Hdtde + elim (lift_inv_lref2 … H) -H * #Hid #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12 + elim (ylt_yle_false … Hidt) -Hidt + @(yle_trans … Hdtde) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *) +| #I #L1 #L2 #K1 #K2 #W1 #W2 #dt #i #Hdti #HLK1 #HLK2 #HW1 #HW12 #_ #X #d #e #H #_ + elim (lift_inv_lref2 … H) -H * #Hid #H destruct + [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12 + lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) + normalize in ⊢ (%→%→?); -I -W1 -W2 -dt /3 width=1 by llpx_sn_skip, ylt_inj/ + | /4 width=9 by llpx_sn_lref, yle_inj, le_plus_b/ + ] +| /2 width=1 by llpx_sn_free/ +| #L1 #L2 #dt #p #HL12 #X #d #e #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #dt #_ #_ #IHV #IHT #X #d #e #H #Hdtde destruct + elim (lift_inv_bind2 … H) -H #V #T #HVW >commutative_plus #HTU #H destruct + @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *) + @(IHT … HTU) /2 width=1 by yle_succ/ +| #I #L1 #L2 #W #U #dt #_ #_ #IHV #IHT #X #d #e #H #Hdtde destruct + elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct + /3 width=4 by llpx_sn_flat/ +] +qed-. + +(**) (* the minor premise comes first *) +lemma llpx_sn_ge: ∀R,L1,L2,T,d1,d2. d1 ≤ d2 → + llpx_sn R d1 T L1 L2 → llpx_sn R d2 T L1 L2. +#R #L1 #L2 #T #d1 #d2 * -d1 -d2 (**) (* destructed yle *) +/3 width=6 by llpx_sn_ge_up, llpx_sn_Y, llpx_sn_fwd_length, yle_inj/ +qed-. + +lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 → + llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → + llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2. +/3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-. + +lemma llpx_sn_co: ∀R1,R2. (∀I,L,T1,T2. R1 I L T1 T2 → R2 I L T1 T2) → + ∀L1,L2,T,d. llpx_sn R1 d T L1 L2 → llpx_sn R2 d T L1 L2. +#R1 #R2 #HR12 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d +/3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_alt.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_alt.etc new file mode 100644 index 000000000..0916edb67 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/llpx_sn_alt.etc @@ -0,0 +1,62 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/cofrees_alt.ma". +include "basic_2/substitution/llpx_sn_alt_rec.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* alternative definition of llpx_sn (not recursive) *) +definition llpx_sn_alt: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝ + λR,d,T,L1,L2. |L1| = |L2| ∧ + (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) → + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + I1 = I2 ∧ R I1 K1 V1 V2 + ). + +(* Main properties **********************************************************) + +theorem llpx_sn_llpx_sn_alt: ∀R,T,L1,L2,d. llpx_sn R d T L1 L2 → llpx_sn_alt R d T L1 L2. +#R #U #L1 @(f2_ind … rfw … L1 U) -L1 -U +#n #IHn #L1 #U #Hn #L2 #d #H elim (llpx_sn_inv_alt_r … H) -H +#HL12 #IHU @conj // +#I1 #I2 #K1 #K2 #V1 #V2 #i #Hdi #H #HLK1 #HLK2 elim (frees_inv_ge … H) -H // +[ -n #HnU elim (IHU … HnU HLK1 HLK2) -IHU -HnU -HLK1 -HLK2 /2 width=1 by conj/ +| * #J1 #K10 #W10 #j #Hdj #Hji #HLK10 #HnW10 #HnU destruct + lapply (ldrop_fwd_drop2 … HLK10) #H + lapply (ldrop_conf_ge … H … HLK1 ?) -H /2 width=1 by lt_to_le/ (minus_plus_m_m j (i+1)) in ⊢ (%→?); >commutative_plus (lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_sort/ +| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct + [ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_skip/ + | elim (ylt_yle_false … Hid0) -L1 -L2 -K1 -K2 -e -Hid0 + /3 width=3 by yle_trans, yle_inj/ + ] +| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct [ -HK12 | -IHK12 ] + [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 + elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 + /3 width=18 by llpx_sn_lref/ + | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hdi -Hd0 -K2 + /3 width=9 by llpx_sn_lref, yle_plus_dx1_trans/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e + /2 width=1 by llpx_sn_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_lift_ge: ∀R,K1,K2,T,d0. llpx_sn R d0 T K1 K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → llpx_sn R (d0+e) U L1 L2. +#R #K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0 +[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_sort/ +| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 + [ /3 width=3 by llpx_sn_skip, ylt_plus_dx2_trans/ + | /3 width=3 by llpx_sn_skip, monotonic_ylt_plus_dx/ + ] +| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e -Hid0 + /3 width=3 by ylt_yle_trans, ylt_inj/ + | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hid -Hd0 -K2 + /3 width=9 by llpx_sn_lref, monotonic_yle_plus_dx/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=5 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/ +] +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma llpx_sn_inv_lift_le: ∀R. (∀I. l_deliftable_sn (R I)) → + ∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2. +#R #HR #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + [ /2 width=1 by llpx_sn_skip/ + | /3 width=3 by llpx_sn_skip, yle_ylt_trans/ + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -HK12 | -IHK12 ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V1 #HKL1 #HKL11 #HVW1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V2 #HKL2 #HKL22 #HVW2 + elim (HR … HW12 … HKL11 … HVW1) -HR #V0 #HV0 #HV12 + lapply (lift_inj … HV0 … HVW2) -HV0 -HVW2 #H destruct + /3 width=10 by llpx_sn_lref/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 + elim (le_inv_plus_l … Hid) -Hid /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *) + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ yinj d + e → llpx_sn R d T K1 K2. +#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + -Hid0 /3 width=1 by llpx_sn_skip, ylt_inj/ + | elim (ylt_yle_false … Hid0) -L1 -L2 -Hd0 -Hid0 + /3 width=3 by yle_trans, yle_inj/ (**) (* slow *) + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hd0e -Hid0 + /3 width=3 by ylt_yle_trans, ylt_inj/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hd0e + elim (le_inv_plus_l … Hid) -Hid /3 width=9 by llpx_sn_lref, yle_inj/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_bind2 … H) -H + >commutative_plus #V #T #HVW #HTU #H destruct + @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) + @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, yle_succ/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ d0 → llpx_sn R (d0-e) T K1 K2. +#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -Hid0 | -Hded0 ] + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + [ /4 width=3 by llpx_sn_skip, yle_plus_to_minus_inj2, ylt_yle_trans, ylt_inj/ + | elim (le_inv_plus_l … Hid) -Hid #_ + /4 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx, yle_inj/ + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hid0 + /3 width=3 by yle_fwd_plus_sn1, ylt_yle_trans, ylt_inj/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 -Hid + /3 width=9 by llpx_sn_lref, monotonic_yle_minus_dx/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct + @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) + (lpx_sn_inv_atom1 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L1 #K1 #V1 #e #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct + elim (IHLK1 … HL12) -L1 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct + elim (HR … HV12 … HLK1 … HWV1) -V1 + elim (IHLK1 … HL12) -L1 /3 width=5 by ldrop_skip, lpx_sn_pair, ex2_intro/ +] +qed-. + +lemma lpx_sn_liftable_dedropable: ∀R. (∀I,L. reflexive ? (R I L)) → + (∀I. l_liftable (R I)) → dedropable_sn (lpx_sn R). +#R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H + /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lpx_sn_pair, monotonic_le_plus_l/ + @leq_O2 normalize // +| #I #L1 #K1 #V1 #e #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by ldrop_drop, leq_pair, lpx_sn_pair, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #d #e #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (lift_total W2 d e) #V2 #HWV2 + lapply (H2R … HW12 … HLK1 … HWV1 … HWV2) -W1 + elim (IHLK1 … HK12) -K1 + /3 width=6 by ldrop_skip, leq_succ, lpx_sn_pair, ex3_intro/ +] +qed-. + +fact lpx_sn_dropable_aux: ∀R,L2,K2,s,d,e. ⇩[s, d, e] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + d = 0 → ∃∃K1. ⇩[s, 0, e] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #s #d #e #H elim H -L2 -K2 -d -e +[ #d #e #He #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by ldrop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #e #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by ldrop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #d #e #_ #_ #_ #L1 #_ + (lpx_sn_inv_atom1 … H1) -X1 + >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/ +| #L0 #I #V0 #Hn #X1 #H1 #X2 #H2 destruct + elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH normalize // #L #HL1 #HL2 + elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lpx_sn_pair, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc new file mode 100644 index 000000000..2a3a87cf4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc @@ -0,0 +1,119 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair_refl: ∀R. (∀I,L. reflexive … (R I L)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,V. TC … (lpx_sn R) (L1.ⓑ{I}V) (L2. ⓑ{I}V). +#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 +[ /2 width=1 by lpx_sn_refl/ +| /3 width=1 by TC_reflexive, lpx_sn_refl/ +| /3 width=5 by lpx_sn_pair, step/ +] +qed-. + +lemma TC_lpx_sn_pair: ∀R. (∀I,L. reflexive … (R I L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … (R I) L1 V1 V2 → + TC … (lpx_sn R) (L1.ⓑ{I}V1) (L2. ⓑ{I}V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀I,L. reflexive … (R I L)) → + ∀L1,L2. lpx_sn (λI.LTC … (R I)) L1 L2 → + TC … (lpx_sn R) L1 L2. +#R #HR #L1 #L2 #H elim H -L1 -L2 +/2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L1 = K1.ⓑ{I}V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_ind: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → + ∀S:relation lenv. + S (⋆) (⋆) → ( + ∀I,K1,K2,V1,V2. + TC … (lpx_sn R) K1 K2 → LTC … (R I) K1 V1 V2 → + S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. +#R #HR #S #IH1 #IH2 #L2 elim L2 -L2 +[ #X #H >(TC_lpx_sn_inv_atom2 … H) -X // +| #L2 #I #V2 #IHL2 #X #H + elim (TC_lpx_sn_inv_pair2 … H) // -H -HR + #L1 #V1 #HL12 #HV12 #H destruct /3 width=1 by/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + lpx_sn (λI.LTC … (R I)) L1 L2. +/3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ssta_llpx_sn.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ssta_llpx_sn.etc new file mode 100644 index 000000000..3b1db6a9a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/ssta_llpx_sn.etc @@ -0,0 +1,44 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/substitution/llpx_sn_ldrop.ma". +include "basic_2/static/ssta.ma". + +(* STRATIFIED STATIC TYPE ASSIGNMENT FOR TERMS ******************************) + +(* Properties on lazy sn pointwise extensions *******************************) + +lemma ssta_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → + (∀I.l_liftable (R I)) → + ∀h,g,G. s_r_confluent1 … (ssta h g G) (llpx_sn R 0). +#R #H1R #H2R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 +[ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ +| #G #Ls #Ks #V1s #W2s #V2s #i #HLKs #_ #HVW2s #IHV12s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW2s) -HLKs -HLKd -HVW2s /2 width=1 by/ (**) (* full auto too slow *) +| #G #Ls #Ks #V1s #W1s #l #i #HLKs #Hl #HVW1s #Ld #H elim (llpx_sn_inv_lref_ge_sn … H … HLKs) // -H + #Kd #V1d #HLKd #HV1s #HV1sd + lapply (ldrop_fwd_drop2 … HLKs) -HLKs #HLKs + lapply (ldrop_fwd_drop2 … HLKd) -HLKd #HLKd + @(llpx_sn_lift_le … HLKs HLKd … HVW1s) -HLKs -HLKd -HVW1s /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_bind_O … H) -H + /4 width=5 by llpx_sn_bind_repl_SO, llpx_sn_bind/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +| #G #Ls #V #T1 #T2 #_ #IHT12 #Ld #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma index 4db858798..ec085821e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpr_llpx_sn.ma @@ -19,9 +19,7 @@ include "basic_2/reduction/cpr.ma". (* Properties on lazy sn pointwise extensions *******************************) -lemma cpr_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → - (∀I.l_liftable (R I)) → - (∀I.l_deliftable_sn (R I)) → +lemma cpr_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → ∀G. s_r_confluent1 … (cpr G) (llpx_sn R 0). #R #H1R #H2R #H3R #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma index 418106494..285157b45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_llpx_sn.ma @@ -20,9 +20,7 @@ include "basic_2/reduction/cpx.ma". (* Properties on lazy sn pointwise extensions *******************************) (* Note: lemma 1000 *) -lemma cpx_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → - (∀I.l_liftable (R I)) → - (∀I.l_deliftable_sn (R I)) → +lemma cpx_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → l_deliftable_sn R → ∀h,g,G. s_r_confluent1 … (cpx h g G) (llpx_sn R 0). #R #H1R #H2R #H3R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 [ // diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma index fd05f6373..01966eefb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpr.ma @@ -18,7 +18,7 @@ include "basic_2/reduction/cpr.ma". (* SN PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS *****************************) -definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (λ_.cpr G). +definition lpr: relation3 genv lenv lenv ≝ λG. lpx_sn (cpr G). interpretation "parallel reduction (local environment, sn variant)" 'PRedSn G L1 L2 = (lpr G L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma index 2482329c7..b10b13a28 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx.ma @@ -19,7 +19,7 @@ include "basic_2/reduction/cpx.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) definition lpx: ∀h. sd h → relation3 genv lenv lenv ≝ - λh,g,G. lpx_sn (λ_.cpx h g G). + λh,g,G. lpx_sn (cpx h g G). interpretation "extended parallel reduction (local environment, sn variant)" 'PRedSn h g G L1 L2 = (lpx h g G L1 L2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma index eb640da89..977fd887b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma @@ -16,16 +16,16 @@ include "basic_2/grammar/lenv_length.ma". (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) -inductive lpx_sn (R:relation4 bind2 lenv term term): relation lenv ≝ +inductive lpx_sn (R:relation3 lenv term term): relation lenv ≝ | lpx_sn_atom: lpx_sn R (⋆) (⋆) | lpx_sn_pair: ∀I,K1,K2,V1,V2. - lpx_sn R K1 K2 → R I K1 V1 V2 → - lpx_sn R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + lpx_sn R K1 K2 → R K1 V1 V2 → + lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) . (* Basic properties *********************************************************) -lemma lpx_sn_refl: ∀R. (∀I,L. reflexive ? (R I L)) → reflexive … (lpx_sn R). +lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). #R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/ qed-. @@ -41,16 +41,16 @@ qed-. lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. /2 width=4 by lpx_sn_inv_atom1_aux/ qed-. -fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2. +fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. #R #L1 #L2 * -L1 -L2 [ #J #K1 #V1 #H destruct | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. lpx_sn R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2. +lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → + ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by lpx_sn_inv_pair1_aux/ qed-. fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. @@ -63,21 +63,21 @@ qed-. lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. /2 width=4 by lpx_sn_inv_atom2_aux/ qed-. -fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2.ⓑ{I}V2 → - ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1. +fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. #R #L1 #L2 * -L1 -L2 [ #J #K2 #V2 #H destruct | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. lpx_sn R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1. +lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → + ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. /2 width=3 by lpx_sn_inv_pair2_aux/ qed-. lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) → - ∧∧ lpx_sn R L1 L2 & R I1 L1 V1 V2 & I1 = I2. + ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2. #R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H #L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma index 8a0aa3931..4f9ae350b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_alt.ma @@ -18,11 +18,11 @@ include "basic_2/relocation/lpx_sn.ma". (* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) (* alternative definition of lpx_sn *) -definition lpx_sn_alt: relation4 bind2 lenv term term → relation lenv ≝ +definition lpx_sn_alt: relation3 lenv term term → relation lenv ≝ λR,L1,L2. |L1| = |L2| ∧ (∀I1,I2,K1,K2,V1,V2,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R I1 K1 V1 V2 + I1 = I2 ∧ R K1 V1 V2 ). (* Basic forward lemmas ******************************************************) @@ -39,7 +39,7 @@ normalize /2 width=1 by length_inv_zero_sn/ qed-. lemma lpx_sn_alt_inv_pair1: ∀R,I,L2,K1,V1. lpx_sn_alt R (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L2 = K2.ⓑ{I}V2. + ∃∃K2,V2. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L2 = K2.ⓑ{I}V2. #R #I1 #L2 #K1 #V1 #H elim H -H #H #IH elim (length_inv_pos_sn … H) -H #I2 #K2 #V2 #HK12 #H destruct @@ -56,7 +56,7 @@ normalize /2 width=1 by length_inv_zero_dx/ qed-. lemma lpx_sn_alt_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn_alt R L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. lpx_sn_alt R K1 K2 & R I K1 V1 V2 & L1 = K1.ⓑ{I}V1. + ∃∃K1,V1. lpx_sn_alt R K1 K2 & R K1 V1 V2 & L1 = K1.ⓑ{I}V1. #R #I2 #L1 #K2 #V2 #H elim H -H #H #IH elim (length_inv_pos_dx … H) -H #I1 #K1 #V1 #HK12 #H destruct @@ -76,7 +76,7 @@ lemma lpx_sn_alt_atom: ∀R. lpx_sn_alt R (⋆) (⋆). qed. lemma lpx_sn_alt_pair: ∀R,I,L1,L2,V1,V2. - lpx_sn_alt R L1 L2 → R I L1 V1 V2 → + lpx_sn_alt R L1 L2 → R L1 V1 V2 → lpx_sn_alt R (L1.ⓑ{I}V1) (L2.ⓑ{I}V2). #R #I #L1 #L2 #V1 #V2 #H #HV12 elim H -H #HL12 #IH @conj normalize // @@ -111,7 +111,7 @@ qed-. lemma lpx_sn_intro_alt: ∀R,L1,L2. |L1| = |L2| → (∀I1,I2,K1,K2,V1,V2,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R I1 K1 V1 V2 + I1 = I2 ∧ R K1 V1 V2 ) → lpx_sn R L1 L2. /4 width=4 by lpx_sn_alt_inv_lpx_sn, conj/ qed. @@ -119,7 +119,7 @@ lemma lpx_sn_inv_alt: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2| ∧ ∀I1,I2,K1,K2,V1,V2,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R I1 K1 V1 V2. + I1 = I2 ∧ R K1 V1 V2. #R #L1 #L2 #H lapply (lpx_sn_lpx_sn_alt … H) -H #H elim H -H /3 width=4 by conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_ldrop.ma index 2b44e20fb..1edda7640 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_ldrop.ma @@ -21,7 +21,7 @@ include "basic_2/relocation/lpx_sn.ma". lemma lpx_sn_ldrop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1,i. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R I K1 V1 V2. + ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. #R #L1 #L2 #H elim H -L1 -L2 [ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H @@ -34,7 +34,7 @@ qed-. lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2,i. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R I K1 V1 V2. + ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. #R #L1 #L2 #H elim H -L1 -L2 [ #I0 #K0 #V0 #i #H elim (ldrop_inv_atom1 … H) -H #H destruct | #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (ldrop_inv_O1_pair1 … H) * -H @@ -45,7 +45,7 @@ lemma lpx_sn_ldrop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → ] qed-. -lemma lpx_sn_deliftable_dropable: ∀R. (∀I. l_deliftable_sn (R I)) → dropable_sn (lpx_sn R). +lemma lpx_sn_deliftable_dropable: ∀R. l_deliftable_sn R → dropable_sn (lpx_sn R). #R #HR #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H /4 width=3 by ldrop_atom, lpx_sn_atom, ex2_intro/ @@ -62,8 +62,8 @@ lemma lpx_sn_deliftable_dropable: ∀R. (∀I. l_deliftable_sn (R I)) → dropab ] qed-. -lemma lpx_sn_liftable_dedropable: ∀R. (∀I,L. reflexive ? (R I L)) → - (∀I. l_liftable (R I)) → dedropable_sn (lpx_sn R). +lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → + l_liftable R → dedropable_sn (lpx_sn R). #R #H1R #H2R #L1 #K1 #s #d #e #H elim H -L1 -K1 -d -e [ #d #e #He #X #H >(lpx_sn_inv_atom1 … H) -H /4 width=4 by ldrop_atom, lpx_sn_atom, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_lpx_sn.ma index bd72cf61e..5d72fb119 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_lpx_sn.ma @@ -18,23 +18,23 @@ include "basic_2/relocation/lpx_sn.ma". definition lpx_sn_confluent: relation (relation3 lenv term term) ≝ λR1,R2. ∀L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → - ∀L1. lpx_sn (λ_.R1) L0 L1 → ∀L2. lpx_sn (λ_.R2) L0 L2 → + ∀L1. lpx_sn R1 L0 L1 → ∀L2. lpx_sn R2 L0 L2 → ∃∃T. R2 L1 T1 T & R1 L2 T2 T. definition lpx_sn_transitive: relation (relation3 lenv term term) ≝ λR1,R2. - ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn (λ_.R1) L1 L2 → + ∀L1,T1,T. R1 L1 T1 T → ∀L2. lpx_sn R1 L1 L2 → ∀T2. R2 L2 T T2 → R1 L1 T1 T2. (* Main properties **********************************************************) -theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn (λ_.R)). +theorem lpx_sn_trans: ∀R. lpx_sn_transitive R R → Transitive … (lpx_sn R). #R #HR #L1 #L #H elim H -L1 -L // #I #L1 #L #V1 #V #HL1 #HV1 #IHL1 #X #H elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL2 #HV2 #H destruct /3 width=5 by lpx_sn_pair/ qed-. theorem lpx_sn_conf: ∀R1,R2. lpx_sn_confluent R1 R2 → - confluent2 … (lpx_sn (λ_.R1)) (lpx_sn (λ_.R2)). + confluent2 … (lpx_sn R1) (lpx_sn R2). #R1 #R2 #HR12 #L0 @(f_ind … length … L0) -L0 #n #IH * [ #_ #X1 #H1 #X2 #H2 -n >(lpx_sn_inv_atom1 … H1) -X1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma index 2a3a87cf4..e994bf076 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_tc.ma @@ -18,9 +18,9 @@ include "basic_2/relocation/lpx_sn.ma". (* Properties on transitive_closure *****************************************) -lemma TC_lpx_sn_pair_refl: ∀R. (∀I,L. reflexive … (R I L)) → +lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,V. TC … (lpx_sn R) (L1.ⓑ{I}V) (L2. ⓑ{I}V). + ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). #R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 [ /2 width=1 by lpx_sn_refl/ | /3 width=1 by TC_reflexive, lpx_sn_refl/ @@ -28,18 +28,18 @@ lemma TC_lpx_sn_pair_refl: ∀R. (∀I,L. reflexive … (R I L)) → ] qed-. -lemma TC_lpx_sn_pair: ∀R. (∀I,L. reflexive … (R I L)) → +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → - ∀V1,V2. LTC … (R I) L1 V1 V2 → - TC … (lpx_sn R) (L1.ⓑ{I}V1) (L2. ⓑ{I}V2). + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). #R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // [ /2 width=1 by TC_lpx_sn_pair_refl/ | /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ ] qed-. -lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀I,L. reflexive … (R I L)) → - ∀L1,L2. lpx_sn (λI.LTC … (R I)) L1 L2 → +lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. lpx_sn (LTC … R) L1 L2 → TC … (lpx_sn R) L1 L2. #R #HR #L1 #L2 #H elim H -L1 -L2 /2 width=1 by TC_lpx_sn_pair, lpx_sn_atom, inj/ @@ -54,9 +54,9 @@ lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. ] qed-. -lemma TC_lpx_sn_inv_pair2: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L1 = K1.ⓑ{I}V1. + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. #R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 [ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ | #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct @@ -65,11 +65,11 @@ lemma TC_lpx_sn_inv_pair2: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) ] qed-. -lemma TC_lpx_sn_ind: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → +lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀S:relation lenv. S (⋆) (⋆) → ( ∀I,K1,K2,V1,V2. - TC … (lpx_sn R) K1 K2 → LTC … (R I) K1 V1 V2 → + TC … (lpx_sn R) K1 K2 → LTC … R K1 V1 V2 → S K1 K2 → S (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) ) → ∀L2,L1. TC … (lpx_sn R) L1 L2 → S L1 L2. @@ -88,24 +88,24 @@ lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. ] qed-. -fact TC_lpx_sn_inv_pair1_aux: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2. + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. #R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 [ #J #K #W #H destruct | #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma TC_lpx_sn_inv_pair1: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … (R I) K1 V1 V2 & L2 = K2. ⓑ{I} V2. + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. (∀I.s_rs_transitive … (R I) (λ_.lpx_sn R)) → +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → - lpx_sn (λI.LTC … (R I)) L1 L2. + lpx_sn (LTC … R) L1 L2. /3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. (* Forward lemmas on transitive closure *************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma index 3b1db6a9a..0d08b9f5d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ssta_llpx_sn.ma @@ -19,8 +19,7 @@ include "basic_2/static/ssta.ma". (* Properties on lazy sn pointwise extensions *******************************) -lemma ssta_llpx_sn_conf: ∀R. (∀I,L.reflexive … (R I L)) → - (∀I.l_liftable (R I)) → +lemma ssta_llpx_sn_conf: ∀R. (∀L. reflexive … (R L)) → l_liftable R → ∀h,g,G. s_r_confluent1 … (ssta h g G) (llpx_sn R 0). #R #H1R #H2R #h #g #G #Ls #T1 #T2 #H elim H -G -Ls -T1 -T2 [ /3 width=4 by llpx_sn_fwd_length, llpx_sn_sort/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index dc138a492..92dffd80f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -17,7 +17,7 @@ include "basic_2/substitution/llpx_sn.ma". (* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -definition ceq: relation4 bind2 lenv term term ≝ λI,L,T1,T2. T1 = T2. +definition ceq: relation3 lenv term term ≝ λL,T1,T2. T1 = T2. definition lleq: relation4 ynat term lenv lenv ≝ llpx_sn ceq. @@ -25,8 +25,8 @@ interpretation "lazy equivalence (local environment)" 'LazyEq T d L1 L2 = (lleq d T L1 L2). -definition lleq_transitive: predicate (relation4 bind2 lenv term term) ≝ - λR. ∀I,L2,T1,T2. R I L2 T1 T2 → ∀L1. L1 ≡[T1, 0] L2 → R I L1 T1 T2. +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. (* Basic inversion lemmas ***************************************************) @@ -155,6 +155,6 @@ lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ≡[V, 0] L2 → L1.ⓑ{I}V ≡[T, 0] L2 (* Advancded properties on lazy pointwise exyensions ************************) -lemma llpx_sn_lrefl: ∀R. (∀I,L. reflexive … (R I L)) → +lemma llpx_sn_lrefl: ∀R. (∀L. reflexive … (R L)) → ∀L1,L2,T,d. L1 ≡[T, d] L2 → llpx_sn R d T L1 L2. /2 width=3 by llpx_sn_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma new file mode 100644 index 000000000..9d0122cca --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/lazyor_4.ma". +include "basic_2/relocation/lpx_sn.ma". +include "basic_2/substitution/cofrees.ma". + +(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) + +inductive clor (T) (L2) (K1) (V1): predicate term ≝ +| clor_sn: |K1| < |L2| → K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → clor T L2 K1 V1 V1 +| clor_dx: ∀I,K2,V2. |K1| < |L2| → (K1 ⊢ |L2|-|K1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → + ⇩[|L2|-|K1|-1] L2 ≡ K2.ⓑ{I}V2 → clor T L2 K1 V1 V2 +. + +definition llor: relation4 term lenv lenv lenv ≝ + λT,L2. lpx_sn (clor T L2). + +interpretation + "lazy union (local environment)" + 'LazyOr L1 T L2 L = (llor T L2 L1 L). + +(* Basic properties *********************************************************) + +lemma llor_pair_sn: ∀I,L1,L2,L,V,T. L1 ⩖[T] L2 ≡ L → + |L1| < |L2| → L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → + L1.ⓑ{I}V ⩖[T] L2 ≡ L.ⓑ{I}V. +/3 width=2 by clor_sn, lpx_sn_pair/ qed. + +lemma llor_pair_dx: ∀I,J,L1,L2,L,K2,V1,V2,T. L1 ⩖[T] L2 ≡ L → + |L1| < |L2| → (L1 ⊢ |L2|-|L1|-1 ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → + ⇩[|L2|-|L1|-1] L2 ≡ K2.ⓑ{J}V2 → + L1.ⓑ{I}V1 ⩖[T] L2 ≡ L.ⓑ{I}V2. +/4 width=3 by clor_dx, lpx_sn_pair/ qed. + +lemma llor_total: ∀T,L2,L1. |L1| ≤ |L2| → ∃L. L1 ⩖[T] L2 ≡ L. +#T #L2 #L1 elim L1 -L1 /2 width=2 by ex_intro/ +#L1 #I1 #V1 #IHL1 normalize +#H elim IHL1 -IHL1 /2 width=3 by transitive_le/ +#L #HT elim (cofrees_dec L1 T 0 (|L2|-|L1|-1)) +[ /3 width=2 by llor_pair_sn, ex_intro/ +| elim (ldrop_O1_lt (Ⓕ) L2 (|L2|-|L1|-1)) + /5 width=4 by llor_pair_dx, monotonic_lt_minus_l, ex_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma new file mode 100644 index 000000000..b62a00263 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llor_alt.ma @@ -0,0 +1,66 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lpx_sn_alt.ma". +include "basic_2/substitution/llor.ma". + +(* POINTWISE UNION FOR LOCAL ENVIRONMENTS ***********************************) + +(* Alternative definition ***************************************************) + +theorem llor_intro_alt: ∀T,L2,L1,L. |L1| ≤ |L2| → |L1| = |L| → + (∀I1,I,K1,K,V1,V,i. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L ≡ K.ⓑ{I}V → + (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → I1 = I ∧ V1 = V) ∧ + (∀I2,K2,V2. (K1 ⊢ |L2|-|L1|+i ~ϵ 𝐅*[yinj 0]⦃T⦄ → ⊥) → + ⇩[|L2|-|L1|+i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I ∧ V2 = V + ) + ) → L1 ⩖[T] L2 ≡ L. +#T #L2 #L1 #L #HL12 #HL1 #IH @lpx_sn_intro_alt // -HL1 +#I1 #I #K1 #K #V1 #V #i #HLK1 #HLK +lapply (ldrop_fwd_length_minus4 … HLK1) +lapply (ldrop_fwd_length_le4 … HLK1) +normalize in ⊢ (%→%→?); #HKL1 #Hi +lapply (plus_minus_minus_be_aux … HL12 Hi) // -Hi Hi -Hi +elim (IH … HLK1 HLK) -IH #HI1 * +/4 width=5 by or_introl, or_intror, and3_intro, ex4_3_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma index 918b42605..4c4fd5edb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn.ma @@ -17,12 +17,12 @@ include "basic_2/relocation/ldrop.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) -inductive llpx_sn (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝ +inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝ | llpx_sn_sort: ∀L1,L2,d,k. |L1| = |L2| → llpx_sn R d (⋆k) L1 L2 | llpx_sn_skip: ∀L1,L2,d,i. |L1| = |L2| → yinj i < d → llpx_sn R d (#i) L1 L2 | llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 → - llpx_sn R (yinj 0) V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d (#i) L1 L2 + llpx_sn R (yinj 0) V1 K1 K2 → R K1 V1 V2 → llpx_sn R d (#i) L1 L2 | llpx_sn_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → llpx_sn R d (#i) L1 L2 | llpx_sn_gref: ∀L1,L2,d,p. |L1| = |L2| → llpx_sn R d (§p) L1 L2 | llpx_sn_bind: ∀a,I,L1,L2,V,T,d. @@ -98,7 +98,7 @@ fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,d. llpx_sn R d X L1 L2 → ∀i. X = #i | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R (yinj 0) V1 K1 K2 & - R I K1 V1 V2 & d ≤ yinj i. + R K1 V1 V2 & d ≤ yinj i. #R #L1 #L2 #X #d * -L1 -L2 -X -d [ #L1 #L2 #d #k #_ #j #H destruct | #L1 #L2 #d #i #_ #Hid #j #H destruct /2 width=1 by or3_intro1/ @@ -117,7 +117,7 @@ lemma llpx_sn_fwd_lref: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R (yinj 0) V1 K1 K2 & - R I K1 V1 V2 & d ≤ yinj i. + R K1 V1 V2 & d ≤ yinj i. /2 width=3 by llpx_sn_fwd_lref_aux/ qed-. lemma llpx_sn_fwd_bind_sn: ∀R,a,I,L1,L2,V,T,d. llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → @@ -147,7 +147,7 @@ qed-. (* Basic_properties *********************************************************) -lemma llpx_sn_refl: ∀R. (∀I,L. reflexive … (R I L)) → ∀T,L,d. llpx_sn R d T L L. +lemma llpx_sn_refl: ∀R. (∀L. reflexive … (R L)) → ∀T,L,d. llpx_sn R d T L L. #R #HR #T #L @(f2_ind … rfw … L T) -L -T #n #IH #L * * /3 width=1 by llpx_sn_sort, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ #i #Hn elim (lt_or_ge i (|L|)) /2 width=1 by llpx_sn_free/ @@ -202,7 +202,7 @@ lemma llpx_sn_bind_O: ∀R,a,I,L1,L2,V,T. llpx_sn R 0 V L1 L2 → llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2. /3 width=3 by llpx_sn_ge, llpx_sn_bind/ qed-. -lemma llpx_sn_co: ∀R1,R2. (∀I,L,T1,T2. R1 I L T1 T2 → R2 I L T1 T2) → +lemma llpx_sn_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T,d. llpx_sn R1 d T L1 L2 → llpx_sn R2 d T L1 L2. #R1 #R2 #HR12 #L1 #L2 #T #d #H elim H -L1 -L2 -T -d /3 width=9 by llpx_sn_sort, llpx_sn_skip, llpx_sn_lref, llpx_sn_free, llpx_sn_gref, llpx_sn_bind, llpx_sn_flat/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma index 0916edb67..b2792cee2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt.ma @@ -18,11 +18,11 @@ include "basic_2/substitution/llpx_sn_alt_rec.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) (* alternative definition of llpx_sn (not recursive) *) -definition llpx_sn_alt: relation4 bind2 lenv term term → relation4 ynat term lenv lenv ≝ +definition llpx_sn_alt: relation3 lenv term term → relation4 ynat term lenv lenv ≝ λR,d,T,L1,L2. |L1| = |L2| ∧ (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (L1 ⊢ i ~ϵ 𝐅*[d]⦃T⦄ → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - I1 = I2 ∧ R I1 K1 V1 V2 + I1 = I2 ∧ R K1 V1 V2 ). (* Main properties **********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt_rec.ma index 2671af0eb..7236ff44b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt_rec.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_alt_rec.ma @@ -19,10 +19,10 @@ include "basic_2/substitution/llpx_sn.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) (* alternative definition of llpx_sn (recursive) *) -inductive llpx_sn_alt_r (R:relation4 bind2 lenv term term): relation4 ynat term lenv lenv ≝ +inductive llpx_sn_alt_r (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝ | llpx_sn_alt_r_intro: ∀L1,L2,T,d. (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R I1 K1 V1 V2 + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → I1 = I2 ∧ R K1 V1 V2 ) → (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → llpx_sn_alt_r R 0 V1 K1 K2 @@ -33,8 +33,8 @@ inductive llpx_sn_alt_r (R:relation4 bind2 lenv term term): relation4 ynat term lemma llpx_sn_alt_r_intro_alt: ∀R,L1,L2,T,d. |L1| = |L2| → (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 ) → llpx_sn_alt_r R d T L1 L2. #R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_intro // -HL12 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 @@ -45,7 +45,7 @@ lemma llpx_sn_alt_r_ind_alt: ∀R. ∀S:relation4 ynat term lenv lenv. (∀L1,L2,T,d. |L1| = |L2| → ( ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2 + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2 & S 0 V1 K1 K2 ) → S d T L1 L2) → ∀L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → S d T L1 L2. #R #S #IH #L1 #L2 #T #d #H elim H -L1 -L2 -T -d @@ -57,8 +57,8 @@ qed-. lemma llpx_sn_alt_r_inv_alt: ∀R,L1,L2,T,d. llpx_sn_alt_r R d T L1 L2 → |L1| = |L2| ∧ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → - ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2. + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn_alt_r R 0 V1 K1 K2. #R #L1 #L2 #T #d #H @(llpx_sn_alt_r_ind_alt … H) -L1 -L2 -T -d #L1 #L2 #T #d #HL12 #IH @conj // -HL12 #I1 #I2 #K1 #K2 #V1 #V2 #i #Hid #HnT #HLK1 #HLK2 @@ -103,7 +103,7 @@ lemma llpx_sn_alt_r_fwd_lref: ∀R,L1,L2,d,i. llpx_sn_alt_r R d (#i) L1 L2 → | ∃∃I,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn_alt_r R (yinj 0) V1 K1 K2 & - R I K1 V1 V2 & d ≤ yinj i. + R K1 V1 V2 & d ≤ yinj i. #R #L1 #L2 #d #i #H elim (llpx_sn_alt_r_inv_alt … H) -H #HL12 #IH elim (lt_or_ge i (|L1|)) /3 width=1 by or3_intro0, conj/ elim (ylt_split i d) /3 width=1 by or3_intro1/ @@ -141,7 +141,7 @@ qed. lemma llpx_sn_alt_r_lref: ∀R,I,L1,L2,K1,K2,V1,V2,d,i. d ≤ yinj i → ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ⇩[i] L2 ≡ K2.ⓑ{I}V2 → - llpx_sn_alt_r R 0 V1 K1 K2 → R I K1 V1 V2 → + llpx_sn_alt_r R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn_alt_r R d (#i) L1 L2. #R #I #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hdi #HLK1 #HLK2 #HK12 #HV12 @llpx_sn_alt_r_intro_alt [ lapply (llpx_sn_alt_r_fwd_length … HK12) -HK12 #HK12 @@ -215,7 +215,7 @@ qed-. lemma llpx_sn_intro_alt_r: ∀R,L1,L2,T,d. |L1| = |L2| → (∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2 + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 ) → llpx_sn R d T L1 L2. #R #L1 #L2 #T #d #HL12 #IH @llpx_sn_alt_r_inv_lpx_sn @llpx_sn_alt_r_intro_alt // -HL12 @@ -227,7 +227,7 @@ lemma llpx_sn_ind_alt_r: ∀R. ∀S:relation4 ynat term lenv lenv. (∀L1,L2,T,d. |L1| = |L2| → ( ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2 + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2 & S 0 V1 K1 K2 ) → S d T L1 L2) → ∀L1,L2,T,d. llpx_sn R d T L1 L2 → S d T L1 L2. #R #S #IH1 #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H @@ -241,7 +241,7 @@ lemma llpx_sn_inv_alt_r: ∀R,L1,L2,T,d. llpx_sn R d T L1 L2 → |L1| = |L2| ∧ ∀I1,I2,K1,K2,V1,V2,i. d ≤ yinj i → (∀U. ⇧[i, 1] U ≡ T → ⊥) → ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & R I1 K1 V1 V2 & llpx_sn R 0 V1 K1 K2. + ∧∧ I1 = I2 & R K1 V1 V2 & llpx_sn R 0 V1 K1 K2. #R #L1 #L2 #T #d #H lapply (llpx_sn_lpx_sn_alt_r … H) -H #H elim (llpx_sn_alt_r_inv_alt … H) -H #HL12 #IH @conj // diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma index 509a836b3..749407b4f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_ldrop.ma @@ -23,7 +23,7 @@ lemma llpx_sn_fwd_lref_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → i < d ∨ ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & llpx_sn R 0 V1 K1 K2 & - R I K1 V1 V2 & d ≤ i. + R K1 V1 V2 & d ≤ i. #R #L1 #L2 #d #i #H #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref … H) -H [ * || * ] [ #_ #H elim (lt_refl_false i) lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 @@ -39,7 +39,7 @@ lemma llpx_sn_fwd_lref_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → i < d ∨ ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R 0 V1 K1 K2 & - R I K1 V1 V2 & d ≤ i. + R K1 V1 V2 & d ≤ i. #R #L1 #L2 #d #i #H #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref … H) -H [ * || * ] [ #H #_ elim (lt_refl_false i) lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1 @@ -56,7 +56,7 @@ qed-. lemma llpx_sn_inv_lref_ge_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & - llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2. + llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. #R #L1 #L2 #d #i #H #Hdi #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2 [ #H elim (ylt_yle_false … H Hdi) | * /2 width=5 by ex3_2_intro/ @@ -66,7 +66,7 @@ qed-. lemma llpx_sn_inv_lref_ge_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & - llpx_sn R 0 V1 K1 K2 & R I K1 V1 V2. + llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. #R #L1 #L2 #d #i #H #Hdi #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1 [ #H elim (ylt_yle_false … H Hdi) | * /2 width=5 by ex3_2_intro/ @@ -76,7 +76,7 @@ qed-. lemma llpx_sn_inv_lref_ge_bi: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → ∀I1,I2,K1,K2,V1,V2. ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → - ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R I1 K1 V1 V2. + ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. #R #L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 elim (llpx_sn_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d #J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by and3_intro/ @@ -84,7 +84,7 @@ qed-. fact llpx_sn_inv_S_aux: ∀R,L1,L2,T,d0. llpx_sn R d0 T L1 L2 → ∀d. d0 = d + 1 → ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 → - llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2. + llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2. #R #L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0 /2 width=1 by llpx_sn_gref, llpx_sn_free, llpx_sn_sort/ [ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V1 #V2 #HLK1 #HLK2 #HK12 #HV12 destruct @@ -101,10 +101,10 @@ qed-. lemma llpx_sn_inv_S: ∀R,L1,L2,T,d. llpx_sn R (d + 1) T L1 L2 → ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 → - llpx_sn R 0 V1 K1 K2 → R I K1 V1 V2 → llpx_sn R d T L1 L2. + llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2. /2 width=9 by llpx_sn_inv_S_aux/ qed-. -lemma llpx_sn_inv_bind_O: ∀R. (∀I,L. reflexive … (R I L)) → +lemma llpx_sn_inv_bind_O: ∀R. (∀L. reflexive … (R L)) → ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → llpx_sn R 0 V L1 L2 ∧ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V). #R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind … H) -H @@ -113,7 +113,7 @@ qed-. (* More advanced forward lemmas *********************************************) -lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀I,L. reflexive … (R I L)) → +lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀L. reflexive … (R L)) → ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V). #R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind_O … H) -H // @@ -122,10 +122,10 @@ qed-. (* Advanced properties ******************************************************) lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) → - ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R J L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2). + ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2). /3 width=9 by llpx_sn_bind_repl_SO, llpx_sn_inv_S/ qed-. -lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) → +lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀T,L1,L2,d. Decidable (llpx_sn R d T L1 L2). #R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * * @@ -137,7 +137,7 @@ lemma llpx_sn_dec: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) → elim (ldrop_O1_lt (Ⓕ) … HiL2) #I2 #K2 #V2 #HLK2 elim (ldrop_O1_lt (Ⓕ) … HiL1) #I1 #K1 #V1 #HLK1 elim (eq_bind2_dec I2 I1) - [ #H2 elim (HR I1 K1 V1 V2) -HR + [ #H2 elim (HR K1 V1 V2) -HR [ #H3 elim (IH K1 V1 … K2 0) destruct /3 width=9 by llpx_sn_lref, ldrop_fwd_rfw, or_introl/ ] @@ -169,7 +169,7 @@ qed-. (* Properties on relocation *************************************************) -lemma llpx_sn_lift_le: ∀R. (∀I. l_liftable (R I)) → +lemma llpx_sn_lift_le: ∀R. l_liftable R → ∀K1,K2,T,d0. llpx_sn R d0 T K1 K2 → ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 U L1 L2. @@ -252,7 +252,7 @@ qed-. (* Inversion lemmas on relocation *******************************************) -lemma llpx_sn_inv_lift_le: ∀R. (∀I. l_deliftable_sn (R I)) → +lemma llpx_sn_inv_lift_le: ∀R. l_deliftable_sn R → ∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 → ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2. @@ -409,21 +409,21 @@ qed-. (* Inversion lemmas on negated lazy pointwise extension *********************) -lemma nllpx_sn_inv_bind: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) → +lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀a,I,L1,L2,V,T,d. (llpx_sn R d (ⓑ{a,I}V.T) L1 L2 → ⊥) → (llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R (⫯d) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥). #R #HR #a #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d) /4 width=1 by llpx_sn_bind, or_intror, or_introl/ qed-. -lemma nllpx_sn_inv_flat: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) → +lemma nllpx_sn_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀I,L1,L2,V,T,d. (llpx_sn R d (ⓕ{I}V.T) L1 L2 → ⊥) → (llpx_sn R d V L1 L2 → ⊥) ∨ (llpx_sn R d T L1 L2 → ⊥). #R #HR #I #L1 #L2 #V #T #d #H elim (llpx_sn_dec … HR V L1 L2 d) /4 width=1 by llpx_sn_flat, or_intror, or_introl/ qed-. -lemma nllpx_sn_inv_bind_O: ∀R. (∀I,L,T1,T2. Decidable (R I L T1 T2)) → +lemma nllpx_sn_inv_bind_O: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀a,I,L1,L2,V,T. (llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → ⊥) → (llpx_sn R 0 V L1 L2 → ⊥) ∨ (llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥). #R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_dec … HR V L1 L2 0) diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma index 21a88ca0e..6a0a210ca 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_lpx_sn.ma @@ -19,7 +19,7 @@ include "basic_2/substitution/llpx_sn.ma". (* Properties on pointwise extensions ***************************************) -lemma lpx_sn_llpx_sn: ∀R. (∀I,L. reflexive … (R I L)) → +lemma lpx_sn_llpx_sn: ∀R. (∀L. reflexive … (R L)) → ∀T,L1,L2,d. lpx_sn R L1 L2 → llpx_sn R d T L1 L2. #R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #n #IH #L1 * * diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma index d22e09069..1ab9a7984 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/llpx_sn_tc.ma @@ -18,8 +18,8 @@ include "basic_2/substitution/llpx_sn_ldrop.ma". (* Properties about transitive closure **************************************) -lemma llpx_sn_TC_pair_dx: ∀R. (∀I,L. reflexive … (R I L)) → - ∀I,L,V1,V2,T. LTC … (R I) L V1 V2 → +lemma llpx_sn_TC_pair_dx: ∀R. (∀L. reflexive … (R L)) → + ∀I,L,V1,V2,T. LTC … R L V1 V2 → LTC … (llpx_sn R 0) T (L.ⓑ{I}V1) (L.ⓑ{I}V2). #R #HR #I #L #V1 #V2 #T #H @(TC_star_ind … V2 H) -V2 /4 width=9 by llpx_sn_bind_repl_O, llpx_sn_refl, step, inj/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index e501a1f69..54cb06e9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -219,7 +219,7 @@ table { } ] [ { "pointwise union for local environments" * } { - [ "llor ( ? ⩖[?] ? ≡ ? )" * ] + [ "llor ( ? ⩖[?] ? ≡ ? )" "llor_alt" * ] } ] [ { "context-sensitive exclusion from free variables" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma index 3eec591c6..dcf7e2de0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma @@ -19,6 +19,14 @@ include "ground_2/lib/star.ma". (* Equations ****************************************************************) +(* Note: uses minus_minus_comm, minus_plus_m_m, commutative_plus, plus_minus *) +lemma plus_minus_minus_be: ∀x,y,z. y ≤ z → z ≤ x → (x - z) + (z - y) = x - y. +#x #z #y #Hzy #Hyx >plus_minus // >commutative_plus >plus_minus // +qed-. + +fact plus_minus_minus_be_aux: ∀i,x,y,z. y ≤ z → z ≤ x → i = z - y → x - z + i = x - y. +/2 width=1 by plus_minus_minus_be/ qed-. + lemma plus_n_2: ∀n. n + 2 = n + 1 + 1. // qed. -- 2.39.2