From dca4170c5ce5f2cd6be8ae1dc0422bd6a680b43f Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 10 Jan 2014 18:05:18 +0000 Subject: [PATCH] new definition of lleq allows to complete the proof of lemma 1000 (lleq_cpx_conf_dx)! --- .../basic_2/computation/cpxs_lleq.ma | 6 +- .../lambdadelta/basic_2/computation/fpbu.ma | 6 +- .../lambdadelta/basic_2/computation/fpns.ma | 6 +- .../basic_2/computation/fpns_fpns.ma | 2 +- .../basic_2/computation/fsb_csx.ma | 4 +- .../basic_2/computation/lpxs_lleq.ma | 28 +- .../lambdadelta/basic_2/computation/lsx.ma | 6 +- .../basic_2/computation/lsx_cpxs.ma | 2 +- .../cpx_leq.ma => etc/leq/cpx_leq.etc} | 0 .../relations/iso_4.ma => etc/leq/iso_4.etc} | 0 .../ldrop_leq.ma => etc/leq/ldrop_leq.etc} | 0 .../lambdadelta/basic_2/etc/leq/leq.etc | 88 ++-- .../lambdadelta/basic_2/etc/leq/leq_nat.etc | 65 +++ .../lpx_leq.ma => etc/leq/lpx_leq.etc} | 1 - .../basic_2/etc/preservation/snv_cpcs.etc | 161 ------- .../basic_2/etc/preservation/snv_ltpr.etc | 113 ----- .../etc/preservation/snv_ssta_ltpr.etc | 120 ----- .../lambdadelta/basic_2/grammar/leq.ma | 81 ---- .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 74 +++ .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 20 +- .../basic_2/relocation/fquq_lleq.ma | 29 -- .../lambdadelta/basic_2/relocation/lleq.ma | 163 ------- .../basic_2/relocation/lleq_lleq.ma | 441 ------------------ .../lambdadelta/basic_2/relocation/lsuby.ma | 11 + .../basic_2/substitution/fqup_lleq.ma | 32 -- .../basic_2/substitution/fqus_lleq.ma | 29 -- .../lambdadelta/basic_2/substitution/lleq.ma | 20 + .../basic_2/substitution/lleq_alt.ma | 48 +- .../fqu_lleq.ma => substitution/lleq_fqus.ma} | 44 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 20 +- 30 files changed, 336 insertions(+), 1284 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cpx_leq.ma => etc/leq/cpx_leq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/iso_4.ma => etc/leq/iso_4.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/ldrop_leq.ma => etc/leq/ldrop_leq.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/leq/leq_nat.etc rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_leq.ma => etc/leq/lpx_leq.etc} (99%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_cpcs.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ltpr.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/preservation/snv_ssta_ltpr.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/leq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma rename matita/matita/contribs/lambdadelta/basic_2/{relocation/fqu_lleq.ma => substitution/lleq_fqus.ma} (52%) 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/reduction/cpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/leq/cpx_leq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/iso_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/leq/iso_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/leq/ldrop_leq.etc 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/reduction/lpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc similarity index 99% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc index 17c2dc14d..b2b5324a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/leq/lpx_leq.etc @@ -24,7 +24,6 @@ axiom- lleq_beta: ∀L2s,L2d,V2,W2,T2,d. (* 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 → 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) (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/relocation/fqu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma similarity index 52% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma index 530f4dfa5..e4c64833f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma @@ -12,19 +12,19 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lleq_lleq.ma". -include "basic_2/relocation/fqu.ma". +include "basic_2/substitution/fqus_alt.ma". +include "basic_2/substitution/lleq_alt.ma". -(* SUPCLOSURE ***************************************************************) +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) -(* Properties on 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 ⋕[0, T] L2 → - ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[0, U] K2. + ∀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 // - #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 + #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) @@ -43,3 +43,33 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, 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" * ] } -- 2.39.2