From: Ferruccio Guidi Date: Fri, 25 May 2018 14:39:04 +0000 (+0200) Subject: partial update update in basic_2 X-Git-Tag: make_still_working~316 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6b35f96790b871aa06b22045b4e8e8dd7bba6590;hp=05b047be6817f430c8c72fd9b0902df8bb9f579e;p=helm.git partial update update in basic_2 + lpxs reconstructed --- 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/lfpxs/lfpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc deleted file mode 100644 index fc77921e7..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc +++ /dev/null @@ -1,29 +0,0 @@ -fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → - ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & - (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). -#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k -[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H - /3 width=5 by ex3_intro, conj/ -| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct -| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H - elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct - lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm - elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/ -| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H - elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct - elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lreq_succ/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/ -] -qed-. - -lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → - ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & - (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). -/2 width=1 by lreq_lpxs_trans_lleq_aux/ 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/lpxs/lpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc new file mode 100644 index 000000000..fc77921e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpxs/lpxs_lreq.etc @@ -0,0 +1,29 @@ +fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → + ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & + (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). +#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k +[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct +| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lreq_succ/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/ +] +qed-. + +lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → + ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & + (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). +/2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc new file mode 100644 index 000000000..0e1bee1d1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs.etc @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/notation/relations/predtysnstar_5.ma". +include "basic_2/i_static/tc_lfxs.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +definition lfpxs: ∀h. relation4 genv term lenv lenv ≝ + λh,G. tc_lfxs (cpx h G). + +interpretation + "unbound parallel rt-computation on referred entries (local environment)" + 'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2). + +(* Basic properties *********************************************************) + +(* Basic_2A1: was just: lpx_lpxs *) +lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=1 by inj/ qed. + +lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_step_dx/ qed. + +lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_step_sn/ qed. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: uses: lpxs_inv_atom1 *) +lemma lfpxs_inv_atom1: ∀h,I,G,L2. ⦃G, ⋆⦄ ⊢ ⬈*[h, ⓪{I}] L2 → L2 = ⋆. +/2 width=3 by tc_lfxs_inv_atom_sn/ qed-. + +(* Basic_2A1: uses: lpxs_inv_atom2 *) +lemma lfpxs_inv_atom2: ∀h,I,G,L1. ⦃G, L1⦄ ⊢ ⬈*[h, ⓪{I}] ⋆ → L1 = ⋆. +/2 width=3 by tc_lfxs_inv_atom_dx/ qed-. + +(* Basic forward lemmas *****************************************************) + +lemma lfpxs_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, V] L2. +/2 width=3 by tc_lfxs_fwd_pair_sn/ qed-. + +lemma lfpxs_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_fwd_flat_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc new file mode 100644 index 000000000..43febff41 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_aaa.etc @@ -0,0 +1,25 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpx_aaa.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with atomic arity assignment on terms *************************) + +(* Basic_2A1: uses: lpxs_aaa_conf *) +lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T). +#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc new file mode 100644 index 000000000..a5288e11a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_cpxs.etc @@ -0,0 +1,76 @@ +(**************************************************************************) +(* ___ *) +(* ||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_computation/cpxs_lfpx.ma". +include "basic_2/rt_computation/lfpxs_fqup.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with unbound context-sensitive rt-computation for terms *******) + +(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *) +lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → + ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2. +/2 width=1 by tc_lfxs_pair_refl/ qed. + +lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G). +#h #G @s_r_trans_CTC2 @lfpx_cpxs_trans (**) (* auto fails *) +qed-. + +(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_CTC1 *) +lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G). +#h #G @s_r_to_s_rs_trans @s_r_trans_CTC2 +@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *) +qed-. + +(* Advanced properties on unbound rt-computation for terms ******************) + +lemma cpxs_bind2: ∀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=3 by lfpxs_cpxs_trans, lfpxs_pair_refl, cpxs_bind/ qed. + +(* Advanced inversion lemmas on unbound rt-computation for terms ************) + +lemma cpxs_inv_abst1: ∀h,p,G,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 #p #G #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 (lfpxs_cpx_trans … HT02 (L.ⓛV1) ?) +/3 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro/ +qed-. + +lemma cpxs_inv_abbr1: ∀h,p,G,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 = true. +#h #p #G #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 (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) + /4 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ + | #T2 #HT02 #HUT2 + lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 + /4 width=3 by lfpxs_pair_refl, cpxs_trans, ex3_intro, or_intror/ + ] +| #U1 #HTU1 #HU01 + elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) + /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc new file mode 100644 index 000000000..caeb2bf77 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_drops.etc @@ -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/i_static/tc_lfxs_drops.ma". +include "basic_2/rt_transition/lfpx_drops.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with generic slicing for local environments *******************) + +(* Basic_2A1: uses: drop_lpxs_trans *) +lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G). +/3 width=5 by drops_lfpx_trans, dedropable_sn_CTC/ qed-. + +(* Inversion lemmas with generic slicing for local environments *************) + +(* Basic_2A1: uses: lpxs_drop_conf *) +lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G). +/3 width=5 by lfpx_drops_conf, dropable_sn_CTC/ qed-. + +(* Basic_2A1: uses: lpxs_drop_trans_O1 *) +lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G). +/3 width=5 by lfpx_drops_trans, dropable_dx_CTC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc new file mode 100644 index 000000000..35ed9931b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_ffdeq.etc @@ -0,0 +1,30 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpxs_lfdeq.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with degree-based equivalence on closures *********************) + +lemma ffdeq_lfpxs_trans: ∀h,o,G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ → + ∀L2. ⦃G2, L0⦄ ⊢⬈*[h, T2] L2 → + ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h, T1] 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_lfpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02 +lapply (tdeq_lfpxs_trans … HT12 … HL10) -HL10 #HL10 +/3 width=3 by ffdeq_intro_dx, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc new file mode 100644 index 000000000..1ca306ddb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_fqup.etc @@ -0,0 +1,49 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/i_static/tc_lfxs_fqup.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Advanced properties ******************************************************) + +lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T). +/2 width=1 by tc_lfxs_refl/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. +/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-. + +lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ. +/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-. + +(* Advanced eliminators *****************************************************) + +(* Basic_2A1: uses: lpxs_ind *) +lemma lfpxs_ind_sn: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. +#h #G @tc_lfxs_ind_sn // (**) (* auto fails *) +qed-. + +(* Basic_2A1: uses: lpxs_ind_dx *) +lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 → + (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) → + ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1. +#h #G @tc_lfxs_ind_dx // (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc new file mode 100644 index 000000000..27bf18d49 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_length.etc @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs_length.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Forward lemmas with length for local environments ************************) + +lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|. +/2 width=3 by tc_lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc new file mode 100644 index 000000000..2d6871c34 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfdeq.etc @@ -0,0 +1,58 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lfpx_lfdeq.ma". +include "basic_2/rt_computation/lfpxs_fqup.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with degree-based equivalence on terms ************************) + +lemma lfpxs_tdeq_trans: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpxs h G). +#h #o #G #L1 #T1 #T2 #HT12 #L2 #H @(lfpxs_ind_sn … H) -L2 +/3 width=6 by lfpxs_step_dx, lfpx_tdeq_conf/ +qed-. + +lemma tdeq_lfpxs_trans: ∀h,o,T1,T2. T1 ≛[h, o] T2 → + ∀G,L1,L2. ⦃G, L1⦄ ⊢⬈*[h, T2] L2 → ⦃G, L1⦄ ⊢⬈*[h, T1] L2. +/3 width=4 by lfpxs_tdeq_trans, tdeq_sym/ qed-. + +(* Properties with degree-based equivalence on referred entries *************) + +(* Basic_2A1: was: lleq_lpxs_trans *) +lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 → + ∀L1. L1 ≛[h, o, T] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≛[h, o, T] K2. +#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/ +#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2 +#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K +/3 width=3 by lfpxs_step_dx, ex2_intro/ +qed-. + +(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *) +lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → + ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≛[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≛[h, o, T] L2. +#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … 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_lfpx_trans … H1 … H) -L + #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2 + #H2 elim (lfdeq_lfpxs_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/etc/referred/lfpxs_lfpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc new file mode 100644 index 000000000..9f2b0b6e1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lfpxs.etc @@ -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/i_static/tc_lfxs_tc_lfxs.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Main properties **********************************************************) + +(* Basic_2A1: uses: lpxs_trans *) +theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T). +/2 width=3 by tc_lfxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc new file mode 100644 index 000000000..aa13ac53a --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/lfpxs_lpxs.etc @@ -0,0 +1,36 @@ +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs_lex.ma". +include "basic_2/rt_transition/cpx_lfeq.ma". +include "basic_2/rt_computation/cpxs_lpx.ma". +include "basic_2/rt_computation/lpxs.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) + +(* Properties with unbound parallel rt-computation for local environments ***) + +lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=1 by tc_lfxs_lex/ qed. + +lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → + ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_lex_lfeq/ qed. + +(* Inversion lemmas with unbound parallel rt-computation for local envs *****) + +lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → + ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. +/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc new file mode 100644 index 000000000..5bb15a4f0 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/referred/predtysnstar_5.etc @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedTySnStar $h $T $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma new file mode 100644 index 000000000..a12748a9b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_4.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ➡*[ break term 46 h ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'PRedSnStar $h $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma deleted file mode 100644 index 095cc3e31..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predsnstar_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* 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 )" - non associative with precedence 45 - for @{ 'PRedSnStar $h $o $G $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma deleted file mode 100644 index 5bb15a4f0..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predtysnstar_5.ma +++ /dev/null @@ -1,19 +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 *) -(* *) -(**************************************************************************) - -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) - -notation "hvbox( ⦃ term 46 G, break term 46 L1 ⦄ ⊢ ⬈ * [ break term 46 h, break term 46 T ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'PRedTySnStar $h $T $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/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma deleted file mode 100644 index 0e1bee1d1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma +++ /dev/null @@ -1,56 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/predtysnstar_5.ma". -include "basic_2/i_static/tc_lfxs.ma". -include "basic_2/rt_transition/lfpx.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -definition lfpxs: ∀h. relation4 genv term lenv lenv ≝ - λh,G. tc_lfxs (cpx h G). - -interpretation - "unbound parallel rt-computation on referred entries (local environment)" - 'PRedTySnStar h T G L1 L2 = (lfpxs h G T L1 L2). - -(* Basic properties *********************************************************) - -(* Basic_2A1: was just: lpx_lpxs *) -lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=1 by inj/ qed. - -lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by tc_lfxs_step_dx/ qed. - -lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by tc_lfxs_step_sn/ qed. - -(* Basic inversion lemmas ***************************************************) - -(* Basic_2A1: uses: lpxs_inv_atom1 *) -lemma lfpxs_inv_atom1: ∀h,I,G,L2. ⦃G, ⋆⦄ ⊢ ⬈*[h, ⓪{I}] L2 → L2 = ⋆. -/2 width=3 by tc_lfxs_inv_atom_sn/ qed-. - -(* Basic_2A1: uses: lpxs_inv_atom2 *) -lemma lfpxs_inv_atom2: ∀h,I,G,L1. ⦃G, L1⦄ ⊢ ⬈*[h, ⓪{I}] ⋆ → L1 = ⋆. -/2 width=3 by tc_lfxs_inv_atom_dx/ qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lfpxs_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, V] L2. -/2 width=3 by tc_lfxs_fwd_pair_sn/ qed-. - -lemma lfpxs_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by tc_lfxs_fwd_flat_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma deleted file mode 100644 index 43febff41..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_aaa.ma +++ /dev/null @@ -1,25 +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/rt_transition/lfpx_aaa.ma". -include "basic_2/rt_computation/lfpxs.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with atomic arity assignment on terms *************************) - -(* Basic_2A1: uses: lpxs_aaa_conf *) -lemma lfpxs_aaa_conf: ∀h,G,T. Conf3 … (λL. aaa G L T) (lfpxs h G T). -#h #G #T @TC_Conf3 @lfpx_aaa_conf (**) (* auto fails *) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma deleted file mode 100644 index a5288e11a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma +++ /dev/null @@ -1,76 +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/rt_computation/cpxs_lfpx.ma". -include "basic_2/rt_computation/lfpxs_fqup.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with unbound context-sensitive rt-computation for terms *******) - -(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *) -lemma lfpxs_pair_refl: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → - ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2. -/2 width=1 by tc_lfxs_pair_refl/ qed. - -lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G). -#h #G @s_r_trans_CTC2 @lfpx_cpxs_trans (**) (* auto fails *) -qed-. - -(* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_CTC1 *) -lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G). -#h #G @s_r_to_s_rs_trans @s_r_trans_CTC2 -@s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *) -qed-. - -(* Advanced properties on unbound rt-computation for terms ******************) - -lemma cpxs_bind2: ∀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=3 by lfpxs_cpxs_trans, lfpxs_pair_refl, cpxs_bind/ qed. - -(* Advanced inversion lemmas on unbound rt-computation for terms ************) - -lemma cpxs_inv_abst1: ∀h,p,G,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 #p #G #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 (lfpxs_cpx_trans … HT02 (L.ⓛV1) ?) -/3 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro/ -qed-. - -lemma cpxs_inv_abbr1: ∀h,p,G,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 = true. -#h #p #G #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 (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) - /4 width=5 by lfpxs_pair_refl, cpxs_trans, cpxs_strap1, ex3_2_intro, or_introl/ - | #T2 #HT02 #HUT2 - lapply (lfpxs_cpx_trans … HT02 (L.ⓓV1) ?) -HT02 - /4 width=3 by lfpxs_pair_refl, cpxs_trans, ex3_intro, or_intror/ - ] -| #U1 #HTU1 #HU01 - elim (cpx_lifts_sn … HU02 (Ⓣ) … (L.ⓓV1) … HU01) - /4 width=3 by cpxs_strap1, drops_refl, drops_drop, ex3_intro, or_intror/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma deleted file mode 100644 index caeb2bf77..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_drops.ma +++ /dev/null @@ -1,34 +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/i_static/tc_lfxs_drops.ma". -include "basic_2/rt_transition/lfpx_drops.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with generic slicing for local environments *******************) - -(* Basic_2A1: uses: drop_lpxs_trans *) -lemma drops_lfpxs_trans: ∀h,G. tc_dedropable_sn (cpx h G). -/3 width=5 by drops_lfpx_trans, dedropable_sn_CTC/ qed-. - -(* Inversion lemmas with generic slicing for local environments *************) - -(* Basic_2A1: uses: lpxs_drop_conf *) -lemma lfpxs_drops_conf: ∀h,G. tc_dropable_sn (cpx h G). -/3 width=5 by lfpx_drops_conf, dropable_sn_CTC/ qed-. - -(* Basic_2A1: uses: lpxs_drop_trans_O1 *) -lemma lfpxs_drops_trans: ∀h,G. tc_dropable_dx (cpx h G). -/3 width=5 by lfpx_drops_trans, dropable_dx_CTC/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma deleted file mode 100644 index 35ed9931b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_ffdeq.ma +++ /dev/null @@ -1,30 +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/static/ffdeq.ma". -include "basic_2/rt_computation/lfpxs_lfdeq.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with degree-based equivalence on closures *********************) - -lemma ffdeq_lfpxs_trans: ∀h,o,G1,G2,L1,L0,T1,T2. ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L0, T2⦄ → - ∀L2. ⦃G2, L0⦄ ⊢⬈*[h, T2] L2 → - ∃∃L. ⦃G1, L1⦄ ⊢⬈*[h, T1] 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_lfpxs_trans … HL02 … HL10) -L0 #L0 #HL10 #HL02 -lapply (tdeq_lfpxs_trans … HT12 … HL10) -HL10 #HL10 -/3 width=3 by ffdeq_intro_dx, ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma deleted file mode 100644 index 1ca306ddb..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ /dev/null @@ -1,49 +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/i_static/tc_lfxs_fqup.ma". -include "basic_2/rt_computation/lfpxs.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Advanced properties ******************************************************) - -lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T). -/2 width=1 by tc_lfxs_refl/ qed. - -(* Advanced forward lemmas **************************************************) - -lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → - ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. -/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-. - -lemma lfpxs_fwd_bind_dx_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → - ⦃G, L1.ⓧ⦄ ⊢ ⬈*[h, T] L2.ⓧ. -/2 width=4 by tc_lfxs_fwd_bind_dx_void/ qed-. - -(* Advanced eliminators *****************************************************) - -(* Basic_2A1: uses: lpxs_ind *) -lemma lfpxs_ind_sn: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. -#h #G @tc_lfxs_ind_sn // (**) (* auto fails *) -qed-. - -(* Basic_2A1: uses: lpxs_ind_dx *) -lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 → - (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) → - ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1. -#h #G @tc_lfxs_ind_dx // (**) (* auto fails *) -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma deleted file mode 100644 index 27bf18d49..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma +++ /dev/null @@ -1,23 +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/i_static/tc_lfxs_length.ma". -include "basic_2/rt_computation/lfpxs.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Forward lemmas with length for local environments ************************) - -lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|. -/2 width=3 by tc_lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma deleted file mode 100644 index 2d6871c34..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma +++ /dev/null @@ -1,58 +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/rt_transition/lfpx_lfdeq.ma". -include "basic_2/rt_computation/lfpxs_fqup.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with degree-based equivalence on terms ************************) - -lemma lfpxs_tdeq_trans: ∀h,o,G. s_r_confluent1 … (cdeq h o) (lfpxs h G). -#h #o #G #L1 #T1 #T2 #HT12 #L2 #H @(lfpxs_ind_sn … H) -L2 -/3 width=6 by lfpxs_step_dx, lfpx_tdeq_conf/ -qed-. - -lemma tdeq_lfpxs_trans: ∀h,o,T1,T2. T1 ≛[h, o] T2 → - ∀G,L1,L2. ⦃G, L1⦄ ⊢⬈*[h, T2] L2 → ⦃G, L1⦄ ⊢⬈*[h, T1] L2. -/3 width=4 by lfpxs_tdeq_trans, tdeq_sym/ qed-. - -(* Properties with degree-based equivalence on referred entries *************) - -(* Basic_2A1: was: lleq_lpxs_trans *) -lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 → - ∀L1. L1 ≛[h, o, T] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≛[h, o, T] K2. -#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/ -#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2 -#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K -/3 width=3 by lfpxs_step_dx, ex2_intro/ -qed-. - -(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *) -lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≛[h, o, T] L2 → ⊥) → - ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≛[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≛[h, o, T] L2. -#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … 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_lfpx_trans … H1 … H) -L - #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2 - #H2 elim (lfdeq_lfpxs_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/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma deleted file mode 100644 index 9f2b0b6e1..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma +++ /dev/null @@ -1,24 +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/i_static/tc_lfxs_tc_lfxs.ma". -include "basic_2/rt_computation/lfpxs.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Main properties **********************************************************) - -(* Basic_2A1: uses: lpxs_trans *) -theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T). -/2 width=3 by tc_lfxs_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma deleted file mode 100644 index aa13ac53a..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ /dev/null @@ -1,36 +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/i_static/tc_lfxs_lex.ma". -include "basic_2/rt_transition/cpx_lfeq.ma". -include "basic_2/rt_computation/cpxs_lpx.ma". -include "basic_2/rt_computation/lpxs.ma". -include "basic_2/rt_computation/lfpxs.ma". - -(* UNBOUND PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ******) - -(* Properties with unbound parallel rt-computation for local environments ***) - -lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=1 by tc_lfxs_lex/ qed. - -lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → - ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by tc_lfxs_lex_lfeq/ qed. - -(* Inversion lemmas with unbound parallel rt-computation for local envs *****) - -lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. -/3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ 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" * ] }