From: Ferruccio Guidi Date: Fri, 10 Jan 2014 18:05:18 +0000 (+0000) Subject: new definition of lleq allows to complete the proof of lemma 1000 X-Git-Tag: make_still_working~1002 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dca4170c5ce5f2cd6be8ae1dc0422bd6a680b43f;p=helm.git new definition of lleq allows to complete the proof of lemma 1000 (lleq_cpx_conf_dx)! --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma index f8790c5d9..6c5b811eb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/reduction/lpx_leq.ma". +include "basic_2/reduction/cpx_lleq.ma". include "basic_2/computation/cpxs.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) @@ -20,12 +20,12 @@ include "basic_2/computation/cpxs.ma". (* Properties on lazy equivalence for local environments ********************) lemma lleq_cpxs_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. + ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2. #h #g #G #L2 #T1 #T2 #H @(cpxs_ind_dx … H) -T1 /4 width=6 by lleq_cpx_conf_dx, lleq_cpx_trans, cpxs_strap2/ qed-. lemma lleq_cpxs_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡*[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2. + ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. #h #g #G #L2 #T1 #T2 #H @(cpxs_ind … H) -T2 /3 width=6 by lleq_cpx_conf_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index ab90b6f6f..7165feaee 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/relocation/lleq.ma". +include "basic_2/substitution/lleq.ma". include "basic_2/computation/fpbs.ma". (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) @@ -21,7 +21,7 @@ include "basic_2/computation/fpbs.ma". inductive fpbu (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝ | fpbu_fqup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → fpbu h g G1 L1 T1 G2 L2 T2 | fpbu_cpxs: ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) → fpbu h g G1 L1 T1 G1 L1 T2 -| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T1] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 +| fpbu_lpxs: ∀L2. ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → fpbu h g G1 L1 T1 G1 L2 T1 . interpretation @@ -34,7 +34,7 @@ lemma cprs_fpbu: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡* T2 → (T1 = T2 → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpbu_cpxs, cprs_cpxs/ qed. -lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[0, T] L2 → ⊥) → +lemma lprs_fpbu: ∀h,g,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡* L2 → (L1 ⋕[T, 0] L2 → ⊥) → ⦃G, L1, T⦄ ≻[h, g] ⦃G, L2, T⦄. /3 width=1 by fpbu_lpxs, lprs_lpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma index beb022541..6e68fef14 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma @@ -13,13 +13,13 @@ (**************************************************************************) include "basic_2/notation/relations/btpredsnstar_8.ma". -include "basic_2/relocation/lleq.ma". +include "basic_2/substitution/lleq.ma". include "basic_2/computation/lpxs.ma". (* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) inductive fpns (h) (g) (G) (L1) (T): relation3 genv lenv term ≝ -| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[0, T] L2 → fpns h g G L1 T G L2 T +| fpns_intro: ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → L1 ⋕[T, 0] L2 → fpns h g G L1 T G L2 T . interpretation @@ -34,6 +34,6 @@ lemma fpns_refl: ∀h,g. tri_reflexive … (fpns h g). (* Basic inversion lemmas ***************************************************) lemma fpns_inv_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊢ ⋕➡*[h, g] ⦃G2, L2, T2⦄ → - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[0, T1] L2 & T1 = T2. + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡*[h, g] L2 & L1 ⋕[T1, 0] L2 & T1 = T2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by and4_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma index deaa7a967..728f48df9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/substitution/lleq_lleq.ma". include "basic_2/computation/lpxs_lpxs.ma". include "basic_2/computation/fpns.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma index f25939dd3..a460855c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb_csx.ma @@ -19,9 +19,9 @@ axiom lsx_fqup_conf: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, G1 ⊢ ⋕⬊*[h, g, T1] L1 → G2 ⊢ ⋕⬊*[h, g, T2] L2. axiom fqup_lpxs_trans_nlleq: ∀h,g,G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ → - ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[O, T2] L2 →⊥) → + ∀L2. ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 → (K2 ⋕[T2, 0] L2 →⊥) → ∃∃L1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 & - K1 ⋕[O, T1] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. + K1 ⋕[T1, 0] L1 → ⊥ & ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄. (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 792b639dc..4609675a7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/substitution/lleq_alt.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lpxs_cpxs.ma". @@ -20,25 +20,25 @@ include "basic_2/computation/lpxs_cpxs.ma". (* Advanced properties ******************************************************) -axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[d, T] L1d → - ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[d, T] L2d → ⊥) → - ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[d, T] L2d & L1s ⋕[d, T] L2s → ⊥. +axiom lleq_lpxs_trans_nlleq: ∀h,g,G,L1s,L1d,T,d. L1s ⋕[T, d] L1d → + ∀L2d. ⦃G, L1d⦄ ⊢ ➡*[h, g] L2d → (L1d ⋕[T, d] L2d → ⊥) → + ∃∃L2s. ⦃G, L1s⦄ ⊢ ➡*[h, g] L2s & L2s ⋕[T, d] L2d & L1s ⋕[T, d] L2s → ⊥. (* Advanced inversion lemmas ************************************************) -axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[O, T1] L2 → ⊥) → +axiom lpxs_inv_cpxs_nlleq: ∀h,g,G,L1,L2,T1. ⦃G, L1⦄ ⊢ ➡*[h,g] L2 → (L1 ⋕[T1, 0] L2 → ⊥) → ∃∃T2. ⦃G, L1⦄ ⊢ T1 ➡*[h, g] T2 & T1 = T2 → ⊥ & ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2. (* Properties on lazy equivalence for local environments ********************) lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct /2 width=4 by fqu_lref_O, ex3_intro/ | * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H [ elim (lleq_inv_bind … H) @@ -61,8 +61,8 @@ lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, qed-. lemma lpxs_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fquq_inv_gen … H) -H [ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 @@ -72,8 +72,8 @@ elim (fquq_inv_gen … H) -H qed-. lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 [ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 /3 width=4 by fqu_fqup, ex3_intro/ @@ -84,8 +84,8 @@ lemma lpxs_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G qed-. lemma lpxs_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fqus_inv_gen … H) -H [ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 61363bf9f..c842a9448 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazysn_5.ma". -include "basic_2/relocation/lleq.ma". +include "basic_2/substitution/lleq.ma". include "basic_2/computation/lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) @@ -29,7 +29,7 @@ interpretation lemma lsx_ind: ∀h,g,T,G. ∀R:predicate lenv. (∀L1. G ⊢ ⋕⬊*[h, g, T] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → R L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → R L2) → R L1 ) → ∀L. G ⊢ ⋕⬊*[h, g, T] L → R L. @@ -40,7 +40,7 @@ qed-. (* Basic properties *********************************************************) lemma lsx_intro: ∀h,g,T,G,L1. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[0, T] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) → + (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, g] L2 → (L1 ⋕[T, 0] L2 → ⊥) → G ⊢ ⋕⬊*[h, g, T] L2) → G ⊢ ⋕⬊*[h, g, T] L1. /5 width=1 by lleq_sym, SN_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma index e6bf5d3e4..c877a9193 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_cpxs.ma @@ -20,7 +20,7 @@ include "basic_2/computation/lsx.ma". (* Advanced properties ******************************************************) lemma lsx_lleq_trans: ∀h,g,T,G,L1. G ⊢ ⋕⬊*[h, g, T] L1 → - ∀L2. L1 ⋕[0, T] L2 → G ⊢ ⋕⬊*[h, g, T] L2. + ∀L2. L1 ⋕[T, 0] L2 → G ⊢ ⋕⬊*[h, g, T] L2. #h #g #T #G #L1 #H @(lsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 @lsx_intro #L #HL2 #HnT elim (lleq_lpxs_trans_nlleq … HL12 … HL2 HnT) -L2 /3 width=4 by/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc new file mode 100644 index 000000000..321ff3737 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||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/ldrop_leq.ma". +include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_cpx_trans_leq: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1,d. L1 ⋕[d, T1] L2 → L1 ≃[d, ∞] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/ +[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #d #H #HL12 elim (lleq_inv_lref_dx … H … HLK2) -H * + [ #K1 #HLK1 #HV1 #Hdi elim (ldrop_leq_conf_be … HL12 … HLK1) -HL12 /2 width=1 by yle_inj/ + >yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 + #H destruct /3 width=7 by cpx_delta/ + | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/ + yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 + #H destruct /3 width=7 by cpx_delta/ + ] +| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H + /4 width=3 by cpx_bind, leq_succ/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H + /3 width=3 by cpx_flat/ +| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H + /4 width=3 by cpx_zeta, leq_succ/ +| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H + /3 width=3 by cpx_tau/ +| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H + /3 width=3 by cpx_ti/ +| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/ +| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/ +] +qed-. + +(* Note: this can be proved directly *) +lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc new file mode 100644 index 000000000..8a3617c1b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( L1 ≃ break [ term 46 d , break term 46 e ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'Iso $d $e $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc new file mode 100644 index 000000000..179bb5f05 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/leq.ma". +include "basic_2/relocation/ldrop.ma". + +(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) + +lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i → + ⇩[O, i]L2 ≡ K.ⓑ{I}V. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H + * #H1 #H2 + [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12 + #H3 destruct // + | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/ + ] +| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap + #Hei elim (yle_inv_inj2 … Hei) -Hei + #x #Hei #H elim (yplus_inv_inj … H) -H normalize + #y #z >commutative_plus + #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei + #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1 + /4 width=1 by ldrop_ldrop_lt, yle_inj/ +| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei + #x #Hdei #H elim (yplus_inv_inj … H) -H + #y #z >commutative_plus + #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2 + #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei) + #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0 + [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ] + /4 width=3 by yle_inj, monotonic_pred/ +] +qed-. + +lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e → + ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1 + #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] + [ #_ lapply (ldrop_inv_O2 … H) -H + #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/ + | lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ + #Hie lapply (ylt_inv_succ … Hie) -Hie + #Hie elim (IHL12 … H) -IHL12 -H // + >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ + ] +| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) // + #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi + #Hdi #_ #Hide lapply (ylt_inv_succ … Hide) + #Hide lapply (ylt_inv_inj … Hi) -Hi + #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H elim (IHL12 … H) -IHL12 -H + /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ +] +qed-. + +lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 → + ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d → + ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H + #H destruct +| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // +| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // +| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] + [ #_ lapply (ldrop_inv_O2 … H) -H + #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/ + | lapply (ldrop_inv_ldrop1_lt … H ?) -H // + #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ + #Hie lapply (ylt_inv_succ … Hie) -Hie + #Hie elim (IHL12 … H) -IHL12 -H + >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc index a21457b4e..095e1ced3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq.etc @@ -12,54 +12,70 @@ (* *) (**************************************************************************) -include "Basic_2/grammar/lenv_length.ma". +include "ground_2/ynat/ynat_succ.ma". +include "basic_2/notation/relations/iso_4.ma". +include "basic_2/grammar/lenv_length.ma". -(* LOCAL ENVIRONMENT EQUALITY ***********************************************) +(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) -notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" - non associative with precedence 45 - for @{ 'Eq $T1 $d $e $T2 }. - -inductive leq: nat → nat → relation lenv ≝ -| leq_sort: ∀d,e. leq d e (⋆) (⋆) -| leq_OO: ∀L1,L2. leq 0 0 L1 L2 -| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 → - leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V) -| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. - leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) +inductive leq: ynat → ynat → relation lenv ≝ +| leq_atom: ∀d,e. leq d e (⋆) (⋆) +| leq_zero: ∀I,L1,L2,V. leq 0 0 L1 L2 → leq 0 0 (L1.ⓑ{I}V) (L2.ⓑ{I}V) +| leq_pair: ∀I1,I2,L1,L2,V1,V2,e. + leq 0 e L1 L2 → leq 0 (⫯e) (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) +| leq_succ: ∀I,L1,L2,V,d,e. leq d e L1 L2 → leq (⫯d) e (L1.ⓑ{I}V) (L2.ⓑ{I}V) . -interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). - -definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R. - ∀L1,s1,s2. R L1 s1 s2 → - ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2. +interpretation + "equivalence (local environment)" + 'Iso d e L1 L2 = (leq d e L1 L2). (* Basic properties *********************************************************) -lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))). -#S #R #HR #L1 #s1 #s2 #H elim H -H s2 -[ /3 width=5/ -| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 - lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ -] +lemma leq_refl: ∀L,d,e. L ≃[d, e] L. +#L elim L -L /2 width=1 by/ +#L #I #V #IHL #d #e elim (ynat_cases … d) [ | * /2 width=1 by leq_succ/ ] +elim (ynat_cases … e) [ | * ] +/2 width=1 by leq_zero, leq_pair/ qed. -lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. -#d elim d -d -[ #e elim e -e // #e #IHe #L elim L -L /2/ -| #d #IHd #e #L elim L -L /2/ -] -qed. +lemma leq_sym: ∀L1,L2,d,e. L1 ≃[d, e] L2 → L2 ≃[d, e] L1. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e +/2 width=1 by leq_atom, leq_zero, leq_pair, leq_succ/ +qed-. -lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. -#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ +lemma leq_O_Y: ∀L1,L2. |L1| = |L2| → L1 ≃[0, ∞] L2. +#L1 elim L1 -L1 +[ #X #H lapply (length_inv_zero_sn … H) -H // +| #L1 #I1 #V1 #IHL1 #X #H elim (length_inv_pos_sn … H) -H + #L2 #I2 #V2 #HL12 #H destruct + @(leq_pair … (∞)) /2 width=1 by/ (**) (* explicit constructor *) +] qed. -lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → - ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. +(* Basic forward lemmas *****************************************************) -#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ -qed. +lemma leq_fwd_length: ∀L1,L2,d,e. L1 ≃[d, e] L2 → |L1| = |L2|. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e normalize // +qed-. (* Basic inversion lemmas ***************************************************) + +fact leq_inv_O2_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → e = 0 → L1 = L2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/ +#I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H elim (ysucc_inv_O_dx … H) +qed-. + +lemma leq_inv_O2: ∀L1,L2,d. L1 ≃[d, 0] L2 → L1 = L2. +/2 width=4 by leq_inv_O2_aux/ qed-. + +fact leq_inv_Y1_aux: ∀L1,L2,d,e. L1 ≃[d, e] L2 → d = ∞ → L1 = L2. +#L1 #L2 #d #e #H elim H -L1 -L2 -d -e /3 width=1 by eq_f3/ +[ #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #H destruct +| #I #L1 #L2 #V #d #e #_ #IHL12 #H lapply (ysucc_inv_Y_dx … H) -H + /3 width=1 by eq_f3/ +] +qed-. + +lemma leq_inv_Y1: ∀L1,L2,e. L1 ≃[∞, e] L2 → L1 = L2. +/2 width=4 by leq_inv_Y1_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc new file mode 100644 index 000000000..a21457b4e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc @@ -0,0 +1,65 @@ +(**************************************************************************) +(* ___ *) +(* ||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/grammar/lenv_length.ma". + +(* LOCAL ENVIRONMENT EQUALITY ***********************************************) + +notation "hvbox( T1 break [ d , break e ] ≈ break T2 )" + non associative with precedence 45 + for @{ 'Eq $T1 $d $e $T2 }. + +inductive leq: nat → nat → relation lenv ≝ +| leq_sort: ∀d,e. leq d e (⋆) (⋆) +| leq_OO: ∀L1,L2. leq 0 0 L1 L2 +| leq_eq: ∀L1,L2,I,V,e. leq 0 e L1 L2 → + leq 0 (e + 1) (L1. 𝕓{I} V) (L2.𝕓{I} V) +| leq_skip: ∀L1,L2,I1,I2,V1,V2,d,e. + leq d e L1 L2 → leq (d + 1) e (L1. 𝕓{I1} V1) (L2. 𝕓{I2} V2) +. + +interpretation "local environment equality" 'Eq L1 d e L2 = (leq d e L1 L2). + +definition leq_repl_dx: ∀S. (lenv → relation S) → Prop ≝ λS,R. + ∀L1,s1,s2. R L1 s1 s2 → + ∀L2,d,e. L1 [d, e]≈ L2 → R L2 s1 s2. + +(* Basic properties *********************************************************) + +lemma TC_leq_repl_dx: ∀S,R. leq_repl_dx S R → leq_repl_dx S (λL. (TC … (R L))). +#S #R #HR #L1 #s1 #s2 #H elim H -H s2 +[ /3 width=5/ +| #s #s2 #_ #Hs2 #IHs1 #L2 #d #e #HL12 + lapply (HR … Hs2 … HL12) -HR Hs2 HL12 /3/ +] +qed. + +lemma leq_refl: ∀d,e,L. L [d, e] ≈ L. +#d elim d -d +[ #e elim e -e // #e #IHe #L elim L -L /2/ +| #d #IHd #e #L elim L -L /2/ +] +qed. + +lemma leq_sym: ∀L1,L2,d,e. L1 [d, e] ≈ L2 → L2 [d, e] ≈ L1. +#L1 #L2 #d #e #H elim H -H L1 L2 d e /2/ +qed. + +lemma leq_skip_lt: ∀L1,L2,d,e. L1 [d - 1, e] ≈ L2 → 0 < d → + ∀I1,I2,V1,V2. L1. 𝕓{I1} V1 [d, e] ≈ L2. 𝕓{I2} V2. + +#L1 #L2 #d #e #HL12 #Hd >(plus_minus_m_m d 1) /2/ +qed. + +(* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc new file mode 100644 index 000000000..b2b5324a6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc @@ -0,0 +1,125 @@ +(**************************************************************************) +(* ___ *) +(* ||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/reduction/cpx_leq.ma". +include "basic_2/reduction/lpx_ldrop.ma". + +(**) (* to be proved later *) +axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d. + L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 → + L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2. + +(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) + +(* Properties using equivalences for local environments *********************) + +lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d → + ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 → + ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s → + ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d → + L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d. +#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d +[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 + lapply (leq_fwd_length … H3) -H3 #HL2sd + elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ] + #H destruct /2 width=1 by lleq_sort/ +| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 + elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/ + yminus_inj #Y #H1 #HY + lapply (ldrop_mono … HY … HLK1d) -HY #H destruct + elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s + elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct + elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d + elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct + elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/ + >yplus_O1 yminus_inj #Z #Y #X #HK12s #H + lapply (ldrop_mono … H … HLK2s) -H #H destruct + elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/ + >yplus_O1 yminus_inj #Z #Y #X #HK12d #H + lapply (ldrop_mono … H … HLK2d) -H #H destruct + elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/ + yminus_inj #Y #H3 #HY + lapply (ldrop_mono … HY … HLK2d) -HY #H destruct + elim (cpx_inv_lref1 … H2) -H2 -L1s + [ -L1d #H destruct /3 width=15 by lleq_skip/ + | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d + #H destruct >(plus_minus_m_m d (i+1)) // + lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s + lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d + /3 width=9 by lleq_lift_ge/ + ] +| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 + elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY + lapply (ldrop_mono … HY … HLK1d) -HY #H destruct + elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s + elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct + elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d + elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct + lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H + lapply (ldrop_mono … H … HLK2s) -H #H destruct + lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H + lapply (ldrop_mono … H … HLK2d) -H #H destruct + elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/ + >yminus_Y_inj #Z #Y #X #H3 #HY + lapply (ldrop_mono … HY … HLK2d) -HY #H destruct + elim (cpx_inv_lref1 … H2) -H2 -L1s + [ -L1d #H destruct /3 width=12 by lleq_lref/ + | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d + #H destruct + lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s + lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d + @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *) + ] +| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3 + lapply (leq_fwd_length … H2d) -H2d + lapply (leq_fwd_length … H3) -H3 + elim (cpx_inv_lref1 … H2) -H2 + [ #H destruct /2 width=1 by lleq_free/ + | -L1s * #I #K1d #V1 #V2 #HLK1d + lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H + elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) + ] +| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 + lapply (leq_fwd_length … H3) -H3 #HL2sd + lapply (cpx_inv_gref1 … H2) -H2 + #H destruct /2 width=1 by lleq_gref/ +| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 + elim (cpx_inv_bind1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct + /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/ + | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1) + /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/ + ] +| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 + elim (cpx_inv_flat1 … H2) -H2 * + [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/ + | #HT1X #H destruct /2 width=1 by/ + | #HV1X #H destruct /2 width=1 by/ + | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct + lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H + elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2 + /4 width=1 by lleq_beta, lleq_flat, lleq_bind/ + | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct + lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H + elim (lleq_inv_bind … H) -H -HW12 -HT02 + /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/ + ] +] +qed-. + +lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2. +#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1) +/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc deleted file mode 100644 index 9451e34d2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc +++ /dev/null @@ -1,161 +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 "basic_2/unwind/sstas_sstas.ma". -include "basic_2/equivalence/cpcs_ltpr.ma". -include "basic_2/dynamic/snv_ltpss_dx.ma". -include "basic_2/dynamic/snv_sstas.ma". -include "basic_2/dynamic/ygt.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Inductive premises for the preservation results **************************) - -definition IH_snv_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. - -definition IH_ssta_ltpr_tpr: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → - ∀L2. L1 ➡ L2 → ∀T2. T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. - -definition IH_snv_ssta: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L1,T1. ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ⦃h, L1⦄ ⊢ U1 ¡[g]. - -definition IH_snv_lsubsv: ∀h:sh. sd h → relation2 lenv term ≝ - λh,g,L2,T. ⦃h, L2⦄ ⊢ T ¡[g] → - ∀L1. h ⊢ L1 ¡⊑[g] L2 → ⦃h, L1⦄ ⊢ T ¡[g]. - -(* Properties for the preservation results **********************************) - -fact snv_ltpr_cpr_aux: ∀h,g,L1,T1. IH_snv_ltpr_tpr h g L1 T1 → - ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. -#h #g #L1 #T1 #IH #HT1 #L2 #HL12 #T2 * #T #HT1T #HTT2 -lapply (IH … HL12 … HT1T) -HL12 // -T1 #HT0 -lapply (snv_tpss_conf … HT0 … HTT2) -T // -qed-. - -fact ssta_ltpr_cpr_aux: ∀h,g,L1,T1. IH_ssta_ltpr_tpr h g L1 T1 → - ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡ T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. -#h #g #L1 #T1 #IH #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 * #T #HT1T #HTT2 -elim (IH … HTU1 … HL12 … HT1T) // -L1 -T1 #U #HTU #HU1 -elim (ssta_tpss_conf … HTU … HTT2) -T #U2 #HTU2 #HU2 -lapply (cpcs_cpr_strap1 … HU1 U2 ?) /2 width=3/ -qed-. - -fact snv_ltpr_cprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ⦃h, L2⦄ ⊢ T2 ¡[g]. -#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #L2 #HL12 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=6 by snv_ltpr_cpr_aux/ ] -HT1 -/5 width=6 by snv_ltpr_cpr_aux, ygt_yprs_trans, ltpr_cprs_yprs/ -qed-. - -fact ssta_ltpr_cprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1,l. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l, U1⦄ → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l, U2⦄ & L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 #l #HTU1 #L2 #HL12 #T2 #H -@(cprs_ind … H) -T2 [ /2 width=7 by ssta_ltpr_cpr_aux/ ] -#T #T2 #HT1T #HTT2 * #U #HTU #HU1 -elim (ssta_ltpr_cpr_aux … HTU … HTT2) // -[2: /3 width=9 by snv_ltpr_cprs_aux/ -|3: /5 width=6 by ygt_yprs_trans, ltpr_cprs_yprs/ -] -L0 -L1 -T0 -T1 -T #U2 #HTU2 #HU2 -lapply (cpcs_trans … HU1 … HU2) -U /2 width=3/ -qed-. - -fact ssta_ltpr_cpcs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,L2,T1,T2. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → h ⊢ ⦃L0, T0⦄ >[g] ⦃L2, T2⦄ → - ⦃h, L1⦄ ⊢ T1 ¡[g] → ⦃h, L2⦄ ⊢ T2 ¡[g] → - ∀U1,l1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l1, U1⦄ → - ∀U2,l2. ⦃h, L2⦄ ⊢ T2 •[g] ⦃l2, U2⦄ → - L1 ➡ L2 → L2 ⊢ T1 ⬌* T2 → - l1 = l2 ∧ L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #L2 #T1 #T2 #HLT01 #HLT02 #HT1 #HT2 #U1 #l1 #HTU1 #U2 #l2 #HTU2 #HL12 #H -elim (cpcs_inv_cprs … H) -H #T #H1 #H2 -elim (ssta_ltpr_cprs_aux … HLT01 HT1 … HTU1 … H1) -T1 /2 width=1/ #W1 #H1 #HUW1 -elim (ssta_ltpr_cprs_aux … HLT02 HT2 … HTU2 … H2) -T2 /2 width=1/ #W2 #H2 #HUW2 -L1 -L0 -T0 -elim (ssta_mono … H1 … H2) -h -T #H1 #H2 destruct -lapply (cpcs_canc_dx … HUW1 … HUW2) -W2 /2 width=1/ -qed-. - -fact snv_sstas_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → ⦃h, L1⦄ ⊢ U1 ¡[g]. -#h #g #L0 #T0 #IH #L1 #T1 #HLT0 #HT1 #U1 #H -@(sstas_ind … H) -U1 // -HT1 /4 width=5 by ygt_yprs_trans, sstas_yprs/ -qed-. - -fact sstas_ltpr_cprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → ∀U1. ⦃h, L1⦄ ⊢ T1 •*[g] U1 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*[g] U2 & L2 ⊢ U1 ⬌* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #L2 #HL12 #T2 #HT12 #U1 #H -@(sstas_ind … H) -U1 [ /3 width=3/ ] -#U1 #W1 #l1 #HTU1 #HUW1 * #U2 #HTU2 #HU12 -lapply (snv_ltpr_cprs_aux … IH2 … HT1 … HT12) // #HT2 -elim (snv_sstas_fwd_correct … HTU2) // #W2 #l2 #HUW2 -elim (ssta_ltpr_cpcs_aux … IH2 IH1 … HUW1 … HUW2 … HU12) -IH2 -IH1 -HUW1 -HU12 // -[2: /4 width=8 by snv_sstas_aux, ygt_yprs_trans, ltpr_cprs_yprs/ -|3: /3 width=7 by snv_sstas_aux, ygt_yprs_trans, cprs_yprs/ -|4: /4 width=5 by ygt_yprs_trans, ltpr_cprs_yprs, sstas_yprs/ -|5: /3 width=4 by ygt_yprs_trans, cprs_yprs, sstas_yprs/ -] -L0 -T0 -T1 -HT2 #H #HW12 destruct /3 width=4/ -qed-. - -fact dxprs_ltpr_cprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀U1. ⦃h, L1⦄ ⊢ T1 •*➡*[g] U1 → - ∀L2. L1 ➡ L2 → ∀T2. L2 ⊢ T1 ➡* T2 → - ∃∃U2. ⦃h, L2⦄ ⊢ T2 •*➡*[g] U2 & L2 ⊢ U1 ➡* U2. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 #T1 #H01 #HT1 #U1 * #W1 #HTW1 #HWU1 #L2 #HL12 #T2 #HT12 -elim (sstas_ltpr_cprs_aux … IH3 IH2 IH1 … H01 … HT12 … HTW1) // -L0 -T0 -T1 #W2 #HTW2 #HW12 -lapply (ltpr_cprs_conf … HL12 … HWU1) -L1 #HWU1 -lapply (cpcs_canc_sn … HW12 HWU1) -W1 #H -elim (cpcs_inv_cprs … H) -H /3 width=3/ -qed-. - -fact ssta_dxprs_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → ⦃h, L1⦄ ⊢ T1 ¡[g] → - ∀l,U1. ⦃h, L1⦄ ⊢ T1 •[g] ⦃l+1, U1⦄ → ∀T2. ⦃h, L1⦄ ⊢ T1 •*➡*[g] T2 → - ∃∃U,U2. ⦃h, L1⦄ ⊢ U1 •*[g] U & ⦃h, L1⦄ ⊢ T2 •*[g] U2 & L1 ⊢ U ⬌* U2. -#h #g #L0 #T0 #IH2 #IH1 #L1 #T1 #H01 #HT1 #l #U1 #HTU1 #T2 * #T #HT1T #HTT2 -elim (sstas_strip … HT1T … HTU1) #HU1T destruct [ -HT1T | -L0 -T0 -T1 ] -[ elim (ssta_ltpr_cprs_aux … IH2 IH1 … HTU1 L1 … HTT2) // -L0 -T0 -T /3 width=5/ -| @(ex3_2_intro …T2 HU1T) // /2 width=1/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc deleted file mode 100644 index 6a0be5953..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc +++ /dev/null @@ -1,113 +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 "basic_2/computation/dxprs_dxprs.ma". -include "basic_2/dynamic/snv_cpcs.ma". - -(* STRATIFIED NATIVE VALIDITY FOR TERMS *************************************) - -(* Properties on context-free parallel reduction for local environments *****) - -fact snv_ltpr_tpr_aux: ∀h,g,L0,T0. - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_lsubsv h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_snv_ltpr_tpr h g L1 T1. -#h #g #L0 #T0 #IH4 #IH3 #IH2 #IH1 #L1 * * [||||*] -[ #k #HL0 #HT0 #H1 #L2 #_ #X #H2 destruct -IH4 -IH3 -IH2 -IH1 -L1 - >(tpr_inv_atom1 … H2) -X // -| #i #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I #K1 #V1 #HLK1 #HV1 - >(tpr_inv_atom1 … H2) -X - elim (ltpr_ldrop_conf … HLK1 … HL12) -HL12 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) -HLK1 #HLK1 - lapply (IH1 … HK12 … HV12) -IH1 -HV12 -HK12 // -HV1 [ /2 width=1/ ] -HLK1 /2 width=5/ -| #p #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct -IH4 -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #HV1 #HT1 - elim (tpr_inv_bind1 … H2) -H2 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 /2 width=1/ #HT02 - lapply (IH1 … HL12 … HV12) // [ /2 width=1/ ] #HV2 - lapply (snv_ltpr_cpr_aux … HT1 (L2.ⓑ{I}V2) … T2 ?) -HT1 - [ /3 width=5 by cpr_intro, tps_tpss/ | /2 width=1/ | /3 width=1/ ] -IH1 -T0 /2 width=1/ - | #T2 #HT12 #HXT2 #H1 #H2 destruct - lapply (IH1 … HT1 (L2.ⓓV1) … HT12) -IH1 -HT1 -HT12 [1,2: /2 width=1/ ] -HL12 #HT2 - lapply (snv_inv_lift … HT2 L2 … HXT2) -T2 // /2 width=1/ - ] -| #V1 #T1 #HL0 #HT0 #H1 #L2 #HL12 #X #H2 destruct - elim (snv_inv_appl … H1) -H1 #a #W10 #W1 #U1 #l #HV1 #HT1 #HVW1 #HW10 #HTU1 - elim (tpr_inv_appl1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct -IH4 - lapply (IH1 … HV1 … HL12 … HV12) [ /2 width=1/ ] #HV2 - lapply (IH1 … HT1 … HL12 … HT12) [ /2 width=1/ ] #HT2 - elim (IH3 … HVW1 … HL12 … HV12) -HVW1 -HV12 // -HV1 [2: /2 width=1/ ] #W2 #HVW2 #HW12 - elim (dxprs_ltpr_cprs_aux … IH2 IH1 IH3 … HTU1 … HL12 T2) // [2: /3 width=1/ |3: /2 width=1/ ] -IH2 -IH1 -IH3 -HT1 -HT12 -HTU1 #X #HTU2 #H - elim (cprs_inv_abst1 Abst W1 … H) -H #W20 #U2 #HW120 #_ #H destruct - lapply (ltpr_cprs_conf … HL12 … HW10) -L1 #HW10 - lapply (cpcs_cprs_strap1 … HW10 … HW120) -W1 #HW120 - lapply (cpcs_canc_sn … HW12 HW120) -W10 #HW20 - elim (cpcs_inv_cprs … HW20) -HW20 #W0 #HW20 #HW200 - lapply (dxprs_cprs_trans … (ⓛ{a}W0.U2) HTU2 ?) [ /2 width=1/ ] -HW200 -HTU2 /2 width=8/ - | #b #V2 #W20 #T20 #T2 #HV12 #HT202 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW20 #HT20 - elim (dxprs_inv_abst1 … HTU1) -HTU1 #W30 #T30 #HW230 #_ #H destruct -T30 - lapply (cprs_div … HW10 … HW230) -W30 #HW120 - elim (snv_fwd_ssta … HW20) #l0 #U20 #HWU20 - elim (ssta_fwd_correct … HVW1) [g] ⦃L1, T1⦄ → IH_snv_ssta h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_snv_ltpr_tpr h g L1 T1) → - (∀L1,T1. h ⊢ ⦃L0, T0⦄ >[g] ⦃L1, T1⦄ → IH_ssta_ltpr_tpr h g L1 T1) → - ∀L1,T1. L0 = L1 → T0 = T1 → IH_ssta_ltpr_tpr h g L1 T1. -#h #g #L0 #T0 #IH3 #IH2 #IH1 #L1 * * [|||| *] -[ #k #_ #_ #_ #X2 #l #H2 #L2 #HL12 #X3 #H3 -IH3 -IH2 -IH1 - elim (ssta_inv_sort1 … H2) -H2 #Hkl #H destruct - >(tpr_inv_atom1 … H3) -X3 /4 width=6/ -| #i #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 - elim (snv_inv_lref … H1) -H1 #I0 #K0 #V0 #H #HV1 - elim (ssta_inv_lref1 … H2) -H2 * #K1 - >(tpr_inv_atom1 … H3) -X3 - [ #V1 #W1 #HLK1 #HVW1 #HWU1 - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 -HL12 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HV12 // [2: /2 width=1/ ] -V1 #W2 #HVW2 #HW12 - lapply (ldrop_fwd_ldrop2 … HLK2) #H2 - elim (lift_total W2 0 (i+1)) #U2 #HWU2 - lapply (cpcs_lift … H2 … HWU1 … HWU2 HW12) -H2 -W1 /3 width=6/ - | #V1 #W1 #l0 #HLK1 #HVW1 #HVU1 #H destruct - lapply (ldrop_mono … H … HLK1) -H #H destruct - lapply (ldrop_pair2_fwd_fw … HLK1 (#i)) #HKV1 - elim (ltpr_ldrop_conf … HLK1 … HL12) -HLK1 #X #H #HLK2 - elim (ltpr_inv_pair1 … H) -H #K2 #V2 #HK12 #HV12 #H destruct - elim (IH1 … HVW1 … HK12 … HV12) -IH1 -HVW1 -HK12 // [2: /2 width=1/ ] -HV1 -HKV1 #W2 #HVW2 #_ -W1 - elim (lift_total V2 0 (i+1)) #U2 #HVU2 - lapply (tpr_lift … HV12 … HVU1 … HVU2) -V1 /4 width=6/ - ] -| #p #_ #HT0 #H1 destruct -IH3 -IH2 -IH1 - elim (snv_inv_gref … H1) -| #a #I #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct -IH3 -IH2 - elim (snv_inv_bind … H1) -H1 #_ #HT1 - elim (ssta_inv_bind1 … H2) -H2 #U1 #HTU1 #H destruct - elim (tpr_inv_bind1 … H3) -H3 * - [ #V2 #T0 #T2 #HV12 #HT10 #HT02 #H destruct - lapply (tps_lsubr_trans … HT02 (L2.ⓑ{I}V2) ?) -HT02 [ /2 width=1/ ] #HT02 - elim (ssta_ltpr_cpr_aux … HT1 … HTU1 (L2.ⓑ{I}V2) … T2) -HT1 -HTU1 - [2: /3 width=5 by cpr_intro, tps_tpss/ |3: /2 width=1/ |4: /3 width=1/ ] -IH1 -T0 -HL12 #U2 #HTU2 #HU12 - lapply (cpcs_bind2 … V1 … HU12 … a) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ - | #T2 #HT12 #HT2 #H1 #H2 destruct - elim (IH1 … HTU1 (L2.ⓓV1) … T2) -IH1 -HTU1 // [2,3: /2 width=1/ ] -T1 -HL12 #U2 #HTU2 #HU12 - lapply (cpcs_bind1 … HU12 … V1 … true) // -HU12 #HU12 - elim (ssta_inv_lift1 … HTU2 … HT2) -T2 [3: /2 width=1/ |2: skip ] #U #HXU #HU2 - lapply (cpcs_cpr_strap1 … HU12 U ?) -HU12 [ /3 width=3/ ] -U2 /2 width=3/ - ] -| #V1 #T1 #HL0 #HT0 #H1 #X2 #l #H2 #L2 #HL12 #X3 #H3 destruct - elim (snv_inv_appl … H1) -H1 #a #W1 #W10 #U10 #l0 #HV1 #HT1 #HVW1 #HW10 #HTU10 - elim (ssta_inv_appl1 … H2) -H2 #U1 #HTU1 #H destruct - elim (tpr_inv_appl1 … H3) -H3 * - [ #V2 #T2 #HV12 #HT12 #H destruct -a -l0 -W1 -W10 -U10 -HV1 -IH3 -IH2 - elim (IH1 … HTU1 … HL12 … HT12) -IH1 -HTU1 -HL12 // [2: /2 width=1/ ] -T1 #U2 #HTU2 #HU12 - lapply (cpcs_flat … V1 V2 … HU12) -HU12 [ /2 width=1/ ] -HV12 /3 width=3/ - | #b #V2 #W #T2 #T20 #HV12 #HT20 #H1 #H2 destruct - elim (snv_inv_bind … HT1) -HT1 #HW #HT2 - elim (ssta_inv_bind1 … HTU1) -HTU1 #U2 #HTU2 #H destruct - elim (dxprs_inv_abst1 … HTU10) -HTU10 #W0 #U0 #HW0 #_ #H destruct - lapply (cprs_div … HW10 … HW0) -W0 #HW1W - elim (ssta_fwd_correct … HVW1) yminus_Y_inj #J #Y #X #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 - #H destruct /3 width=7 by cpx_delta/ - | #J #K1 #V #HLK1 #_ #HV1 #Hid elim (ldrop_leq_conf_lt … HL12 … HLK1) -HL12 /2 width=1 by ylt_inj/ - yminus_inj #Y #HK12 #H lapply (ldrop_mono … H … HLK2) -L2 - #H destruct /3 width=7 by cpx_delta/ - ] -| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_bind … H) -H - /4 width=3 by cpx_bind, leq_succ/ -| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_flat/ -| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #d #H elim (lleq_inv_bind … H) -H - /4 width=3 by cpx_zeta, leq_succ/ -| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_tau/ -| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #d #H elim (lleq_inv_flat … H) -H - /3 width=3 by cpx_ti/ -| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_beta, leq_succ/ -| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #d #H elim (lleq_inv_flat … H) -H - #HV1 #H elim (lleq_inv_bind … H) -H /4 width=3 by cpx_theta, leq_succ/ -] -qed-. - -(* Note: this can be proved directly *) -lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. -/4 width=6 by lleq_cpx_trans_leq, lleq_fwd_length, leq_O_Y/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma new file mode 100644 index 000000000..c3b0ae106 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -0,0 +1,74 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lleq_alt.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_cpx_trans: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1. L1 ⋕[T1, 0] L2 → ⦃G, L1⦄ ⊢ T1 ➡[h, g] T2. +#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 /2 width=2 by cpx_sort/ +[ #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_fwd_lref_dx … H … HLK2) -L2 + [ #H elim (ylt_yle_false … H) // + | * /3 width=7 by cpx_delta/ + ] +| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=1 by cpx_bind/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_flat/ +| #G #L2 #V2 #T1 #T #T2 #_ #HT2 #IHT1 #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=3 by cpx_zeta/ +| #G #L2 #W1 #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_tau/ +| #G #L2 #W1 #W2 #T1 #_ #IHW12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by cpx_ti/ +| #a #G #L1 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=1 by cpx_beta/ +| #a #G #L1 #V1 #V #V2 #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV1 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind_O … H) -H /3 width=3 by cpx_theta/ +] +qed-. + +(* Note: lemma 1000 *) +lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → + ∀L1. L1 ⋕[T1, 0] L2 → L1 ⋕[T2, 0] L2. +#h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 +[ // +| /3 width=3 by lleq_fwd_length, lleq_sort/ +| #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H + #I1 #K1 #HLK1 #HV1 + lapply (ldrop_fwd_ldrop2 … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_ldrop2 … HLK2) -HLK2 #HLK2 + @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *) +| #a #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H + /4 width=3 by lleq_bind_repl_SO, lleq_bind/ +| #I #G #L2 #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + /3 width=1 by lleq_flat/ +| #G #L2 #V #T1 #T2 #T #_ #HT2 #IHT12 #L1 #H elim (lleq_inv_bind_O … H) -H + /3 width=10 by lleq_inv_lift_le, ldrop_ldrop/ +| #G #L2 #V #T1 #T2 #_ #IHT12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/ +| #G #L2 #V1 #V2 #T #_ #IHV12 #L1 #H elim (lleq_inv_flat … H) -H /2 width=1 by/ +| #a #G #L2 #V1 #V2 #W1 #W2 #T1 #T2 #_ #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind_O … H) -H + /4 width=3 by lleq_bind_repl_SO, lleq_flat, lleq_bind/ +| #a #G #L2 #V1 #V2 #V #W1 #W2 #T1 #T2 #_ #HV2 #_ #_ #IHV12 #IHW12 #IHT12 #L1 #H elim (lleq_inv_flat … H) -H + #HV1 #H elim (lleq_inv_bind_O … H) -H + #HW1 #HT1 @lleq_bind_O /2 width=1 by/ @lleq_flat (**) (* full auto too slow *) + [ /3 width=10 by lleq_lift_le, ldrop_ldrop/ + | /3 width=3 by lleq_bind_repl_O/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma deleted file mode 100644 index 17c2dc14d..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma +++ /dev/null @@ -1,126 +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 "basic_2/reduction/cpx_leq.ma". -include "basic_2/reduction/lpx_ldrop.ma". - -(**) (* to be proved later *) -axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d. - L2s.ⓛW2 ⋕[d+1, T2] L2d.ⓛW2 → - L2s.ⓓⓝW2.V2 ⋕[d+1, T2] L2d.ⓓⓝW2.V2. - -(* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) - -(* Properties using equivalences for local environments *********************) - -(* Note: lemma 1000 *) -lemma lleq_cpx_conf_leq_dx: ∀h,g,G,L1s,L1d,T1,d. L1s ⋕[d, T1] L1d → L1s ≃[d, ∞] L1d → - ∀T2. ⦃G, L1d⦄ ⊢ T1 ➡[h, g] T2 → - ∀L2s. ⦃G, L1s⦄ ⊢ ➡[h, g] L2s → L1s ≃[0, d] L2s → - ∀L2d. ⦃G, L1d⦄ ⊢ ➡[h, g] L2d → L1d ≃[0, d] L2d → - L2s ≃[d, ∞] L2d → L2s ⋕[d, T2] L2d. -#h #g #G #L1s #L1d #T1 #d #H elim H -L1s -L1d -T1 -d -[ #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 - lapply (leq_fwd_length … H3) -H3 #HL2sd - elim (cpx_inv_sort1 … H2) -H2 [| * #l #_ ] - #H destruct /2 width=1 by lleq_sort/ -| #Is #Id #L1s #L1d #K1s #K1d #V1s #V1d #d #i #Hid #HLK1s #HLK1d #_ #_ #_ #IHV1d #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (ldrop_leq_conf_lt … H1 … HLK1s) -H1 /2 width=1 by ylt_inj/ - yminus_inj #Y #H1 #HY - lapply (ldrop_mono … HY … HLK1d) -HY #H destruct - elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s - elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct - elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d - elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct - elim (ldrop_leq_conf_be … H2s … HLK1s) -H2s /2 width=1 by ylt_inj/ - >yplus_O1 yminus_inj #Z #Y #X #HK12s #H - lapply (ldrop_mono … H … HLK2s) -H #H destruct - elim (ldrop_leq_conf_be … H2d … HLK1d) -H2d /2 width=1 by ylt_inj/ - >yplus_O1 yminus_inj #Z #Y #X #HK12d #H - lapply (ldrop_mono … H … HLK2d) -H #H destruct - elim (ldrop_leq_conf_lt … H3 … HLK2s) -H3 /2 width=1 by ylt_inj/ - yminus_inj #Y #H3 #HY - lapply (ldrop_mono … HY … HLK2d) -HY #H destruct - elim (cpx_inv_lref1 … H2) -H2 -L1s - [ -L1d #H destruct /3 width=15 by lleq_skip/ - | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d - #H destruct >(plus_minus_m_m d (i+1)) // - lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s - lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d - /3 width=9 by lleq_lift_ge/ - ] -| #I #L1s #L1d #K1s #K1d #V1 #d #i #Hdi #HLK1s #HLK1d #_ #IHV1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (ldrop_leq_conf_be … H1 … HLK1s) -H1 /2 width=1 by ylt_Y, yle_inj/ #Z #Y #X #H1 #HY - lapply (ldrop_mono … HY … HLK1d) -HY #H destruct - elim (lpx_ldrop_conf … HLK1s … H1s) -H1s #Y #H #HLK2s - elim (lpx_inv_pair1 … H) -H #K2s #V2s #H1s #HV12s #H destruct - elim (lpx_ldrop_conf … HLK1d … H1d) -H1d #Y #H #HLK2d - elim (lpx_inv_pair1 … H) -H #K2d #V2d #H1d #HV12d #H destruct - lapply (ldrop_leq_conf_ge … H2s … HLK1s ?) /2 width=1 by yle_inj/ #H - lapply (ldrop_mono … H … HLK2s) -H #H destruct - lapply (ldrop_leq_conf_ge … H2d … HLK1d ?) /2 width=1 by yle_inj/ #H - lapply (ldrop_mono … H … HLK2d) -H #H destruct - elim (ldrop_leq_conf_be … H3 … HLK2s) -H3 /2 width=1 by ylt_Y, yle_inj/ - >yminus_Y_inj #Z #Y #X #H3 #HY - lapply (ldrop_mono … HY … HLK2d) -HY #H destruct - elim (cpx_inv_lref1 … H2) -H2 -L1s - [ -L1d #H destruct /3 width=12 by lleq_lref/ - | * #Z #Y #X1 #X2 #H #HX12 #HX2 lapply (ldrop_mono … H … HLK1d) -L1d - #H destruct - lapply (ldrop_fwd_ldrop2 … HLK2s) -HLK2s #HLK2s - lapply (ldrop_fwd_ldrop2 … HLK2d) -HLK2d #HLK2d - @(lleq_ge … 0) /3 width=10 by lleq_lift_le/ (**) (* full auto too slow *) - ] -| #L1s #L1d #d #i #HL1s #HL1d #_ #_ #X #H2 #L2s #_ #_ #L2s #_ #H2d #H3 - lapply (leq_fwd_length … H2d) -H2d - lapply (leq_fwd_length … H3) -H3 - elim (cpx_inv_lref1 … H2) -H2 - [ #H destruct /2 width=1 by lleq_free/ - | -L1s * #I #K1d #V1 #V2 #HLK1d - lapply (ldrop_fwd_length_lt2 … HLK1d) -HLK1d #H - elim (lt_refl_false … i) /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) - ] -| #L1s #L1d #d #k #_ #_ #X #H2 #L2s #_ #_ #L2d #_ #_ #H3 - lapply (leq_fwd_length … H3) -H3 #HL2sd - lapply (cpx_inv_gref1 … H2) -H2 - #H destruct /2 width=1 by lleq_gref/ -| #a #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (cpx_inv_bind1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct - /5 width=5 by lpx_pair, lleq_cpx_trans_leq, lleq_bind, leq_pair, leq_succ/ - | #T2 #HT12 #HT2X #H1 #H2 destruct >(minus_plus_m_m d 1) - /4 width=9 by lpx_pair, lleq_inv_lift_ge, ldrop_ldrop, leq_pair, leq_succ/ - ] -| #I #L1s #L1d #V1 #T1 #d #HV1 #_ #IHV1 #IHT1 #H1 #X #H2 #L2s #H1s #H2s #L2d #H1d #H2d #H3 - elim (cpx_inv_flat1 … H2) -H2 * - [ #V2 #T2 #HV12 #HT12 #H destruct /3 width=1 by lleq_flat/ - | #HT1X #H destruct /2 width=1 by/ - | #HV1X #H destruct /2 width=1 by/ - | #a #V2 #W1 #W2 #T0 #T2 #HV12 #HW12 #HT02 #H1 #H2 #H3 destruct - lapply (IHT1 … (ⓛ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H - elim (lleq_inv_bind … H) -H -HW12 -HT02 #HW2 #HT2 - /4 width=1 by lleq_beta, lleq_flat, lleq_bind/ - | #a #V0 #V2 #W1 #W2 #T0 #T2 #HV10 #HV02 #HW12 #HT02 #H1 #H2 #H3 destruct - lapply (IHT1 … (ⓓ{a}W2.T2) … L2s … L2d ? ? ?) -IHT1 /2 width=1 by cpx_bind/ #H - elim (lleq_inv_bind … H) -H -HW12 -HT02 - /5 width=9 by lleq_lift_ge, lleq_flat, lleq_bind, ldrop_ldrop/ - ] -] -qed-. - -lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → - ∀L1. L1 ⋕[0, T1] L2 → L1 ⋕[0, T2] L2. -#h #g #G #L2 #T1 #T2 #HT12 #L1 #HT1 lapply (lleq_fwd_length … HT1) -/3 width=13 by lleq_cpx_conf_leq_dx, leq_O_Y/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index fd95e52cd..7c7bbed03 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_lleq.ma". +include "basic_2/substitution/lleq_alt.ma". include "basic_2/reduction/lpx_ldrop.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) @@ -20,13 +20,13 @@ include "basic_2/reduction/lpx_ldrop.ma". (* Properties on lazy equivalence for local environments ********************) lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct /2 width=4 by fqu_lref_O, ex3_intro/ | * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H [ elim (lleq_inv_bind … H) @@ -49,8 +49,8 @@ lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, qed-. lemma lpx_lleq_fquq_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fquq_inv_gen … H) -H [ #H elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 @@ -60,8 +60,8 @@ elim (fquq_inv_gen … H) -H qed-. lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 [ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpx_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 /3 width=4 by fqu_fqup, ex3_intro/ @@ -72,8 +72,8 @@ lemma lpx_lleq_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2 qed-. lemma lpx_lleq_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[0, T1] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[0, T2] L2. + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → K1 ⋕[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊃* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2 & K2 ⋕[T2, 0] L2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 elim (fqus_inv_gen … H) -H [ #H elim (lpx_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma deleted file mode 100644 index 530f4dfa5..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma +++ /dev/null @@ -1,45 +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 "basic_2/relocation/lleq_lleq.ma". -include "basic_2/relocation/fqu.ma". - -(* SUPCLOSURE ***************************************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[0, T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. -#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U -[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // - #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 - #H destruct /2 width=3 by fqu_lref_O, ex2_intro/ -| * [ #a ] #I #G #L2 #V #T #L1 #H - [ elim (lleq_inv_bind … H) - | elim (lleq_inv_flat … H) - ] -H - /2 width=3 by fqu_pair_sn, ex2_intro/ -| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H - #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/ -| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H - /2 width=3 by fqu_flat_dx, ex2_intro/ -| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12 - elim (ldrop_O1_le (e+1) L1) - [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ - | lapply (ldrop_fwd_length_le2 … HLK2) -K2 - lapply (lleq_fwd_length … HL12) -T -U // - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma deleted file mode 100644 index b4d814649..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma +++ /dev/null @@ -1,29 +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 "basic_2/relocation/fqu_lleq.ma". -include "basic_2/relocation/fquq_alt.ma". - -(* OPTIONAL SUPCLOSURE ******************************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[0, T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H -[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma deleted file mode 100644 index 179bb5f05..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ /dev/null @@ -1,96 +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/ynat/ynat_plus.ma". -include "basic_2/grammar/leq.ma". -include "basic_2/relocation/ldrop.ma". - -(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) - -lemma ldrop_leq_conf_ge: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I,K,V,i. ⇩[O, i]L1 ≡ K.ⓑ{I}V → d + e ≤ i → - ⇩[O, i]L2 ≡ K.ⓑ{I}V. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J #K #W #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #HL12 #IHL12 #J #K #W #i #H #_ elim (ldrop_inv_O1_pair1 … H) -H - * #H1 #H2 - [ -IHL12 lapply (leq_inv_O2 … HL12) -HL12 - #H3 destruct // - | -HL12 /4 width=1 by ldrop_ldrop_lt, yle_inj/ - ] -| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #IHL12 #J #K #W #i #H1 >yplus_succ_swap - #Hei elim (yle_inv_inj2 … Hei) -Hei - #x #Hei #H elim (yplus_inv_inj … H) -H normalize - #y #z >commutative_plus - #H1 #H2 #H3 destruct elim (le_inv_plus_l … Hei) -Hei - #Hzi #Hi lapply (ldrop_inv_ldrop1_lt … H1 ?) -H1 - /4 width=1 by ldrop_ldrop_lt, yle_inj/ -| #I #L1 #L2 #V #d #e #_ #IHL12 #J #K #W #i #H0 #Hdei elim (yle_inv_inj2 … Hdei) -Hdei - #x #Hdei #H elim (yplus_inv_inj … H) -H - #y #z >commutative_plus - #H1 #H2 #H3 destruct elim (ysucc_inv_inj_dx … H2) -H2 - #x #H1 #H2 destruct elim (le_inv_plus_l … Hdei) - #_ #Hi lapply (ldrop_inv_ldrop1_lt … H0 ?) -H0 - [2: #H0 @ldrop_ldrop_lt ] [2,3: /2 width=3 by lt_to_le_to_lt/ ] - /4 width=3 by yle_inj, monotonic_pred/ -] -qed-. - -lemma ldrop_leq_conf_be: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I1,K1,V1,i. ⇩[O, i]L1 ≡ K1.ⓑ{I1}V1 → d ≤ i → i < d + e → - ∃∃I2,K2,V2. K1 ≃[0, ⫰(d+e-i)] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I2}V2. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J1 #K1 #W1 #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #HL12 #IHL12 #J1 #K1 #W1 #i #_ #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #e #HL12 >yplus_O1 >yplus_O1 - #IHL12 #J1 #K1 #W1 #i #H #_ elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] - [ #_ lapply (ldrop_inv_O2 … H) -H - #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_3_intro/ - | lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ - #Hie lapply (ylt_inv_succ … Hie) -Hie - #Hie elim (IHL12 … H) -IHL12 -H // - >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ - ] -| #I #L1 #L2 #V #d #e #_ #IHL12 #J1 #K1 #W1 #i #H #Hdi lapply (ylt_yle_trans 0 … Hdi ?) // - #Hi <(ylt_inv_O1 … Hi) >yplus_succ1 >yminus_succ elim (yle_inv_succ1 … Hdi) -Hdi - #Hdi #_ #Hide lapply (ylt_inv_succ … Hide) - #Hide lapply (ylt_inv_inj … Hi) -Hi - #Hi lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H elim (IHL12 … H) -IHL12 -H - /3 width=5 by ldrop_ldrop_lt, ex2_3_intro/ -] -qed-. - -lemma ldrop_leq_conf_lt: ∀L1,L2,d,e. L1 ≃[d, e] L2 → - ∀I,K1,V,i. ⇩[O, i]L1 ≡ K1.ⓑ{I}V → i < d → - ∃∃K2. K1 ≃[⫰(d-i), e] K2 & ⇩[O, i]L2 ≡ K2.ⓑ{I}V. -#L1 #L2 #d #e #H elim H -L1 -L2 -d -e -[ #d #e #J #K1 #W #i #H elim (ldrop_inv_atom1 … H) -H - #H destruct -| #I #L1 #L2 #V #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #e #_ #_ #J #K1 #W #i #_ #H elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #d #e #HL12 #IHL12 #J #K1 #W #i #H elim (eq_or_gt i) #Hi destruct [ -IHL12 | -HL12 ] - [ #_ lapply (ldrop_inv_O2 … H) -H - #H destruct >ypred_succ /2 width=5 by ldrop_pair, ex2_intro/ - | lapply (ldrop_inv_ldrop1_lt … H ?) -H // - #H <(ylt_inv_O1 i) /2 width=1 by ylt_inj/ - #Hie lapply (ylt_inv_succ … Hie) -Hie - #Hie elim (IHL12 … H) -IHL12 -H - >yminus_succ /3 width=5 by ldrop_ldrop_lt, ex2_intro/ - ] -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma deleted file mode 100644 index b5bef1116..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma +++ /dev/null @@ -1,163 +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 "basic_2/notation/relations/lazyeq_4.ma". -include "basic_2/relocation/ldrop.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -inductive lleq: nat → term → relation lenv ≝ -| lleq_sort: ∀L1,L2,d,k. |L1| = |L2| → lleq d (⋆k) L1 L2 -| lleq_skip: ∀I1,I2,L1,L2,K1,K2,V1,V2,d,i. i < d → - ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 → - lleq (d-i-1) V1 K1 K2 → lleq (d-i-1) V2 K1 K2 → lleq d (#i) L1 L2 -| lleq_lref: ∀I,L1,L2,K1,K2,V,d,i. d ≤ i → - ⇩[0, i] L1 ≡ K1.ⓑ{I}V → ⇩[0, i] L2 ≡ K2.ⓑ{I}V → - lleq 0 V K1 K2 → lleq d (#i) L1 L2 -| lleq_free: ∀L1,L2,d,i. |L1| ≤ i → |L2| ≤ i → |L1| = |L2| → lleq d (#i) L1 L2 -| lleq_gref: ∀L1,L2,d,p. |L1| = |L2| → lleq d (§p) L1 L2 -| lleq_bind: ∀a,I,L1,L2,V,T,d. - lleq d V L1 L2 → lleq (d+1) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → - lleq d (ⓑ{a,I}V.T) L1 L2 -| lleq_flat: ∀I,L1,L2,V,T,d. - lleq d V L1 L2 → lleq d T L1 L2 → lleq d (ⓕ{I}V.T) L1 L2 -. - -interpretation - "lazy equivalence (local environment)" - 'LazyEq d T L1 L2 = (lleq d T L1 L2). - -(* Basic_properties *********************************************************) - -lemma lleq_sym: ∀d,T. symmetric … (lleq d T). -#d #T #L1 #L2 #H elim H -d -T -L1 -L2 -/2 width=10 by lleq_sort, lleq_skip, lleq_lref, lleq_free, lleq_gref, lleq_bind, lleq_flat/ -qed-. - -(* Note this is: "∀d,T. reflexive … (lleq d T)" *) -axiom lleq_refl: ∀T,L,d. L ⋕[d, T] L. -(* -#T #L @(f2_ind … rfw … L T) -L -T -#n #IH #L * * /3 width=1 by lleq_sort, lleq_gref, lleq_bind, lleq_flat/ -#i #H elim (lt_or_ge i (|L|)) /2 width=1 by lleq_free/ -#HiL #d elim (lt_or_ge i d) /2 width=1 by lleq_skip/ -elim (ldrop_O1_lt … HiL) -HiL destruct /4 width=7 by lleq_lref, ldrop_fwd_rfw/ -qed. -*) - -lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[d1, T] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[d2, T] L2. -#L1 #L2 #T #d1 #H elim H -L1 -L2 -T -d1 -/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, le_S_S/ -[ /5 width=10 by lleq_skip, lt_to_le_to_lt, monotonic_le_minus_l, monotonic_pred/ (**) (* a bit slow *) -| #I #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (lt_or_ge i d2) - [ -d1 /3 width=10 by lleq_skip/ - | /3 width=7 by lleq_lref, transitive_le/ - ] -] -qed-. - -lemma lleq_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[0, V] L2 → L1.ⓑ{I}V ⋕[0, T] L2.ⓑ{I}V → - L1 ⋕[0, ⓑ{a,I}V.T] L2. -/3 width=3 by lleq_ge, lleq_bind/ qed. - -(* Basic inversion lemmas ***************************************************) - -fact lleq_inv_lref_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀i. X = #i → - ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & - ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & - K1 ⋕[d-i-1, V1] K2 & - K1 ⋕[d-i-1, V2] K2 & - i < d - | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & - ⇩[0, i] L2 ≡ K2.ⓑ{I}V & - K1 ⋕[0, V] K2 & d ≤ i. -#d #X #L1 #L2 * -d -X -L1 -L2 -[ #L1 #L2 #d #k #_ #j #H destruct -| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #Hid #HLK1 #HLK2 #HV1 #HV2 #j #H destruct /3 width=10 by or3_intro1, ex5_6_intro/ -| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #j #H destruct /3 width=7 by or3_intro2, ex4_4_intro/ -| #L1 #L2 #d #i #HL1 #HL2 #_ #j #H destruct /3 width=1 by or3_intro0, conj/ -| #L1 #L2 #d #p #_ #j #H destruct -| #a #I #L1 #L2 #V #T #d #_ #_ #j #H destruct -| #I #L1 #L2 #V #T #d #_ #_ #j #H destruct -] -qed-. - -lemma lleq_inv_lref: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → - ∨∨ |L1| ≤ i ∧ |L2| ≤ i - | ∃∃I1,I2,K1,K2,V1,V2. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & - ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & - K1 ⋕[d-i-1, V1] K2 & - K1 ⋕[d-i-1, V2] K2 & - i < d - | ∃∃I,K1,K2,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & - ⇩[0, i] L2 ≡ K2.ⓑ{I}V & - K1 ⋕[0, V] K2 & d ≤ i. -/2 width=3 by lleq_inv_lref_aux/ qed-. - -fact lleq_inv_bind_aux: ∀d,X,L1,L2. L1 ⋕[d,X] L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T → - L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V. -#d #X #L1 #L2 * -d -X -L1 -L2 -[ #L1 #L2 #d #k #_ #b #J #W #U #H destruct -| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #d #i #_ #_ #_ #b #J #W #U #H destruct -| #L1 #L2 #d #p #_ #b #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #d #HV #HT #b #J #W #U #H destruct /2 width=1 by conj/ -| #I #L1 #L2 #V #T #d #_ #_ #b #J #W #U #H destruct -] -qed-. - -lemma lleq_inv_bind: ∀a,I,L1,L2,V,T,d. L1 ⋕[d, ⓑ{a,I}V.T] L2 → - L1 ⋕[d, V] L2 ∧ L1.ⓑ{I}V ⋕[d+1, T] L2.ⓑ{I}V. -/2 width=4 by lleq_inv_bind_aux/ qed-. - -fact lleq_inv_flat_aux: ∀d,X,L1,L2. L1 ⋕[d, X] L2 → ∀I,V,T. X = ⓕ{I}V.T → - L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2. -#d #X #L1 #L2 * -d -X -L1 -L2 -[ #L1 #L2 #d #k #_ #J #W #U #H destruct -| #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #_ #_ #_ #_ #J #W #U #H destruct -| #I #L1 #L2 #K1 #K2 #V #d #i #_ #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #d #i #_ #_ #_ #J #W #U #H destruct -| #L1 #L2 #d #p #_ #J #W #U #H destruct -| #a #I #L1 #L2 #V #T #d #_ #_ #J #W #U #H destruct -| #I #L1 #L2 #V #T #d #HV #HT #J #W #U #H destruct /2 width=1 by conj/ -] -qed-. - -lemma lleq_inv_flat: ∀I,L1,L2,V,T,d. L1 ⋕[d, ⓕ{I}V.T] L2 → - L1 ⋕[d, V] L2 ∧ L1 ⋕[d, T] L2. -/2 width=4 by lleq_inv_flat_aux/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → |L1| = |L2|. -#L1 #L2 #T #d #H elim H -L1 -L2 -T -d // -[ #I1 #I2 #L1 #L2 #K1 #K2 #V1 #V2 #d #i #_ #HLK1 #HLK2 #_ #_ #HK12 #_ -| #I #L1 #L2 #K1 #K2 #V #d #i #_ #HLK1 #HLK2 #_ #IHK12 -] -lapply (ldrop_fwd_length … HLK1) -HLK1 -lapply (ldrop_fwd_length … HLK2) -HLK2 -normalize // -qed-. - -lemma lleq_fwd_ldrop_sn: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K1,i. ⇩[0, i] L1 ≡ K1 → - ∃K2. ⇩[0, i] L2 ≡ K2. -#L1 #L2 #T #d #H #K1 #i #HLK1 lapply (lleq_fwd_length … H) -H -#HL12 lapply (ldrop_fwd_length_le2 … HLK1) -HLK1 /2 width=1 by ldrop_O1_le/ -qed-. - -lemma lleq_fwd_ldrop_dx: ∀L1,L2,T,d. L1 ⋕[d, T] L2 → ∀K2,i. ⇩[0, i] L2 ≡ K2 → - ∃K1. ⇩[0, i] L1 ≡ K1. -/3 width=6 by lleq_fwd_ldrop_sn, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma deleted file mode 100644 index e12e5ca9c..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma +++ /dev/null @@ -1,441 +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 "basic_2/relocation/ldrop_ldrop.ma". -include "basic_2/relocation/lleq.ma". - -(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) - -(* Advanced inversion lemmas ************************************************) - -lemma lleq_inv_lref_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → - ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V → - (∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨ - ∃∃I1,K1,V1. ⇩[0, i] L1 ≡ K1.ⓑ{I1}V1 & - K1 ⋕[d-i-1, V1] K2 & K1 ⋕[d-i-1, V] K2 & - i < d. -#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H * -[ #_ #H elim (lt_refl_false i) - lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 - /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) -| #I1 #I2 #K11 #K22 #V1 #V2 #HLK11 #HLK22 #HV1 #HV2 #Hdi lapply (ldrop_mono … HLK22 … HLK2) -L2 - #H destruct /3 width=6 by ex4_3_intro, or_intror/ -| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #Hdi lapply (ldrop_mono … HLK0 … HLK2) -L2 - #H destruct /3 width=3 by ex3_intro, or_introl/ -] -qed-. - -lemma lleq_inv_lref_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → - ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V → - (∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2 & d ≤ i) ∨ - ∃∃I2,K2,V2. ⇩[0, i] L2 ≡ K2.ⓑ{I2}V2 & - K1 ⋕[d-i-1, V] K2 & K1 ⋕[d-i-1, V2] K2 & - i < d. -#L1 #L2 #d #i #HL12 #I #K1 #V #HLK1 elim (lleq_inv_lref_dx L2 … d … HLK1) -HLK1 -[1,2: * ] /4 width=6 by lleq_sym, ex4_3_intro, ex3_intro, or_introl, or_intror/ -qed-. - -lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i → - ∀I,K2,V. ⇩[0, i] L2 ≡ K2.ⓑ{I}V → - ∃∃K1. ⇩[0, i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[0, V] K2. -#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (lleq_inv_lref … H) -H * -[ #_ #H elim (lt_refl_false i) - lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 - /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) -| -HLK2 #I1 #I2 #K11 #K22 #V1 #V2 #_ #_ #_ #_ #H elim (lt_refl_false i) - /2 width=3 by lt_to_le_to_lt/ -| #I0 #K1 #K0 #V0 #HLK1 #HLK0 #HK10 #_ lapply (ldrop_mono … HLK0 … HLK2) -L2 - #H destruct /2 width=3 by ex2_intro/ -] -qed-. - -lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[d, #i] L2 → d ≤ i → - ∀I,K1,V. ⇩[0, i] L1 ≡ K1.ⓑ{I}V → - ∃∃K2. ⇩[0, i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[0, V] K2. -#L1 #L2 #d #i #HL12 #Hdi #I #K1 #V #HLK1 elim (lleq_inv_lref_ge_dx L2 … Hdi … HLK1) -Hdi -HLK1 -/3 width=3 by lleq_sym, ex2_intro/ -qed-. - -fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[d0, T] L2 → ∀d. d0 = d + 1 → - ∀K1,K2,I,V. ⇩[0, d] L1 ≡ K1.ⓑ{I}V → ⇩[0, d] L2 ≡ K2.ⓑ{I}V → - L1 ⋕[d, T] L2. -#L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0 -/2 width=1 by lleq_sort, lleq_free, lleq_gref/ -[ #I1 #I2 #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HLK11 #HLK22 #HV1 #_ #IHV1 #IHV2 #d #H #K1 #K2 #J #W #HLK1 #HLK2 destruct - elim (le_to_or_lt_eq i d) /2 width=1 by lleq_skip, monotonic_pred/ -Hid0 - [ -HV1 #Hid - lapply (ldrop_fwd_ldrop2 … HLK11) #H1 - lapply (ldrop_fwd_ldrop2 … HLK22) #H2 - lapply (ldrop_conf_ge … H1 … HLK1 ?) // -H1 -HLK1 - lapply (ldrop_conf_ge … H2 … HLK2 ?) // -H2 -HLK2 - (lift_inv_sort2 … H) -X - lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e - /2 width=1 by lleq_sort/ -| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H - * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ] - [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 - elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 - #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 - @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *) - | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -Hid -L2 - #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 - /2 width=3 by lleq_ge, le_to_lt_to_lt/ (**) (* full auto fails *) - ] -| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #IHW #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H - * #Hid #H destruct [ -HW | -IHW ] - [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V #HKL1 #KL11 #HVW - elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V0 #HKL2 #KL22 #HV0 - lapply (lift_inj … HV0 … HVW) -HV0 #H destruct /3 width=12 by lleq_lref/ - | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 - elim (le_inv_plus_l … Hid) -Hid /3 width=7 by lleq_lref, transitive_le/ - ] -| #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 @lleq_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 lleq_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 lleq_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 lleq_bind, ldrop_skip, le_S_S/ -| #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 lleq_flat/ -] -qed-. - -lemma lleq_inv_lift_ge: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d+e ≤ d0 → K1 ⋕[d0-e, T] K2. -#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 lleq_sort/ -| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HW1 #HW2 #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H - * #Hid #H destruct [ -HW1 -HW2 | -IHW1 -IHW2 ] - [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 - elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 - elim (le_inv_plus_l … Hded0) #Hdd0e #_ - #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 - @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 [ /2 width=3 by lt_to_le_to_lt/ ] (**) (* explicit constructor *) - >minus_minus_comm3 /3 width=6 by arith_k_sn/ (**) (* slow *) - | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 - elim (le_inv_plus_l … Hid) -Hid #_ #Hei - #HK22 #HK11 @(lleq_skip … HK11 HK22) -HK11 -HK22 (**) (* explicit constructor *) - [ /2 width=1 by monotonic_lt_minus_l/ ] >arith_b1 // - ] -| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H - * #Hid #H destruct - [ -I -L1 -L2 -K11 -K22 -W elim (le_plus_xySz_x_false e 0 d) - /3 width=3 by transitive_le, le_to_lt_to_lt/ - | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 - /3 width=7 by lleq_lref, monotonic_le_minus_l/ - ] -| #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 @lleq_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 lleq_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 lleq_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 - elim (le_inv_plus_l … Hded0) #_ #Hed0 - @lleq_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) - >plus_minus /3 width=5 by ldrop_skip, le_minus_to_plus/ -| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_flat2 … H) -H - #V #T #HVW #HTU #H destruct /3 width=5 by lleq_flat/ -] -qed-. - -lemma lleq_inv_lift_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → K1 ⋕[d, T] K2. -#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 lleq_sort/ -| #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H - * #Hid #H destruct - [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 - elim (ldrop_conf_lt … HLK2 … HLK22) // -L2 -Hid0 - #L2 #V2 #HKL2 #HKL22 #HVW2 #L1 #V1 #HKL1 #HKL11 #HVW1 - @(lleq_skip … HKL1 HKL2) -HKL1 -HKL2 // - /3 width=6 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *) - | -I1 -I2 -L1 -L2 -K11 -K22 -W1 -W2 -Hd0 elim (lt_refl_false i) - /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) - ] -| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_lref2 … H) -H - * #Hid #H destruct - [ -I -L1 -L2 -K11 -K22 -W -Hde elim (lt_refl_false i) - /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) - | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hde - elim (le_inv_plus_l … Hid) -Hid /2 width=7 by lleq_lref/ - ] -| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde 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 @lleq_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 lleq_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 lleq_gref/ -| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct - @lleq_bind [ /2 width=5 by/ ] -IHW - @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, le_S_S/ (**) (* full auto too slow *) -| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H - #V #T #HVW #HTU #H destruct /3 width=6 by lleq_flat/ -] -qed-. - -(* Advanced properties ******************************************************) - -lemma lleq_lift_le: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 → - ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → L1 ⋕[d0, U] L2. -#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 lleq_sort/ -| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #_ #_ #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H - * #Hdi #H destruct - [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 - elim (ldrop_trans_lt … HLK2 … HK22) // -K2 - #K2 #W2 #HLK2 #HK22 #HVW2 #K1 #W1 #HLK1 #HK11 #HVW1 -Hdi - @(lleq_skip … HLK1 HLK2) // /3 width=6 by monotonic_le_minus_l2/ (**) (* full auto fails *) - | elim (lt_refl_false i) -I1 -I2 -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e - /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) - ] -| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #IHV #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H - * #Hdi #H destruct [ -HV | -IHV ] - [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W #HLK1 #HK11 #HVW - elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 #K2 #W2 #HLK2 #HK22 #HVW2 - lapply (lift_mono … HVW2 … HVW) -HVW2 #H destruct /3 width=12 by lleq_lref/ - | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1 - lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hdi -K2 - /3 width=7 by lleq_lref, transitive_le/ - ] -| #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=6 by lleq_free, ldrop_fwd_be/ - | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 - lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 - @lleq_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 lleq_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 lleq_bind, ldrop_skip, le_S_S/ -| #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 lleq_flat/ -] -qed-. - -lemma lleq_lift_ge: ∀K1,K2,T,d0. K1 ⋕[d0, T] K2 → - ∀L1,L2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → L1 ⋕[d0+e, U] L2. -#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 lleq_sort/ -| #I1 #I2 #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #hid0 #HK11 #HK22 #HV1 #HV2 #IHV1 #IHV2 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H - * #Hdi #H destruct [ -HV1 -HV2 | -IHV1 -IHV2 ] - [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 #K1 #W1 #HLK1 #HK11 #HVW1 - elim (ldrop_trans_lt … HLK2 … HK22) // -K2 #K2 #W2 #HLK2 #HK22 #HVW2 - @(lleq_skip … HLK1 HLK2) -HLK1 -HLK2 (**) (* explicit constructor *) - [ /2 width=3 by lt_to_le_to_lt/ ] - >arith_i /3 width=5 by monotonic_le_minus_l2/ - | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 - lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -K2 - /4 width=10 by lleq_skip, monotonic_lt_plus_l/ - ] -| #I #K1 #K2 #K11 #K22 #V #d0 #i #Hid0 #HK11 #HK22 #HV #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H - * #Hid #H destruct - [ elim (lt_refl_false i) -I -L1 -L2 -K1 -K2 -K11 -K22 -V -e - /3 width=3 by lt_to_le_to_lt, transitive_le/ (**) (* slow *) - | lapply (ldrop_trans_ge … HLK1 … HK11 ?) // -K1 - lapply (ldrop_trans_ge … HLK2 … HK22 ?) // -Hid -K2 - /3 width=7 by lleq_lref, monotonic_le_plus_l/ - ] -| #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=6 by lleq_free, ldrop_fwd_be/ - | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 - lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 - @lleq_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 lleq_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 lleq_bind, ldrop_skip, le_minus_to_plus/ -| #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 lleq_flat/ -] -qed-. - -lemma lleq_be: ∀L1,L2,U,d0. L1 ⋕[d0, U] L2 → - ∀K1,K2,d,e. ⇩[d, e] L1 ≡ K1 → ⇩[d, e] L2 ≡ K2 → - ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ d + e → L1 ⋕[d, U] L2. -#L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 -/2 width=1 by lleq_sort, lleq_free, lleq_gref/ -[ #I1 #I2 #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #_ #_ #IHW1 #IHW2 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0de elim (lift_inv_lref2 … H) -H - * #Hid #H destruct [ -Hid0 | -Hd0 ] - [ elim (ldrop_conf_lt … HLK1 … HLK11) // -HLK1 - elim (ldrop_conf_lt … HLK2 … HLK22) // -HLK2 - #L2 #V2 #_ #HKL22 #HVW2 #L1 #V1 #_ #HKL21 #HVW1 - @(lleq_skip … HLK11 HLK22) -HLK11 -HLK22 // - /3 width=8 by arith_k_dx, monotonic_le_minus_l2/ (**) (* full auto fails *) - | -I1 -I2 -K11 -K22 -K1 -K2 -W1 -W2 elim (lt_refl_false … i) -L1 -L2 - @(lt_to_le_to_lt … Hid0) -Hid0 /2 width=3 by transitive_le/ (**) (* full auto too slow *) - ] -| #I #L1 #L2 #K11 #K22 #W #d0 #i #Hid0 #HLK11 #HLK22 #HW #_ #K1 #K2 #d #e #_ #_ #X #H #Hd0 #_ elim (lift_inv_lref2 … H) -H - * #Hid #H destruct - [ -I -K1 -K2 -K11 -K22 -W elim (lt_refl_false i) - @(lt_to_le_to_lt … Hid) -Hid /2 width=3 by transitive_le/ (**) (* full auto too slow *) - | -d0 /3 width=7 by lleq_lref, le_plus_b/ - ] -| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_bind2 … H) -H - #V #T #HVW #HTU #H destruct - @lleq_bind [ /2 width=8 by/ ] -IHW - @(IHU … HTU) -IHU -HTU /2 width=2 by ldrop_skip, le_S_S/ (**) (* full auto too slow *) -| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hde elim (lift_inv_flat2 … H) -H - #V #T #HVW #HTU #H destruct /3 width=8 by lleq_flat/ -] -qed-. - -axiom- lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[d, T] L2). -(* -#T #L1 @(f2_ind … rfw … L1 T) -L1 -T -#n #IH #L1 * * -[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_sort/ -| #i #H1 #L2 elim (eq_nat_dec (|L1|) (|L2|)) - [ #HL12 #d elim (lt_or_ge i d) /3 width=1 by lleq_skip, or_introl/ - #Hdi elim (lt_or_ge i (|L1|)) - #HiL1 elim (lt_or_ge i (|L2|)) /3 width=1 by or_introl, lleq_free/ - #HiL2 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 (eq_term_dec V2 V1) - [ #H3 elim (IH K1 V1 … K2 0) destruct - /3 width=7 by lleq_lref, ldrop_fwd_rfw, or_introl/ - ] - ] - -IH #H3 @or_intror - #H elim (lleq_inv_lref … H) -H [1,3,4,6,7,9: * ] - [1,3,5,7,8,9: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ ] - #I0 #X1 #X2 #V0 #HLX1 #HLX2 #HX12 - lapply (ldrop_mono … HLX1 … HLK1) -HLX1 -HLK1 - lapply (ldrop_mono … HLX2 … HLK2) -HLX2 -HLK2 - #H #H0 destruct /2 width=1 by/ - ] -| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, lleq_gref/ -| #a #I #V #T #Hn #L2 #d destruct - elim (IH L1 V … L2 d) /2 width=1 by/ - elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (d+1)) -IH /3 width=1 by or_introl, lleq_bind/ - #H1 #H2 @or_intror - #H elim (lleq_inv_bind … H) -H /2 width=1 by/ -| #I #V #T #Hn #L2 #d destruct - elim (IH L1 V … L2 d) /2 width=1 by/ - elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, lleq_flat/ - #H1 #H2 @or_intror - #H elim (lleq_inv_flat … H) -H /2 width=1 by/ -] --n /4 width=3 by lleq_fwd_length, or_intror/ -qed-. -*) -(* Main properties **********************************************************) - -axiom- lleq_trans: ∀d,T. Transitive … (lleq d T). -(* -#d #T #L1 #L #H elim H -d -T -L1 -L -/4 width=5 by lleq_fwd_length, lleq_gref, lleq_sort, trans_eq/ -[ #L1 #L #d #i #Hid #HL1 #L2 #H lapply (lleq_fwd_length … H) - #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_skip/ -| #I #L1 #L #K1 #K #V #d #i #Hdi #HLK1 #HLK #_ #IHK1 #L2 #H elim (lleq_inv_lref … H) -H - [ -HLK1 -IHK1 * #HLi #_ elim (lt_refl_false i) - /3 width=5 by ldrop_fwd_length_lt2, lt_to_le_to_lt/ (**) (* slow *) - | -K1 -K #Hid elim (lt_refl_false i) /2 width=3 by lt_to_le_to_lt/ - | * #I0 #K0 #K2 #V0 #HLK0 #HLK2 #HK12 lapply (ldrop_mono … HLK0 … HLK) -L - #H destruct /3 width=7 by lleq_lref/ - ] -| #L1 #L #d #i #HL1i #HLi #HL #L2 #H lapply (lleq_fwd_length … H) - #HL2 elim (lleq_inv_lref … H) -H /2 width=1 by lleq_free/ -| #a #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_bind … H) -H - /3 width=1 by lleq_bind/ -| #I #L1 #L #V #T #d #_ #_ #IHV #IHT #L2 #H elim (lleq_inv_flat … H) -H - /3 width=1 by lleq_flat/ -] -qed-. -*) -theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2. -/3 width=3 by lleq_trans, lleq_sym/ qed-. - -theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2. -/3 width=3 by lleq_trans, lleq_sym/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma index a63a9001a..75cc5ce57 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma @@ -61,6 +61,17 @@ lemma lsuby_length: ∀L1,L2. |L2| ≤ |L1| → L1 ⊑×[yinj 0, yinj 0] L2. ] qed. +lemma lsuby_sym: ∀d,e,L1,L2. L1 ⊑×[d, e] L2 → |L1| = |L2| → L2 ⊑×[d, e] L1. +#d #e #L1 #L2 #H elim H -d -e -L1 -L2 +[ #L1 #d #e #H >(length_inv_zero_dx … H) -L1 // +| /2 width=1 by lsuby_length/ +| #I1 #I2 #L1 #L2 #V #e #_ #IHL12 #H lapply (injective_plus_l … H) + /3 width=1 by lsuby_pair/ +| #I1 #I2 #L1 #L2 #V1 #V2 #d #e #_ #IHL12 #H lapply (injective_plus_l … H) + /3 width=1 by lsuby_succ/ +] +qed-. + (* Basic inversion lemmas ***************************************************) fact lsuby_inv_atom1_aux: ∀L1,L2,d,e. L1 ⊑×[d, e] L2 → L1 = ⋆ → L2 = ⋆. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma deleted file mode 100644 index 582888e21..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma +++ /dev/null @@ -1,32 +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 "basic_2/relocation/fqu_lleq.ma". -include "basic_2/substitution/fqup.ma". - -(* PLUS-ITERATED SUPCLOSURE *************************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[0, T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. -#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U -[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 - /3 width=3 by fqu_fqup, ex2_intro/ -| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 - #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K - /3 width=5 by fqup_strap1, ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma deleted file mode 100644 index 7c0cc1340..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma +++ /dev/null @@ -1,29 +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 "basic_2/substitution/fqup_lleq.ma". -include "basic_2/substitution/fqus_alt.ma". - -(* STAR-ITERATED SUPCLOSURE *************************************************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ → - ∀L1. L1 ⋕[0, T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. -#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H -[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ -| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma index 75833e23b..577343c6e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma @@ -74,6 +74,26 @@ lemma lleq_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → ∀T,d,e. ⇧[d, e] T ≡ U #HU0 elim (cpys_up … HU0 … HTU) // -HU0 /4 width=5 by cpys_weak/ qed-. +lemma lsuby_lleq_trans: ∀L2,L,T,d. L2 ⋕[T, d] L → + ∀L1. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L1 ⋕[T, d] L. +#L2 #L #T #d * #HL2 #IH #L1 #HL12 #H @conj // -HL2 +#U elim (IH U) -IH #Hdx #Hsn @conj #HTU +[ @Hdx -Hdx -Hsn @(lsuby_cpys_trans … HTU) -HTU + /2 width=1 by lsuby_sym/ (**) (* full auto does not work *) +| -H -Hdx /3 width=3 by lsuby_cpys_trans/ +] +qed-. + +lemma lleq_lsuby_trans: ∀L,L1,T,d. L ⋕[T, d] L1 → + ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → L ⋕[T, d] L2. +/5 width=4 by lsuby_lleq_trans, lleq_sym, lsuby_sym/ qed-. + +lemma lleq_lsuby_repl: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀K1. K1 ⊑×[d, ∞] L1 → |K1| = |L1| → + ∀K2. L2 ⊑×[d, ∞] K2 → |L2| = |K2| → + K1 ⋕[T, d] K2. +/3 width=4 by lleq_lsuby_trans, lsuby_lleq_trans/ qed-. + (* Basic forward lemmas *****************************************************) lemma lleq_fwd_length: ∀L1,L2,T,d. L1 ⋕[T, d] L2 → |L1| = |L2|. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma index c7bb1a8a7..9f355b2d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma @@ -81,25 +81,6 @@ lemma lleq_ind_alt: ∀R:relation4 ynat term lenv lenv. ( /3 width=9 by lleqa_inv_lleq/ qed-. -(* Advanced properties ******************************************************) - -lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. -#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1 -/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/ -[ /3 width=3 by lleq_skip, ylt_yle_trans/ -| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2) - [ lapply (lleq_fwd_length … HV) #HK12 #Hid2 - lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) - normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ - | /3 width=8 by lleq_lref, yle_trans/ - ] -] -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. -/3 width=3 by lleq_ge, lleq_bind/ qed. - (* Advanced inversion lemmas ************************************************) fact lleq_inv_S_aux: ∀L1,L2,T,d0. L1 ⋕[T, d0] L2 → ∀d. d0 = d + 1 → @@ -129,3 +110,32 @@ lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → #a #I #L1 #L2 #V #T #H elim (lleq_inv_bind … H) -H /3 width=7 by ldrop_pair, conj, lleq_inv_S/ qed-. + +(* Advanced properties ******************************************************) + +lemma lleq_ge: ∀L1,L2,T,d1. L1 ⋕[T, d1] L2 → ∀d2. d1 ≤ d2 → L1 ⋕[T, d2] L2. +#L1 #L2 #T #d1 #H @(lleq_ind_alt … H) -L1 -L2 -T -d1 +/4 width=1 by lleq_sort, lleq_free, lleq_gref, lleq_bind, lleq_flat, yle_succ/ +[ /3 width=3 by lleq_skip, ylt_yle_trans/ +| #I1 #I2 #L1 #L2 #K1 #K2 #V #d1 #i #Hi #HLK1 #HLK2 #HV #IHV #d2 #Hd12 elim (ylt_split i d2) + [ lapply (lleq_fwd_length … HV) #HK12 #Hid2 + lapply (ldrop_fwd_length … HLK1) lapply (ldrop_fwd_length … HLK2) + normalize in ⊢ (%→%→?); -I1 -I2 -V -d1 /2 width=1 by lleq_skip/ + | /3 width=8 by lleq_lref, yle_trans/ + ] +] +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. +/3 width=3 by lleq_ge, lleq_bind/ qed. + +lemma lleq_bind_repl_SO: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + ∀J,W. L1.ⓑ{J}W ⋕[T, 1] L2.ⓑ{J}W. +#I #L1 #L2 #V #T #HT #J #W lapply (lleq_ge … HT 1 ?) // -HT +#HT @(lleq_lsuby_repl … HT) /2 width=1 by lsuby_succ/ (**) (* full auto fails *) +qed-. + +lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W. +/3 width=7 by lleq_bind_repl_SO, lleq_inv_S/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma new file mode 100644 index 000000000..e4c64833f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma @@ -0,0 +1,75 @@ +(**************************************************************************) +(* ___ *) +(* ||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/fqus_alt.ma". +include "basic_2/substitution/lleq_alt.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Properties on supclosure and derivatives *********************************) + +lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U +[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // + #I1 #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 + #H destruct /2 width=3 by fqu_lref_O, ex2_intro/ +| * [ #a ] #I #G #L2 #V #T #L1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H + /2 width=3 by fqu_pair_sn, ex2_intro/ +| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H + #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/ +| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H + /2 width=3 by fqu_flat_dx, ex2_intro/ +| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12 + elim (ldrop_O1_le (e+1) L1) + [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ + | lapply (ldrop_fwd_length_le2 … HLK2) -K2 + lapply (lleq_fwd_length … HL12) -T -U // + ] +] +qed-. + +lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H +[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. + +lemma lleq_fqup_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃+ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃+ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H @(fqup_ind … H) -G2 -K2 -U +[ #G2 #K2 #U #HTU #L1 #HL12 elim (lleq_fqu_trans … HTU … HL12) -L2 + /3 width=3 by fqu_fqup, ex2_intro/ +| #G #G2 #K #K2 #U #U2 #_ #HU2 #IHTU #L1 #HL12 elim (IHTU … HL12) -L2 + #K1 #HTU #HK1 elim (lleq_fqu_trans … HU2 … HK1) -K + /3 width=5 by fqup_strap1, ex2_intro/ +] +qed-. + +lemma lleq_fqus_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃* ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃* ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fqus_inv_gen … H) -H +[ #H elim (lleq_fqup_trans … H … HL12) -L2 /3 width=3 by fqup_fqus, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. 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 464ae9c75..e920ea057 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 @@ -135,8 +135,8 @@ table { } ] [ { "context-sensitive extended reduction" * } { - [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_leq" + "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_leq" + "cpx_lift" + "cpx_cix" * ] + [ "lpx ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lpx_ldrop" + "lpx_lleq" + "lpx_aaa" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpx_lift" + "cpx_lleq" + "cpx_cix" * ] } ] [ { "context-sensitive extended irreducible forms" * } { @@ -209,7 +209,7 @@ table { class "yellow" [ { "substitution" * } { [ { "lazy equivalence for local environments" * } { - [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_lleq" * ] + [ "lleq ( ? ⋕[?,?] ? )" "lleq_alt ( ? ⋕⋕[?,?] ? )" "lleq_ldrop" + "lleq_fqus" + "lleq_lleq" * ] } ] [ { "contxt-sensitive extended multiple substitution" * } { @@ -217,8 +217,8 @@ table { } ] [ { "iterated structural successor for closures" * } { - [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_lleq" + "fqus_fqus" * ] - [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_lleq" + "fqup_fqup" * ] + [ "fqus ( ⦃?,?,?⦄ ⊃* ⦃?,?,?⦄ )" "fqus_alt" + "fqus_fqus" * ] + [ "fqup ( ⦃?,?,?⦄ ⊃+ ⦃?,?,?⦄ )" "fqup_fqup" * ] } ] [ { "generic local env. slicing" * } { @@ -251,8 +251,8 @@ table { } ] [ { "structural successor for closures" * } { - [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" "fquq_lleq" * ] - [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" "fqu_lleq" * ] + [ "fquq ( ⦃?,?,?⦄ ⊃⸮ ⦃?,?,?⦄ )" "fquq_alt ( ⦃?,?,?⦄ ⊃⊃⸮ ⦃?,?,?⦄ )" * ] + [ "fqu ( ⦃?,?,?⦄ ⊃ ⦃?,?,?⦄ )" * ] } ] [ { "global env. slicing" * } { @@ -260,7 +260,7 @@ table { } ] [ { "basic local env. slicing" * } { - [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_leq" + "ldrop_ldrop" * ] + [ "ldrop ( ⇩[?,?] ? ≡ ? )" "ldrop_append" + "ldrop_lpx_sn" + "ldrop_ldrop" * ] } ] [ { "basic term relocation" * } { @@ -272,10 +272,6 @@ table { ] class "red" [ { "grammar" * } { - [ { "equivalence for local environments" * } { - [ "leq ( ? ≃[?,?] ? )" * ] - } - ] [ { "pointwise extension of a relation" * } { [ "lpx_sn" "lpx_sn_tc" + "lpx_sn_lpx_sn" * ] }