From 6b35f96790b871aa06b22045b4e8e8dd7bba6590 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 25 May 2018 16:39:04 +0200 Subject: [PATCH] partial update update in basic_2 + lpxs reconstructed --- .../basic_2/etc/cpxs/cpxs_fqus.etc | 24 +++++ .../basic_2/etc/lfpxs/lfpxs_cpxs.etc | 27 ------ .../basic_2/etc/lpx_sn/lpx_sn_tc.etc | 91 +++++++++++++++++++ .../lfpxs_lreq.etc => lpxs/lpxs_lreq.etc} | 0 .../lfpxs.ma => etc/referred/lfpxs.etc} | 0 .../referred/lfpxs_aaa.etc} | 0 .../referred/lfpxs_cpxs.etc} | 0 .../referred/lfpxs_drops.etc} | 0 .../referred/lfpxs_ffdeq.etc} | 0 .../referred/lfpxs_fqup.etc} | 0 .../referred/lfpxs_length.etc} | 0 .../referred/lfpxs_lfdeq.etc} | 0 .../referred/lfpxs_lfpxs.etc} | 0 .../referred/lfpxs_lpxs.etc} | 0 .../referred/predtysnstar_5.etc} | 0 .../{predsnstar_5.ma => predsnstar_4.ma} | 4 +- .../lambdadelta/basic_2/relocation/lex_tc.ma | 50 +++++++--- .../basic_2/rt_computation/lpxs.ma | 64 ++++++++++--- .../basic_2/rt_computation/lpxs_aaa.ma | 26 ++++++ .../basic_2/rt_computation/lpxs_cpxs.ma | 48 ++++++++-- .../basic_2/rt_computation/lpxs_drops.ma | 34 +++++++ .../basic_2/rt_computation/lpxs_ffdeq.ma | 29 ++++++ .../basic_2/rt_computation/lpxs_length.ma | 4 +- .../basic_2/rt_computation/lpxs_lfdeq.ma | 50 ++++++++++ .../basic_2/rt_computation/lpxs_lpx.ma | 56 ++++++++++-- .../basic_2/rt_computation/lpxs_lpxs.ma | 24 +++++ .../basic_2/rt_computation/partial.txt | 3 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 28 files changed, 460 insertions(+), 76 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc rename matita/matita/contribs/lambdadelta/basic_2/etc/{lfpxs/lfpxs_lreq.etc => lpxs/lpxs_lreq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs.ma => etc/referred/lfpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_aaa.ma => etc/referred/lfpxs_aaa.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_cpxs.ma => etc/referred/lfpxs_cpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_drops.ma => etc/referred/lfpxs_drops.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_ffdeq.ma => etc/referred/lfpxs_ffdeq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_fqup.ma => etc/referred/lfpxs_fqup.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_length.ma => etc/referred/lfpxs_length.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_lfdeq.ma => etc/referred/lfpxs_lfdeq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_lfpxs.ma => etc/referred/lfpxs_lfpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/lfpxs_lpxs.ma => etc/referred/lfpxs_lpxs.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predtysnstar_5.ma => etc/referred/predtysnstar_5.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{predsnstar_5.ma => predsnstar_4.ma} (87%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc new file mode 100644 index 000000000..2509cf852 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_fqus.etc @@ -0,0 +1,24 @@ +(* Properties on supclosure *************************************************) + +lemma lpx_fqup_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H12 #K1 #HKL1 elim (lpx_fqu_trans … H12 … HKL1) -L1 + /3 width=5 by cpx_cpxs, fqu_fqup, ex3_2_intro/ +| #G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 + #L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fqu_trans … H2 … HL0) -L + #L #T3 #HT3 #HT32 #HL2 elim (fqup_cpx_trans … HT0 … HT3) -T + /3 width=7 by cpxs_strap1, fqup_strap1, ex3_2_intro/ +] +qed-. + +lemma lpx_fqus_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡[h, g] L1 → + ∃∃K2,T. ⦃G1, K1⦄ ⊢ T1 ➡*[h, g] T & ⦃G1, K1, T⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡[h, g] L2. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -G2 -L2 -T2 [ /2 width=5 by ex3_2_intro/ ] +#G #G2 #L #L2 #T #T2 #_ #H2 #IH1 #K1 #HLK1 elim (IH1 … HLK1) -L1 +#L0 #T0 #HT10 #HT0 #HL0 elim (lpx_fquq_trans … H2 … HL0) -L +#L #T3 #HT3 #HT32 #HL2 elim (fqus_cpx_trans … HT0 … HT3) -T +/3 width=7 by cpxs_strap1, fqus_strap1, ex3_2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc deleted file mode 100644 index a6eb3b6ac..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc +++ /dev/null @@ -1,27 +0,0 @@ -(* Advanced inversion lemmas ************************************************) - -lemma lpxs_inv_pair1: ∀h,o,I,G,K1,L2,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L2 = K2.ⓑ{I}V2. -/3 width=3 by TC_lpx_sn_inv_pair1, lpx_cpxs_trans/ qed-. - -lemma lpxs_inv_pair2: ∀h,o,I,G,L1,K2,V2. ⦃G, L1⦄ ⊢ ➡*[h, o] K2.ⓑ{I}V2 → - ∃∃K1,V1. ⦃G, K1⦄ ⊢ ➡*[h, o] K2 & ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 & L1 = K1.ⓑ{I}V1. -/3 width=3 by TC_lpx_sn_inv_pair2, lpx_cpxs_trans/ qed-. - -(* Advanced eliminators *****************************************************) - -lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv. - R (⋆) (⋆) → ( - ∀I,K1,K2,V1,V2. - ⦃G, K1⦄ ⊢ ➡*[h, o] K2 → ⦃G, K1⦄ ⊢ V1 ➡*[h, o] V2 → - R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) - ) → - ∀L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → R L1 L2. -/3 width=4 by TC_lpx_sn_ind, lpx_cpxs_trans/ qed-. - - -(* More advanced properties *************************************************) - -lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2. -/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc new file mode 100644 index 000000000..51b09380f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc @@ -0,0 +1,91 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lpx_sn.ma". + +(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) + +(* Properties on transitive_closure *****************************************) + +lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). +#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 +[ /2 width=1 by lpx_sn_refl/ +| /3 width=1 by TC_reflexive, lpx_sn_refl/ +| /3 width=5 by lpx_sn_pair, step/ +] +qed-. + +lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → + ∀V1,V2. LTC … R L1 V1 V2 → + TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). +#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // +[ /2 width=1 by TC_lpx_sn_pair_refl/ +| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ +] +qed-. + +(* Inversion lemmas on transitive closure ***********************************) + +lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. +#R #L1 #H @(TC_ind_dx … L1 H) -L1 +[ /2 width=2 by lpx_sn_inv_atom2/ +| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ +] +qed-. + +lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → + ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. +#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 +[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ +| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct + elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct + lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. +#R #L2 #H elim H -L2 +[ /2 width=2 by lpx_sn_inv_atom1/ +| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ +] +qed-. + +fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀L1,L2. TC … (lpx_sn R) L1 L2 → + ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 +[ #J #K #W #H destruct +| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → + ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → + ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. +/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. + +(* Forward lemmas on transitive closure *************************************) + +lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. +#R #L1 #L2 #H elim H -L2 +[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc rename to matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma similarity index 87% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma index 095cc3e31..a12748a9b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡ * [ break term 46 h, break term 46 o ] break term 46 L2 )" +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡*[ break term 46 h ] break term 46 L2 )" non associative with precedence 45 - for @{ 'PRedSnStar $h $o $G $L1 $L2 }. + for @{ 'PRedSnStar $h $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma index 9e48f4d36..a9ed87b92 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lex_tc.ma @@ -23,14 +23,14 @@ alias symbol "subseteq" = "relation inclusion". (* Inversion lemmas with transitive closure *********************************) (* Basic_2A1: was: lpx_sn_LTC_TC_lpx_sn *) -lemma lex_inv_CTC: ∀R. c_reflexive … R → - lex (CTC … R) ⊆ TC … (lex R). +lemma lex_inv_CTC (R): c_reflexive … R → + lex (CTC … R) ⊆ TC … (lex R). #R #HR #L1 #L2 * /5 width=11 by lexs_inv_tc_dx, lexs_co, ext2_inv_tc, ext2_refl, monotonic_TC, ex2_intro/ qed-. -lemma s_rs_transitive_lex_inv_isid: ∀R. s_rs_transitive … R (λ_.lex R) → - s_rs_transitive_isid cfull (cext2 R). +lemma s_rs_transitive_lex_inv_isid (R): s_rs_transitive … R (λ_.lex R) → + s_rs_transitive_isid cfull (cext2 R). #R #HR #f #Hf #L2 #T1 #T2 #H #L1 #HL12 elim (ext2_tc … H) -H [ /3 width=1 by ext2_inv_tc, ext2_unit/ @@ -43,8 +43,8 @@ qed-. (* Properties with transitive closure ***************************************) (* Basic_2A1: was: TC_lpx_sn_inv_lpx_sn_LTC *) -lemma lex_CTC: ∀R. s_rs_transitive … R (λ_. lex R) → - TC … (lex R) ⊆ lex (CTC … R). +lemma lex_CTC (R): s_rs_transitive … R (λ_. lex R) → + TC … (lex R) ⊆ lex (CTC … R). #R #HR #L1 #L2 #HL12 lapply (monotonic_TC … (lexs cfull (cext2 R) 𝐈𝐝) … HL12) -HL12 [ #L1 #L2 * /3 width=3 by lexs_eq_repl_fwd, eq_id_inv_isid/ @@ -52,12 +52,38 @@ lapply (monotonic_TC … (lexs cfull (cext2 R) 𝐈𝐝) … HL12) -HL12 ] qed-. -lemma lex_CTC_step_dx: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) → - ∀L1,L. lex (CTC … R) L1 L → - ∀L2. lex R L L2 → lex (CTC … R) L1 L2. +lemma lex_CTC_inj (R): s_rs_transitive … R (λ_. lex R) → + (lex R) ⊆ lex (CTC … R). +/3 width=1 by lex_CTC, inj/ qed-. + +lemma lex_CTC_step_dx (R): c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀L1,L. lex (CTC … R) L1 L → + ∀L2. lex R L L2 → lex (CTC … R) L1 L2. /4 width=3 by lex_CTC, lex_inv_CTC, step/ qed-. -lemma lex_CTC_step_sn: ∀R. c_reflexive … R → s_rs_transitive … R (λ_. lex R) → - ∀L1,L. lex R L1 L → - ∀L2. lex (CTC … R) L L2 → lex (CTC … R) L1 L2. +lemma lex_CTC_step_sn (R): c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀L1,L. lex R L1 L → + ∀L2. lex (CTC … R) L L2 → lex (CTC … R) L1 L2. /4 width=3 by lex_CTC, lex_inv_CTC, TC_strap/ qed-. + +(* Eliminators with transitive closure **************************************) + +lemma lex_CTC_ind_sn (R) (L2): c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀Q:predicate lenv. Q L2 → + (∀L1,L. L1 ⪤[R] L → L ⪤[CTC … R] L2 → Q L → Q L1) → + ∀L1. L1 ⪤[CTC … R] L2 → Q L1. +#R #L2 #H1R #H2R #Q #IH1 #IH2 #L1 #H +lapply (lex_inv_CTC … H1R … H) -H #H +@(TC_star_ind_dx ???????? H) -H +/3 width=4 by lex_CTC, lex_refl/ +qed-. + +lemma lex_CTC_ind_dx (R) (L1): c_reflexive … R → s_rs_transitive … R (λ_. lex R) → + ∀Q:predicate lenv. Q L1 → + (∀L,L2. L1 ⪤[CTC … R] L → L ⪤[R] L2 → Q L → Q L2) → + ∀L2. L1 ⪤[CTC … R] L2 → Q L2. +#R #L1 #H1R #H2R #Q #IH1 #IH2 #L2 #H +lapply (lex_inv_CTC … H1R … H) -H #H +@(TC_star_ind ???????? H) -H +/3 width=4 by lex_CTC, lex_refl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma index 4969c4c73..d6538eb9f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs.ma @@ -16,30 +16,66 @@ include "basic_2/notation/relations/predtysnstar_4.ma". include "basic_2/relocation/lex.ma". include "basic_2/rt_computation/cpxs_ext.ma". -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************) +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) -definition lpxs: ∀h. relation3 genv lenv lenv ≝ - λh,G. lex (cpxs h G). +definition lpxs (h) (G): relation lenv ≝ + lex (cpxs h G). interpretation - "unbound parallel rt-computation (local environment)" + "unbound parallel rt-computation on all entries (local environment)" 'PRedTySnStar h G L1 L2 = (lpxs h G L1 L2). (* Basic properties *********************************************************) -lemma lpxs_refl: ∀h,G. reflexive … (lpxs h G). +(* Basic_2A1: uses: lpxs_pair_refl *) +lemma lpxs_bind_refl_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + ∀I. ⦃G, L1.ⓘ{I}⦄ ⊢ ⬈*[h] L2.ⓘ{I}. +/2 width=1 by lex_bind_refl_dx/ qed. + +lemma lpxs_pair (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + ∀V1,V2. ⦃G, L1⦄ ⊢ V1 ⬈*[h] V2 → + ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2.ⓑ{I}V2. +/2 width=1 by lex_pair/ qed. + +lemma lpxs_refl (h) (G): reflexive … (lpxs h G). /2 width=1 by lex_refl/ qed. (* Basic inversion lemmas ***************************************************) -lemma lpxs_inv_bind_sn: ∀h,G,I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 → - ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}. +(* Basic_2A1: was: lpxs_inv_atom1 *) +lemma lpxs_inv_atom_sn (h) (G): ∀L2. ⦃G, ⋆⦄ ⊢ ⬈*[h] L2 → L2 = ⋆. +/2 width=2 by lex_inv_atom_sn/ qed-. + +lemma lpxs_inv_bind_sn (h) (G): ∀I1,L2,K1. ⦃G, K1.ⓘ{I1}⦄ ⊢⬈*[h] L2 → + ∃∃I2,K2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ I1 ⬈*[h] I2 & L2 = K2.ⓘ{I2}. /2 width=1 by lex_inv_bind_sn/ qed-. -lemma lpxs_inv_pair_sn: ∀h,G,I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 → - ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2. -#h #G #I #L2 #K1 #V1 #H -elim (lpxs_inv_bind_sn … H) -H #Y #K2 #HK12 #H0 #H destruct -elim (ext2_inv_pair_sn … H0) -H0 #V2 #HV12 #H destruct -/2 width=5 by ex3_2_intro/ -qed-. +(* Basic_2A1: was: lpxs_inv_pair1 *) +lemma lpxs_inv_pair_sn (h) (G): ∀I,L2,K1,V1. ⦃G, K1.ⓑ{I}V1⦄ ⊢⬈*[h] L2 → + ∃∃K2,V2. ⦃G, K1⦄ ⊢⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L2 = K2.ⓑ{I}V2. +/2 width=1 by lex_inv_pair_sn/ qed-. + +(* Basic_2A1: was: lpxs_inv_atom2 *) +lemma lpxs_inv_atom_dx (h) (G): ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] ⋆ → L1 = ⋆. +/2 width=2 by lex_inv_atom_dx/ qed-. + +(* Basic_2A1: was: lpxs_inv_pair2 *) +lemma lpxs_inv_pair_dx (h) (G): ∀I,L1,K2,V2. ⦃G, L1⦄ ⊢ ⬈*[h] K2.ⓑ{I}V2 → + ∃∃K1,V1. ⦃G, K1⦄ ⊢ ⬈*[h] K2 & ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 & L1 = K1.ⓑ{I}V1. +/2 width=1 by lex_inv_pair_dx/ qed-. + +(* Basic eliminators ********************************************************) + +(* Basic_2A1: was: lpxs_ind_alt *) +lemma lpxs_ind (h) (G): ∀R:relation lenv. + R (⋆) (⋆) → ( + ∀I,K1,K2. + ⦃G, K1⦄ ⊢ ⬈*[h] K2 → + R K1 K2 → R (K1.ⓘ{I}) (K2.ⓘ{I}) + ) → ( + ∀I,K1,K2,V1,V2. + ⦃G, K1⦄ ⊢ ⬈*[h] K2 → ⦃G, K1⦄ ⊢ V1 ⬈*[h] V2 → + R K1 K2 → R (K1.ⓑ{I}V1) (K2.ⓑ{I}V2) + ) → + ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1 L2. +/3 width=4 by lex_ind/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma new file mode 100644 index 000000000..3ec241468 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_aaa.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lpx_aaa.ma". +include "basic_2/rt_computation/lpxs_lpx.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) + +(* Properties with atomic arity assignment for terms ************************) + +lemma lpxs_aaa_conf (h) (G) (T): Conf3 … (λL. aaa G L T) (lpxs h G). +#h #G #T #A #L1 #HT #L2 #H +lapply (lex_inv_CTC … H) -H // +@TC_Conf3 [4: // |*: /2 width=4 by lpx_aaa_conf/ ] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma index 19cc746fc..10831ed73 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_cpxs.ma @@ -12,15 +12,47 @@ (* *) (**************************************************************************) -include "basic_2/rt_computation/lfpxs_cpxs.ma". -include "basic_2/rt_computation/lfpxs_lpxs.ma". +include "basic_2/rt_computation/lpxs_lpx.ma". -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************) +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) -(* Properties with unbound context-sensitive rt-computation for terms *******) +(* Properties with context-sensitive extended rt-computation for terms ******) -lemma lpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (λ_.lpxs h G). -/3 width=3 by lfpxs_cpx_trans, lfpxs_lpxs/ qed-. +(* Basic_2A1: was: cpxs_bind2 *) +lemma cpxs_bind_dx (h) (G): ∀L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀I,T1,T2. ⦃G, L.ⓑ{I}V2⦄ ⊢ T1 ⬈*[h] T2 → + ∀p. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈*[h] ⓑ{p,I}V2.T2. +/4 width=5 by lpxs_cpxs_trans, lpxs_pair, cpxs_bind/ qed. -lemma lpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (λ_.lpxs h G). -/3 width=3 by lfpxs_cpxs_trans, lfpxs_lpxs/ qed-. +(* Inversion lemmas with context-sensitive ext rt-computation for terms *****) + +lemma cpxs_inv_abst1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓛ{p}V1.T1 ⬈*[h] U2 → + ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓛV1⦄ ⊢ T1 ⬈*[h] T2 & + U2 = ⓛ{p}V2.T2. +#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /2 width=5 by ex3_2_intro/ +#U0 #U2 #_ #HU02 * #V0 #T0 #HV10 #HT10 #H destruct +elim (cpx_inv_abst1 … HU02) -HU02 #V2 #T2 #HV02 #HT02 #H destruct +lapply (lpxs_cpx_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro/ +qed-. + +lemma cpxs_inv_abbr1 (h) (G): ∀p,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈*[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & + U2 = ⓓ{p}V2.T2 + | ∃∃T2. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈*[h] T2 & ⬆*[1] U2 ≘ T2 & p = Ⓣ. +#h #G #p #L #V1 #T1 #U2 #H @(cpxs_ind … H) -U2 /3 width=5 by ex3_2_intro, or_introl/ +#U0 #U2 #_ #HU02 * * +[ #V0 #T0 #HV10 #HT10 #H destruct + elim (cpx_inv_abbr1 … HU02) -HU02 * + [ #V2 #T2 #HV02 #HT02 #H destruct + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lpxs_pair, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ + | #T2 #HT02 #HUT2 + lapply (lpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lpxs_pair, cpxs_trans, ex3_intro, or_intror/ + ] +| #U1 #HTU1 #HU01 #Hp + elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) -U0 /3 width=3 by drops_refl, drops_drop/ #U #HU2 #HU1 + /4 width=3 by cpxs_strap1, ex3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma new file mode 100644 index 000000000..0482e3d19 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_drops.ma @@ -0,0 +1,34 @@ +(**************************************************************************) +(* ___ *) +(* ||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/drops_lex.ma". +include "basic_2/rt_computation/cpxs_drops.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: was: drop_lpxs_trans *) +lemma drops_lpxs_trans (h) (G): dedropable_sn (cpxs h G). +/3 width=6 by lex_liftable_dedropable_sn, cpxs_lifts_sn/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: was: lpxs_drop_conf *) +lemma lpxs_drops_conf (h) (G): dropable_sn (cpxs h G). +/2 width=3 by lex_dropable_sn/ qed-. + +(* Basic_2A1: was: lpxs_drop_trans_O1 *) +lemma lpxs_drops_trans (h) (G): dropable_dx (cpxs h G). +/2 width=3 by lex_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma new file mode 100644 index 000000000..530c5e15c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_ffdeq.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/ffdeq.ma". +include "basic_2/rt_computation/lpxs_lfdeq.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) + +(* Properties with degree-based equivalence on closures *********************) + +lemma ffdeq_lpxs_trans (h) (o): ∀G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ → + ∀L2. ⦃G2, L0⦄ ⊢⬈*[h] L2 → + ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h] L & ⦃G1, L, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄. +#h #o #G1 #G2 #L1 #L0 #T1 #T2 #H1 #L2 #HL02 +elim (ffdeq_inv_gen_dx … H1) -H1 #HG #HL10 #HT12 destruct +elim (lfdeq_lpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02 +/3 width=3 by ffdeq_intro_dx, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma index 40c4dc8ef..46dbd458d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_length.ma @@ -15,9 +15,9 @@ include "basic_2/relocation/lex_length.ma". include "basic_2/rt_computation/lpxs.ma". -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************) +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) (* Forward lemmas with length for local environments ************************) -lemma lpxs_fwd_length: ∀h,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|. +lemma lpxs_fwd_length (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → |L1| = |L2|. /2 width=2 by lex_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma new file mode 100644 index 000000000..640c52779 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lfdeq.ma @@ -0,0 +1,50 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_transition/lpx_lfdeq.ma". +include "basic_2/rt_computation/lpxs_lpx.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) + +(* Properties with degree-based equivalence on referred entries *************) + +(* Basic_2A1: uses: lleq_lpxs_trans *) +lemma lfdeq_lpxs_trans (h) (o) (G) (T:term): ∀L2,K2. ⦃G, L2⦄ ⊢ ⬈*[h] K2 → + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h] K1 & K1 ≛[h, o, T] K2. +#h #o #G #T #L2 #K2 #H @(lpxs_ind_sn … H) -L2 /2 width=3 by ex2_intro/ +#L #L2 #HL2 #_ #IH #L1 #HT +elim (lfdeq_lpx_trans … HL2 … HT) -L #L #HL1 #HT +elim (IH … HT) -L2 #K #HLK #HT +/3 width=3 by lpxs_step_sn, ex2_intro/ +qed-. + +(* Basic_2A1: uses: lpxs_nlleq_inv_step_sn *) +lemma lpxs_lfdneq_inv_step_sn (h) (o) (G) (T:term): + ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → (L1 ≛[h, o, T] L2 → ⊥) → + ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h] L & L1 ≛[h, o, T] L → ⊥ & + ⦃G, L⦄ ⊢ ⬈*[h] L0 & L0 ≛[h, o, T] L2. +#h #o #G #T #L1 #L2 #H @(lpxs_ind_sn … H) -L1 +[ #H elim H -H // +| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H + [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lfdeq_trans/ -H12 + #L0 #L3 #H1 #H2 #H3 #H4 lapply (lfdeq_lfdneq_trans … H … H2) -H2 + #H2 elim (lfdeq_lpx_trans … H1 … H) -L + #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2 + #H2 elim (lfdeq_lpxs_trans … H3 … H) -L0 + /3 width=8 by lfdeq_trans, ex4_2_intro/ + | -H12 -IH2 /3 width=6 by ex4_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma index d12f1fe67..7bc58ea45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpx.ma @@ -16,16 +16,56 @@ include "basic_2/relocation/lex_tc.ma". include "basic_2/rt_computation/lpxs.ma". include "basic_2/rt_computation/cpxs_lpx.ma". -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENVIRONMENTS *******************) +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) -(* Properties with unbound rt-transition for local environments *************) +(* Properties with unbound rt-transition for full local environments ********) -(* Basic_2A1: was: lpxs_strap1 *) -lemma lpxs_step_dx: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → - ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. -/3 width=3 by lpx_cpxs_trans, lex_CTC_step_dx/ qed-. +lemma lpx_lpxs (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. +/3 width=3 by lpx_cpxs_trans, lex_CTC_inj/ qed. (* Basic_2A1: was: lpxs_strap2 *) -lemma lpxs_step_sn: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → - ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. +lemma lpxs_step_sn (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → + ∀L2. ⦃G, L⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. /3 width=3 by lpx_cpxs_trans, lex_CTC_step_sn/ qed-. + +(* Basic_2A1: was: lpxs_strap1 *) +lemma lpxs_step_dx (h) (G): ∀L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → + ∀L2. ⦃G, L⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h] L2. +/3 width=3 by lpx_cpxs_trans, lex_CTC_step_dx/ qed-. + +(* Eliminators with unbound rt-transition for full local environments *******) + +(* Basic_2A1: was: lpxs_ind_dx *) +lemma lpxs_ind_sn (h) (G) (L2): ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h] L → ⦃G, L⦄ ⊢ ⬈*[h] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L1. +/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_sn/ qed-. + +(* Basic_2A1: was: lpxs_ind *) +lemma lpxs_ind_dx (h) (G) (L1): ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L → ⦃G, L⦄ ⊢ ⬈[h] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → R L2. +/3 width=7 by lpx_cpxs_trans, cpx_refl, lex_CTC_ind_dx/ qed-. + +(* Properties with context-sensitive extended rt-transition for terms *******) + +lemma lpxs_cpx_trans (h) (G): s_r_transitive … (cpx h G) (λ_.lpxs h G). +#h #G #L2 #T1 #T2 #HT12 #L1 #HL12 +@(s_r_trans_CTC2 ???????? HT12) -HT12 +/2 width=4 by lpx_cpxs_trans, lex_inv_CTC/ +qed-. + +(* Properties with context-sensitive extended rt-computation for terms ******) + +(* Note: alternative proof by s_r_to_s_rs_trans *) +lemma lpxs_cpxs_trans (h) (G): s_rs_transitive … (cpx h G) (λ_.lpxs h G). +#h #G @s_r_trans_CTC1 /2 width=3 by lpxs_cpx_trans/ +qed-. + +(* Advanced properties ******************************************************) + +(* Basic_2A1: was: lpxs_pair2 *) +lemma lpxs_pair_dx (h) (G): ∀L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → + ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ⬈*[h] V2 → + ∀I. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈*[h] L2.ⓑ{I}V2. +/3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma new file mode 100644 index 000000000..f4acf7091 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lex_lex.ma". +include "basic_2/rt_computation/cpxs_cpxs.ma". +include "basic_2/rt_computation/lpxs_lpx.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR FULL LOCAL ENVIRONMENTS **************) + +(* Main properties **********************************************************) + +theorem lpxs_trans (h) (G): Transitive … (lpxs h G). +/4 width=5 by lpxs_cpxs_trans, cpxs_trans, lex_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index be67912d6..05ddbc263 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,7 +1,6 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_lsubr.ma cpxs_lfdeq.ma cpxs_ffdeq.ma cpxs_aaa.ma cpxs_lpx.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma cpxs_ext.ma -lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma -lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_ffdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma +lpxs.ma lpxs_length.ma lpxs_drops.ma lpxs_lfdeq.ma lpxs_ffdeq.ma lpxs_aaa.ma lpxs_lpx.ma lpxs_cpxs.ma lpxs_lpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_ffdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_fpbq.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma 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 71ca47a56..33aa9459d 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 @@ -95,7 +95,7 @@ table { [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_ffdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_fpbq" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_ffdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] - [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ] + [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_drops" + "lpxs_lfdeq" + "lpxs_ffdeq" + "lpxs_aaa" + "lpxs_lpx" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] [ [ "for terms" ] "cpxs" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_fqus" + "cpxs_lsubr" + "cpxs_lfdeq" + "cpxs_ffdeq" + "cpxs_aaa" + "cpxs_lpx" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } -- 2.39.2