From: Ferruccio Guidi Date: Wed, 25 Oct 2017 13:22:29 +0000 (+0000) Subject: - exclusion binder in local environments X-Git-Tag: make_still_working~425 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=747b42f3b9aac5487047f57742f1fcf05b56b57d - exclusion binder in local environments updated: cpm, cpr, lfpr, cpc - some refactoeing and minor corrections --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma deleted file mode 100644 index 156374e3f..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc.ma +++ /dev/null @@ -1,41 +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/pconv_5.ma". -include "basic_2/rt_transition/cpm.ma". - -(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) - -definition cpc: sh → relation4 genv lenv term term ≝ - λh,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 ∨ ⦃G, L⦄ ⊢ T2 ➡[h] T1. - -interpretation - "context-sensitive parallel r-conversion (term)" - 'PConv h G L T1 T2 = (cpc h G L T1 T2). - -(* Basic properties *********************************************************) - -lemma cpc_refl: ∀h,G,L. reflexive … (cpc h G L). -/2 width=1 by or_intror/ qed. - -lemma cpc_sym: ∀h,G,L. symmetric … (cpc h L G). -#h #G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma cpc_fwd_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[h] T & ⦃G, L⦄ ⊢ T2 ➡[h] T. -#h #G #L #T1 #T2 * /2 width=3 by ex2_intro/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.ma deleted file mode 100644 index 92ce08e18..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/conversion/cpc_cpc.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/conversion/cpc.ma". - -(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) - -(* Main properties **********************************************************) - -theorem cpc_conf: ∀h,G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌[h] T1 → ⦃G, L⦄ ⊢ T0 ⬌[h] T2 → - ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌[h] T & ⦃G, L⦄ ⊢ T2 ⬌[h] T. -/3 width=3 by cpc_sym, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/cpm_lsubr.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/cpm_lsubr.etc new file mode 100644 index 000000000..0bc981d0c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/cpm_lsubr.etc @@ -0,0 +1,7 @@ +(* Advanced properties ******************************************************) + +(* Basic_1: was by definition: pr2_free *) +(* Basic_2A1: includes: tpr_cpr *) +lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2. +#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) // +qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc.ma new file mode 100644 index 000000000..156374e3f --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc.ma @@ -0,0 +1,41 @@ +(**************************************************************************) +(* ___ *) +(* ||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/pconv_5.ma". +include "basic_2/rt_transition/cpm.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) + +definition cpc: sh → relation4 genv lenv term term ≝ + λh,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h] T2 ∨ ⦃G, L⦄ ⊢ T2 ➡[h] T1. + +interpretation + "context-sensitive parallel r-conversion (term)" + 'PConv h G L T1 T2 = (cpc h G L T1 T2). + +(* Basic properties *********************************************************) + +lemma cpc_refl: ∀h,G,L. reflexive … (cpc h G L). +/2 width=1 by or_intror/ qed. + +lemma cpc_sym: ∀h,G,L. symmetric … (cpc h L G). +#h #G #L #T1 #T2 * /2 width=1 by or_introl, or_intror/ +qed-. + +(* Basic forward lemmas *****************************************************) + +lemma cpc_fwd_cpr: ∀h,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ⬌[h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ➡[h] T & ⦃G, L⦄ ⊢ T2 ➡[h] T. +#h #G #L #T1 #T2 * /2 width=3 by ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma new file mode 100644 index 000000000..b5b9ac86c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_conversion/cpc_cpc.ma @@ -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/rt_conversion/cpc.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-CONVERSION FOR TERMS ************************) + +(* Main properties **********************************************************) + +theorem cpc_conf: ∀h,G,L,T0,T1,T2. ⦃G, L⦄ ⊢ T0 ⬌[h] T1 → ⦃G, L⦄ ⊢ T0 ⬌[h] T2 → + ∃∃T. ⦃G, L⦄ ⊢ T1 ⬌[h] T & ⦃G, L⦄ ⊢ T2 ⬌[h] T. +/3 width=3 by cpc_sym, ex2_intro/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma index 260cd45a4..95af51e0b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpg.ma @@ -106,7 +106,7 @@ lemma cpg_inv_atom1: ∀Rt,c,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[Rt, c, h] T2 /2 width=3 by cpg_inv_atom1_aux/ qed-. lemma cpg_inv_sort1: ∀Rt,c,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[Rt, c, h] T2 → - (T2 = ⋆s ∧ c = 𝟘𝟘) ∨ (T2 = ⋆(next h s) ∧ c = 𝟘𝟙). + ∨∨ T2 = ⋆s ∧ c = 𝟘𝟘 | T2 = ⋆(next h s) ∧ c = 𝟘𝟙. #Rt #c #h #G #L #T2 #s #H elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/ [ #s0 #H destruct /3 width=1 by or_intror, conj/ @@ -116,7 +116,7 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/ qed-. lemma cpg_inv_zero1: ∀Rt,c,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[Rt, c, h] T2 → - ∨∨ (T2 = #0 ∧ c = 𝟘𝟘) + ∨∨ T2 = #0 ∧ c = 𝟘𝟘 | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 & c = cV | ∃∃cV,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & @@ -130,8 +130,8 @@ elim (cpg_inv_atom1 … H) -H * /3 width=1 by or3_intro0, conj/ qed-. lemma cpg_inv_lref1: ∀Rt,c,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 → - (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨ - ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. + ∨∨ T2 = #(⫯i) ∧ c = 𝟘𝟘 + | ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. #Rt #c #h #G #L #T2 #i #H elim (cpg_inv_atom1 … H) -H * /3 width=1 by or_introl, conj/ [ #s #H destruct @@ -150,12 +150,11 @@ elim (cpg_inv_atom1 … H) -H * /2 width=1 by conj/ qed-. fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 → - ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → ( - ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 & - U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT) - ) ∨ - ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & - p = true & J = Abbr & c = cT+𝟙𝟘. + ∀p,J,V1,U1. U = ⓑ{p,J}V1.U1 → + ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{J}V1⦄ ⊢ U1 ⬈[Rt, cT, h] T2 & + U2 = ⓑ{p,J}V2.T2 & c = ((↓cV)∨cT) + | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ U1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & + p = true & J = Abbr & c = cT+𝟙𝟘. #Rt #c #h #G #L #U #U2 * -c -G -L -U -U2 [ #I #G #L #q #J #W #U1 #H destruct | #G #L #s #q #J #W #U1 #H destruct @@ -173,20 +172,18 @@ fact cpg_inv_bind1_aux: ∀Rt,c,h,G,L,U,U2. ⦃G, L⦄ ⊢ U ⬈[Rt, c, h] U2 ] qed-. -lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 → ( - ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & - U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT) - ) ∨ - ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & - p = true & I = Abbr & c = cT+𝟙𝟘. +lemma cpg_inv_bind1: ∀Rt,c,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[Rt, c, h] U2 → + ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & + U2 = ⓑ{p,I}V2.T2 & c = ((↓cV)∨cT) + | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & + p = true & I = Abbr & c = cT+𝟙𝟘. /2 width=3 by cpg_inv_bind1_aux/ qed-. -lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 → ( - ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & - U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT) - ) ∨ - ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & - p = true & c = cT+𝟙𝟘. +lemma cpg_inv_abbr1: ∀Rt,c,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ⬈[Rt, c, h] U2 → + ∨∨ ∃∃cV,cT,V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T2 & + U2 = ⓓ{p}V2.T2 & c = ((↓cV)∨cT) + | ∃∃cT,T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[Rt, cT, h] T & ⬆*[1] U2 ≡ T & + p = true & c = cT+𝟙𝟘. #Rt #c #h #p #G #L #V1 #T1 #U2 #H elim (cpg_inv_bind1 … H) -H * /3 width=8 by ex4_4_intro, ex4_2_intro, or_introl, or_intror/ qed-. @@ -267,7 +264,7 @@ lemma cpg_inv_cast1: ∀Rt,c,h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝV1.U1 ⬈[Rt, c, (* Advanced inversion lemmas ************************************************) lemma cpg_inv_zero1_pair: ∀Rt,c,h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[Rt, c, h] T2 → - ∨∨ (T2 = #0 ∧ c = 𝟘𝟘) + ∨∨ T2 = #0 ∧ c = 𝟘𝟘 | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & I = Abbr & c = cV | ∃∃cV,V2. ⦃G, K⦄ ⊢ V1 ⬈[Rt, cV, h] V2 & ⬆*[1] V2 ≡ T2 & @@ -277,8 +274,8 @@ lemma cpg_inv_zero1_pair: ∀Rt,c,h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[ qed-. lemma cpg_inv_lref1_bind: ∀Rt,c,h,I,G,K,T2,i. ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈[Rt, c, h] T2 → - (T2 = #(⫯i) ∧ c = 𝟘𝟘) ∨ - ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2. + ∨∨ T2 = #(⫯i) ∧ c = 𝟘𝟘 + | ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[Rt, c, h] T & ⬆*[1] T ≡ T2. #Rt #c #h #I #G #L #T2 #i #H elim (cpg_inv_lref1 … H) -H /2 width=1 by or_introl/ * #Z #Y #T #HT #HT2 #H destruct /3 width=3 by ex2_intro, or_intror/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma index c207e05c1..7af9a5730 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm.ma @@ -47,9 +47,9 @@ lemma cpm_ell: ∀n,h,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 → /3 width=5 by cpg_ell, ex2_intro, isrt_succ/ qed. -lemma cpm_lref: ∀n,h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → - ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ➡[n, h] U. -#n #h #I #G #K #V #T #U #i * +lemma cpm_lref: ∀n,h,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T → + ⬆*[1] T ≡ U → ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ➡[n, h] U. +#n #h #I #G #K #T #U #i * /3 width=5 by cpg_lref, ex2_intro/ qed. @@ -126,8 +126,8 @@ lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → L = K.ⓓV1 & J = LRef 0 | ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓛV1 & J = LRef 0 & n = ⫯k - | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & - L = K.ⓑ{I}V & J = LRef (⫯i). + | ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & + L = K.ⓘ{I} & J = LRef (⫯i). #n #h #J #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1 … H) -H * [ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or5_intro0, conj/ | #s #H1 #H2 #H3 destruct /4 width=3 by isrt_inv_01, or5_intro1, ex3_intro/ @@ -136,21 +136,21 @@ lemma cpm_inv_atom1: ∀n,h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[n, h] T2 → | #cV #K #V1 #V2 #HV12 #HVT2 #H1 #H2 #H3 destruct elim (isrt_inv_plus_SO_dx … Hc) -Hc // #k #Hc #H destruct /4 width=9 by or5_intro3, ex5_4_intro, ex2_intro/ -| #I #K #V1 #V2 #i #HV2 #HVT2 #H1 #H2 destruct - /4 width=9 by or5_intro4, ex4_5_intro, ex2_intro/ +| #I #K #V2 #i #HV2 #HVT2 #H1 #H2 destruct + /4 width=8 by or5_intro4, ex4_4_intro, ex2_intro/ ] qed-. lemma cpm_inv_sort1: ∀n,h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[n,h] T2 → - (T2 = ⋆s ∧ n = 0) ∨ - (T2 = ⋆(next h s) ∧ n = 1). + ∨∨ T2 = ⋆s ∧ n = 0 + | T2 = ⋆(next h s) ∧ n = 1. #n #h #G #L #T2 #s * #c #Hc #H elim (cpg_inv_sort1 … H) -H * #H1 #H2 destruct /4 width=1 by isrt_inv_01, isrt_inv_00, or_introl, or_intror, conj/ qed-. lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[n, h] T2 → - ∨∨ (T2 = #0 ∧ n = 0) + ∨∨ T2 = #0 ∧ n = 0 | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[n, h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 | ∃∃k,K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[k, h] V2 & ⬆*[1] V2 ≡ T2 & @@ -166,12 +166,12 @@ lemma cpm_inv_zero1: ∀n,h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[n, h] T2 → qed-. lemma cpm_inv_lref1: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ➡[n, h] T2 → - (T2 = #(⫯i) ∧ n = 0) ∨ - ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. + ∨∨ T2 = #(⫯i) ∧ n = 0 + | ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ➡[n, h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. #n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1 … H) -H * [ #H1 #H2 destruct /4 width=1 by isrt_inv_00, or_introl, conj/ -| #I #K #V1 #V2 #HV2 #HVT2 #H1 destruct - /4 width=7 by ex3_4_intro, ex2_intro, or_intror/ +| #I #K #V2 #HV2 #HVT2 #H destruct + /4 width=6 by ex3_3_intro, ex2_intro, or_intror/ ] qed-. @@ -181,12 +181,11 @@ lemma cpm_inv_gref1: ∀n,h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[n, h] T2 → T2 = qed-. (* Basic_2A1: includes: cpr_inv_bind1 *) -lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 & - U2 = ⓑ{p,I}V2.T2 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & - p = true & I = Abbr. +lemma cpm_inv_bind1: ∀n,h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ➡[n, h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ➡[n, h] T2 & + U2 = ⓑ{p,I}V2.T2 + | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & + p = true & I = Abbr. #n #h #p #I #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_bind1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct @@ -199,11 +198,10 @@ qed-. (* Basic_1: includes: pr0_gen_abbr pr2_gen_abbr *) (* Basic_2A1: includes: cpr_inv_abbr1 *) -lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T2 & - U2 = ⓓ{p}V2.T2 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & p = true. +lemma cpm_inv_abbr1: ∀n,h,p,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓓ{p}V1.T1 ➡[n, h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T2 & + U2 = ⓓ{p}V2.T2 + | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ➡[n, h] T & ⬆*[1] U2 ≡ T & p = true. #n #h #p #G #L #V1 #T1 #U2 * #c #Hc #H elim (cpg_inv_abbr1 … H) -H * [ #cV #cT #V2 #T2 #HV12 #HT12 #H1 #H2 destruct elim (isrt_inv_max … Hc) -Hc #nV #nT #HcV #HcT #H destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma index 790970db3..03e5a9440 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_drops.ma @@ -42,8 +42,8 @@ lemma cpm_inv_atom1_drops: ∀n,h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[n, h] T2 | ∃∃s. T2 = ⋆(next h s) & I = Sort s & n = 1 | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 & ⬆*[⫯i] V2 ≡ T2 & I = LRef i - | ∃∃k,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[k, h] V2 & - ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯k. + | ∃∃m,K,V,V2,i. ⬇*[i] L ≡ K.ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i & n = ⫯m. #n #h #I #G #L #T2 * #c #Hc #H elim (cpg_inv_atom1_drops … H) -H * [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc /3 width=1 by or4_intro0, conj/ @@ -59,10 +59,10 @@ qed-. lemma cpm_inv_lref1_drops: ∀n,h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[n, h] T2 → ∨∨ T2 = #i ∧ n = 0 - | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 & + | ∃∃K,V,V2. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[n, h] V2 & ⬆*[⫯i] V2 ≡ T2 - | ∃∃k,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[k, h] V2 & - ⬆*[⫯i] V2 ≡ T2 & n = ⫯k. + | ∃∃m,K,V,V2. ⬇*[i] L ≡ K. ⓛV & ⦃G, K⦄ ⊢ V ➡[m, h] V2 & + ⬆*[⫯i] V2 ≡ T2 & n = ⫯m. #n #h #G #L #T2 #i * #c #Hc #H elim (cpg_inv_lref1_drops … H) -H * [ #H1 #H2 destruct lapply (isrt_inv_00 … Hc) -Hc /3 width=1 by or3_intro0, conj/ @@ -78,24 +78,26 @@ qed-. (* Basic_1: includes: pr0_lift pr2_lift *) (* Basic_2A1: includes: cpr_lift *) -lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn (cpm n h G). +lemma cpm_lifts_sn: ∀n,h,G. d_liftable2_sn … lifts (cpm n h G). #n #h #G #K #T1 #T2 * #c #Hc #HT12 #b #f #L #HLK #U1 #HTU1 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1 /3 width=5 by ex2_intro/ qed-. -lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi (cpm n h G). -/3 width=9 by cpm_lifts_sn, d_liftable2_sn_bi/ qed-. +lemma cpm_lifts_bi: ∀n,h,G. d_liftable2_bi … lifts (cpm n h G). +#n #h #G #K #T1 #T2 * /3 width=11 by cpg_lifts_bi, ex2_intro/ +qed-. (* Inversion lemmas with generic slicing for local environments *************) (* Basic_1: includes: pr0_gen_lift pr2_gen_lift *) (* Basic_2A1: includes: cpr_inv_lift1 *) -lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn (cpm n h G). +lemma cpm_inv_lifts_sn: ∀n,h,G. d_deliftable2_sn … lifts (cpm n h G). #n #h #G #L #U1 #U2 * #c #Hc #HU12 #b #f #K #HLK #T1 #HTU1 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1 /3 width=5 by ex2_intro/ qed-. -lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi (cpm n h G). -/3 width=9 by cpm_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. +lemma cpm_inv_lifts_bi: ∀n,h,G. d_deliftable2_bi … lifts (cpm n h G). +#n #h #G #L #U1 #U2 * /3 width=11 by cpg_inv_lifts_bi, ex2_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma index ac03ed30c..4b246a283 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpm_lsubr.ma @@ -23,11 +23,3 @@ include "basic_2/rt_transition/cpm.ma". lemma lsubr_cpm_trans: ∀n,h,G. lsub_trans … (cpm n h G) lsubr. #n #h #G #L1 #T1 #T2 * /3 width=5 by lsubr_cpg_trans, ex2_intro/ qed-. - -(* Advanced properties ******************************************************) - -(* Basic_1: was by definition: pr2_free *) -(* Basic_2A1: includes: tpr_cpr *) -lemma tpm_cpm: ∀n,h,G,T1,T2. ⦃G, ⋆⦄ ⊢ T1 ➡[n, h] T2 → ∀L. ⦃G, L⦄ ⊢ T1 ➡[n, h] T2. -#n #h #G #T1 #T2 #HT12 #L lapply (lsubr_cpm_trans … HT12 L ?) // -qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma index 6bcfa173e..fd5163073 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr.ma @@ -38,13 +38,11 @@ lemma cpr_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ➡[h] T2 → ∨∨ T2 = ⓪{J} | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓓV1 & J = LRef 0 - | ∃∃I,K,V,T,i. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & - L = K.ⓑ{I}V & J = LRef (⫯i). + | ∃∃I,K,T,i. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & + L = K.ⓘ{I} & J = LRef (⫯i). #h #J #G #L #T2 #H elim (cpm_inv_atom1 … H) -H * -/3 width=9 by or3_intro0, or3_intro1, or3_intro2, ex4_5_intro, ex4_3_intro/ -[ #n #_ #_ #H destruct -| #n #K #V1 #V2 #_ #_ #_ #_ #H destruct -] +/3 width=8 by tri_lt, or3_intro0, or3_intro1, or3_intro2, ex4_4_intro, ex4_3_intro/ +#n #_ #_ #H destruct qed-. (* Basic_1: includes: pr0_gen_sort pr2_gen_sort *) @@ -53,19 +51,19 @@ lemma cpr_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ➡[h] T2 → T2 = ⋆s. qed-. lemma cpr_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ➡[h] T2 → - T2 = #0 ∨ - ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓓV1. + ∨∨ T2 = #0 + | ∃∃K,V1,V2. ⦃G, K⦄ ⊢ V1 ➡[h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓓV1. #h #G #L #T2 #H elim (cpm_inv_zero1 … H) -H * /3 width=6 by ex3_3_intro, or_introl, or_intror/ #n #K #V1 #V2 #_ #_ #_ #H destruct qed-. lemma cpr_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ➡[h] T2 → - T2 = #(⫯i) ∨ - ∃∃I,K,V,T. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & L = K.ⓑ{I}V. + ∨∨ T2 = #(⫯i) + | ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ➡[h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. #h #G #L #T2 #i #H elim (cpm_inv_lref1 … H) -H * -/3 width=7 by ex3_4_intro, or_introl, or_intror/ +/3 width=6 by ex3_3_intro, or_introl, or_intror/ qed-. lemma cpr_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[h] T2 → T2 = §l. @@ -73,10 +71,10 @@ lemma cpr_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ➡[h] T2 → T2 = §l. qed-. (* Basic_1: includes: pr0_gen_cast pr2_gen_cast *) -lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1. U1 ➡[h] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 & - U2 = ⓝV2.T2 - ) ∨ ⦃G, L⦄ ⊢ U1 ➡[h] U2. +lemma cpr_inv_cast1: ∀h,G,L,V1,U1,U2. ⦃G, L⦄ ⊢ ⓝ V1.U1 ➡[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 & ⦃G, L⦄ ⊢ U1 ➡[h] T2 & + U2 = ⓝV2.T2 + | ⦃G, L⦄ ⊢ U1 ➡[h] U2. #h #G #L #V1 #U1 #U2 #H elim (cpm_inv_cast1 … H) -H /2 width=1 by or_introl, or_intror/ * #n #_ #H destruct qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma index c7c287036..714ce2f45 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_drops.ma @@ -20,26 +20,26 @@ include "basic_2/rt_transition/cpm_drops.ma". (* Basic_2A1: includes: cpr_inv_atom1 *) lemma cpr_inv_atom1_drops: ∀h,I,G,L,T2. ⦃G, L⦄ ⊢ ⓪{I} ➡[h] T2 → - T2 = ⓪{I} ∨ - ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & - ⬆*[⫯i] V2 ≡ T2 & I = LRef i. + ∨∨ T2 = ⓪{I} + | ∃∃K,V,V2,i. ⬇*[i] L ≡ K.ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2 & I = LRef i. #h #I #G #L #T2 #H elim (cpm_inv_atom1_drops … H) -H * [ /2 width=1 by or_introl/ | #s #_ #_ #H destruct | /3 width=8 by ex4_4_intro, or_intror/ -| #k #K #V1 #V2 #i #_ #_ #_ #_ #H destruct +| #m #K #V1 #V2 #i #_ #_ #_ #_ #H destruct ] qed-. (* Basic_1: includes: pr0_gen_lref pr2_gen_lref *) (* Basic_2A1: includes: cpr_inv_lref1 *) lemma cpr_inv_lref1_drops: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #i ➡[h] T2 → - T2 = #i ∨ - ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & - ⬆*[⫯i] V2 ≡ T2. + ∨∨ T2 = #i + | ∃∃K,V,V2. ⬇*[i] L ≡ K. ⓓV & ⦃G, K⦄ ⊢ V ➡[h] V2 & + ⬆*[⫯i] V2 ≡ T2. #h #G #L #T2 #i #H elim (cpm_inv_lref1_drops … H) -H * [ /2 width=1 by or_introl/ | /3 width=6 by ex3_3_intro, or_intror/ -| #k #K #V1 #V2 #_ #_ #_ #H destruct +| #m #K #V1 #V2 #_ #_ #_ #H destruct ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma new file mode 100644 index 000000000..434efb137 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpr_ext.ma @@ -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/syntax/lenv_ext2.ma". +include "basic_2/rt_transition/cpm.ma". + +(* CONTEXT-SENSITIVE PARALLEL R-TRANSITION FOR BINDERS **********************) + +definition cpr_ext (h) (G): relation3 lenv bind bind ≝ + cext2 (cpm 0 h G). + +interpretation + "context-sensitive parallel r-transition (binder)" + 'PRed h G L I1 I2 = (cpr_ext h G L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma index 1517ab340..c0bb4856e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -113,22 +113,22 @@ lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[h] T2 → qed-. lemma cpx_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] T2 → - T2 = ⋆s ∨ T2 = ⋆(next h s). + ∨∨ T2 = ⋆s | T2 = ⋆(next h s). #h #G #L #T2 #s * #c #H elim (cpg_inv_sort1 … H) -H * /2 width=1 by or_introl, or_intror/ qed-. lemma cpx_inv_zero1: ∀h,G,L,T2. ⦃G, L⦄ ⊢ #0 ⬈[h] T2 → - T2 = #0 ∨ - ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2 & - L = K.ⓑ{I}V1. + ∨∨ T2 = #0 + | ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2 & + L = K.ⓑ{I}V1. #h #G #L #T2 * #c #H elim (cpg_inv_zero1 … H) -H * /4 width=7 by ex3_4_intro, ex_intro, or_introl, or_intror/ qed-. lemma cpx_inv_lref1: ∀h,G,L,T2,i. ⦃G, L⦄ ⊢ #⫯i ⬈[h] T2 → - T2 = #(⫯i) ∨ - ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. + ∨∨ T2 = #(⫯i) + | ∃∃I,K,T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2 & L = K.ⓘ{I}. #h #G #L #T2 #i * #c #H elim (cpg_inv_lref1 … H) -H * /4 width=6 by ex3_3_intro, ex_intro, or_introl, or_intror/ qed-. @@ -137,21 +137,19 @@ lemma cpx_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[h] T2 → T2 = §l. #h #G #L #T2 #l * #c #H elim (cpg_inv_gref1 … H) -H // qed-. -lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] U2 → ( - ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 & - U2 = ⓑ{p,I}V2.T2 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≡ T & - p = true & I = Abbr. +lemma cpx_inv_bind1: ∀h,p,I,G,L,V1,T1,U2. ⦃G, L⦄ ⊢ ⓑ{p,I}V1.T1 ⬈[h] U2 → + ∨∨ ∃∃V2,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 & ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 & + U2 = ⓑ{p,I}V2.T2 + | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≡ T & + p = true & I = Abbr. #h #p #I #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_bind1 … H) -H * /4 width=5 by ex4_intro, ex3_2_intro, ex_intro, or_introl, or_intror/ qed-. -lemma cpx_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 - ) ∨ - ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≡ T & p = true. +lemma cpx_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 + | ∃∃T. ⦃G, L.ⓓV1⦄ ⊢ T1 ⬈[h] T & ⬆*[1] U2 ≡ T & p = true. #h #p #G #L #V1 #T1 #U2 * #c #H elim (cpg_inv_abbr1 … H) -H * /4 width=5 by ex3_2_intro, ex3_intro, ex_intro, or_introl, or_intror/ qed-. @@ -188,15 +186,15 @@ qed-. (* Advanced inversion lemmas ************************************************) lemma cpx_inv_zero1_pair: ∀h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[h] T2 → - T2 = #0 ∨ - ∃∃V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2. + ∨∨ T2 = #0 + | ∃∃V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2. #h #I #G #L #V1 #T2 * #c #H elim (cpg_inv_zero1_pair … H) -H * /4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/ qed-. lemma cpx_inv_lref1_bind: ∀h,I,G,K,T2,i. ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈[h] T2 → - T2 = #(⫯i) ∨ - ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2. + ∨∨ T2 = #(⫯i) + | ∃∃T. ⦃G, K⦄ ⊢ #i ⬈[h] T & ⬆*[1] T ≡ T2. #h #I #G #L #T2 #i * #c #H elim (cpg_inv_lref1_bind … H) -H * /4 width=3 by ex2_intro, ex_intro, or_introl, or_intror/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma index cc8550d21..92ff748bd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/predsn_5.ma". include "basic_2/static/lfxs.ma". -include "basic_2/rt_transition/cpm.ma". +include "basic_2/rt_transition/cpr_ext.ma". (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) @@ -34,23 +34,23 @@ lemma lfpr_sort: ∀h,I,G,L1,L2,V1,V2,s. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2. /2 width=1 by lfxs_sort/ qed. -lemma lfpr_zero: ∀h,I,G,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → +lemma lfpr_pair: ∀h,I,G,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → ⦃G, L1⦄ ⊢ V1 ➡[h] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] L2.ⓑ{I}V2. -/2 width=1 by lfxs_zero/ qed. +/2 width=1 by lfxs_pair/ qed. -lemma lfpr_lref: ∀h,I,G,L1,L2,V1,V2,i. - ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #⫯i] L2.ⓑ{I}V2. +lemma lfpr_lref: ∀h,I1,I2,G,L1,L2,i. + ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ⦃G, L1.ⓘ{I1}⦄ ⊢ ➡[h, #⫯i] L2.ⓘ{I2}. /2 width=1 by lfxs_lref/ qed. -lemma lfpr_gref: ∀h,I,G,L1,L2,V1,V2,l. - ⦃G, L1⦄ ⊢ ➡[h, §l] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, §l] L2.ⓑ{I}V2. +lemma lfpr_gref: ∀h,I1,I2,G,L1,L2,l. + ⦃G, L1⦄ ⊢ ➡[h, §l] L2 → ⦃G, L1.ⓘ{I1}⦄ ⊢ ➡[h, §l] L2.ⓘ{I2}. /2 width=1 by lfxs_gref/ qed. -lemma lfpr_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1. - ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V1 → - ∀V2. ⦃G, L1⦄ ⊢ V ➡[h] V2 → - ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V2. -/2 width=2 by lfxs_pair_repl_dx/ qed-. +lemma lfpr_bind_repl_dx: ∀h,I,I1,G,L1,L2,T. + ⦃G, L1.ⓘ{I}⦄ ⊢ ➡[h, T] L2.ⓘ{I1} → + ∀I2. ⦃G, L1⦄ ⊢ I ➡[h] I2 → + ⦃G, L1.ⓘ{I}⦄ ⊢ ➡[h, T] L2.ⓘ{I2}. +/2 width=2 by lfxs_bind_repl_dx/ qed-. (* Basic inversion lemmas ***************************************************) @@ -63,47 +63,47 @@ lemma lfpr_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ➡[h, ⓪{I}] ⋆ → Y1 = /2 width=3 by lfxs_inv_atom_dx/ qed-. lemma lfpr_inv_sort: ∀h,G,Y1,Y2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_sort/ qed-. - +(* lemma lfpr_inv_zero: ∀h,G,Y1,Y2. ⦃G, Y1⦄ ⊢ ➡[h, #0] Y2 → (Y1 = ⋆ ∧ Y2 = ⋆) ∨ ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_zero/ qed-. - +*) lemma lfpr_inv_lref: ∀h,G,Y1,Y2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_lref/ qed-. lemma lfpr_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. + ∨∨ Y1 = ⋆ ∧ Y2 = ⋆ + | ∃∃I1,I2,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & + Y1 = L1.ⓘ{I1} & Y2 = L2.ⓘ{I2}. /2 width=1 by lfxs_inv_gref/ qed-. lemma lfpr_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → - ⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V. + ∧∧ ⦃G, L1⦄ ⊢ ➡[h, V] L2 & ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. lemma lfpr_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 → - ⦃G, L1⦄ ⊢ ➡[h, V] L2 ∧ ⦃G, L1⦄ ⊢ ➡[h, T] L2. + ∧∧ ⦃G, L1⦄ ⊢ ➡[h, V] L2 & ⦃G, L1⦄ ⊢ ➡[h, T] L2. /2 width=2 by lfxs_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lfpr_inv_sort_pair_sn: ∀h,I,G,Y2,L1,V1,s. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, ⋆s] Y2 → - ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. -/2 width=2 by lfxs_inv_sort_pair_sn/ qed-. +lemma lfpr_inv_sort_bind_sn: ∀h,I1,G,Y2,L1,s. ⦃G, L1.ⓘ{I1}⦄ ⊢ ➡[h, ⋆s] Y2 → + ∃∃I2,L2. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y2 = L2.ⓘ{I2}. +/2 width=2 by lfxs_inv_sort_bind_sn/ qed-. -lemma lfpr_inv_sort_pair_dx: ∀h,I,G,Y1,L2,V2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] L2.ⓑ{I}V2 → - ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. -/2 width=2 by lfxs_inv_sort_pair_dx/ qed-. +lemma lfpr_inv_sort_bind_dx: ∀h,I2,G,Y1,L2,s. ⦃G, Y1⦄ ⊢ ➡[h, ⋆s] L2.ⓘ{I2} → + ∃∃I1,L1. ⦃G, L1⦄ ⊢ ➡[h, ⋆s] L2 & Y1 = L1.ⓘ{I1}. +/2 width=2 by lfxs_inv_sort_bind_dx/ qed-. lemma lfpr_inv_zero_pair_sn: ∀h,I,G,Y2,L1,V1. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #0] Y2 → ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 & ⦃G, L1⦄ ⊢ V1 ➡[h] V2 & @@ -115,21 +115,21 @@ lemma lfpr_inv_zero_pair_dx: ∀h,I,G,Y1,L2,V2. ⦃G, Y1⦄ ⊢ ➡[h, #0] L2. Y1 = L1.ⓑ{I}V1. /2 width=1 by lfxs_inv_zero_pair_dx/ qed-. -lemma lfpr_inv_lref_pair_sn: ∀h,I,G,Y2,L1,V1,i. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, #⫯i] Y2 → - ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y2 = L2.ⓑ{I}V2. -/2 width=2 by lfxs_inv_lref_pair_sn/ qed-. +lemma lfpr_inv_lref_bind_sn: ∀h,I1,G,Y2,L1,i. ⦃G, L1.ⓘ{I1}⦄ ⊢ ➡[h, #⫯i] Y2 → + ∃∃I2,L2. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y2 = L2.ⓘ{I2}. +/2 width=2 by lfxs_inv_lref_bind_sn/ qed-. -lemma lfpr_inv_lref_pair_dx: ∀h,I,G,Y1,L2,V2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] L2.ⓑ{I}V2 → - ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y1 = L1.ⓑ{I}V1. -/2 width=2 by lfxs_inv_lref_pair_dx/ qed-. +lemma lfpr_inv_lref_bind_dx: ∀h,I2,G,Y1,L2,i. ⦃G, Y1⦄ ⊢ ➡[h, #⫯i] L2.ⓘ{I2} → + ∃∃I1,L1. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 & Y1 = L1.ⓘ{I1}. +/2 width=2 by lfxs_inv_lref_bind_dx/ qed-. -lemma lfpr_inv_gref_pair_sn: ∀h,I,G,Y2,L1,V1,l. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, §l] Y2 → - ∃∃L2,V2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y2 = L2.ⓑ{I}V2. -/2 width=2 by lfxs_inv_gref_pair_sn/ qed-. +lemma lfpr_inv_gref_bind_sn: ∀h,I1,G,Y2,L1,l. ⦃G, L1.ⓘ{I1}⦄ ⊢ ➡[h, §l] Y2 → + ∃∃I2,L2. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y2 = L2.ⓘ{I2}. +/2 width=2 by lfxs_inv_gref_bind_sn/ qed-. -lemma lfpr_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] L2.ⓑ{I}V2 → - ∃∃L1,V1. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y1 = L1.ⓑ{I}V1. -/2 width=2 by lfxs_inv_gref_pair_dx/ qed-. +lemma lfpr_inv_gref_bind_dx: ∀h,I2,G,Y1,L2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] L2.ⓘ{I2} → + ∃∃I1,L1. ⦃G, L1⦄ ⊢ ➡[h, §l] L2 & Y1 = L1.ⓘ{I1}. +/2 width=2 by lfxs_inv_gref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma index 7c630638c..4b531bf74 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma @@ -34,10 +34,10 @@ lemma lfpr_drops_conf: ∀h,G. dropable_sn (cpm 0 h G). lemma lfpr_drops_trans: ∀h,G. dropable_dx (cpm 0 h G). /2 width=5 by lfxs_dropable_dx/ qed-. -lemma lfpr_inv_lref_sn: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & ⦃G, K1⦄ ⊢ ➡[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h] V2. -/2 width=3 by lfxs_inv_lref_sn/ qed-. +lemma lfpr_inv_lref_pair_sn: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ∀I,K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 & ⦃G, K1⦄ ⊢ ➡[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h] V2. +/2 width=3 by lfxs_inv_lref_pair_sn/ qed-. -lemma lfpr_inv_lref_dx: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & ⦃G, K1⦄ ⊢ ➡[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h] V2. -/2 width=3 by lfxs_inv_lref_dx/ qed-. +lemma lfpr_inv_lref_pair_dx: ∀h,G,L1,L2,i. ⦃G, L1⦄ ⊢ ➡[h, #i] L2 → ∀I,K2,V2. ⬇*[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇*[i] L1 ≡ K1.ⓑ{I}V1 & ⦃G, K1⦄ ⊢ ➡[h, V1] K2 & ⦃G, K1⦄ ⊢ V1 ➡[h] V2. +/2 width=3 by lfxs_inv_lref_pair_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma index a0f5b490d..8de2443e0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma @@ -28,3 +28,15 @@ lemma lfpr_refl: ∀h,G,T. reflexive … (lfpr h G T). lemma lfpr_pair: ∀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 lfxs_pair/ qed. + +(* Advanced inversion lemmas ************************************************) + +lemma lfpr_inv_bind_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → + ∧∧ ⦃G, L1⦄ ⊢ ➡[h, V] L2 & ⦃G, L1.ⓧ⦄ ⊢ ➡[h, T] L2.ⓧ. +/2 width=3 by lfxs_inv_bind_void/ qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lfpr_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 lfxs_fwd_bind_dx_void/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma index 72c313796..79208e25f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma @@ -14,6 +14,7 @@ include "basic_2/s_transition/fquq.ma". include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_transition/cpm_lsubr.ma". include "basic_2/rt_transition/cpr.ma". include "basic_2/rt_transition/lfpr_fqup.ma". @@ -21,41 +22,45 @@ include "basic_2/rt_transition/lfpr_fqup.ma". (* Properties with supclosure ***********************************************) -lemma fqu_cpr_trans_dx: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → +lemma fqu_cpr_trans_dx: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ -#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U -/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +[ /5 width=5 by lsubr_cpm_trans, cpm_bind, lsubr_unit, fqu_clear, ex3_2_intro/ +| #I #G #L #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U + /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +] qed-. (* Basic_2A1: uses: fqu_lpr_trans *) -lemma fqu_cpr_trans_sn: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → +lemma fqu_cpr_trans_sn: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 /3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ -#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U -/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +[ /5 width=5 by lsubr_cpm_trans, cpm_bind, lsubr_unit, fqu_clear, ex3_2_intro/ +| #I #G #L #U #T #HUT #U2 #HU2 elim (cpm_lifts_sn … HU2 (Ⓣ) … HUT) -U + /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +] qed-. (* Properties with optional supclosure **************************************) -lemma fquq_cpr_trans_dx: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → +lemma fquq_cpr_trans_dx: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [ #HT12 #U2 #HTU2 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] qed-. (* Basic_2A1: uses: fquq_lpr_trans *) -lemma fquq_cpr_trans_sn: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → +lemma fquq_cpr_trans_sn: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H + ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [ #HT12 #U2 #HTU2 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ | * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma index 3c204dcd1..b79a65745 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_frees.ma @@ -14,6 +14,7 @@ include "basic_2/rt_transition/lfpx_frees.ma". include "basic_2/rt_transition/cpm_cpx.ma". +include "basic_2/rt_transition/cpr_ext.ma". (* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) @@ -22,5 +23,5 @@ include "basic_2/rt_transition/cpm_cpx.ma". lemma cpm_frees_conf: ∀n,h,G. R_frees_confluent (cpm n h G). /3 width=6 by cpm_fwd_cpx, cpx_frees_conf/ qed-. -lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpm 0 h G) cfull. -/4 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co/ qed-. +lemma lfpr_frees_conf: ∀h,G. lexs_frees_confluent (cpr_ext h G) cfull. +/5 width=9 by cpm_fwd_cpx, lfpx_frees_conf, lexs_co, cext2_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma index 7c6c22237..9f1831141 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpr.ma @@ -40,10 +40,10 @@ fact cpr_conf_lfpr_atom_delta: ∀L1. ⦃G, L0⦄ ⊢ ➡[h, #i] L1 → ∀L2. ⦃G, L0⦄ ⊢ ➡[h, #i] L2 → ∃∃T. ⦃G, L1⦄ ⊢ #i ➡[h] T & ⦃G, L2⦄ ⊢ T2 ➡[h] T. #h #G #L0 #i #IH #K0 #V0 #HLK0 #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 -elim (lfpr_inv_lref_sn … HL01 … HLK0) -HL01 #K1 #V1 #HLK1 #HK01 #HV01 -elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ +elim (lfpr_inv_lref_pair_sn … HL01 … HLK0) -HL01 #K1 #V1 #HLK1 #HK01 #HV01 +elim (lfpr_inv_lref_pair_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ lapply (drops_isuni_fwd_drop2 … HLK2) // -W2 #HLK2 -lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 +lapply (fqup_lref (Ⓣ) … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 /3 width=6 by cpm_delta_drops, ex2_intro/ @@ -66,11 +66,11 @@ fact cpr_conf_lfpr_delta_delta: #h #G #L0 #i #IH #K0 #V0 #HLK0 #V1 #HV01 #T1 #HVT1 #KX #VX #H #V2 #HV02 #T2 #HVT2 #L1 #HL01 #L2 #HL02 lapply (drops_mono … H … HLK0) -H #H destruct -elim (lfpr_inv_lref_sn … HL01 … HLK0) -HL01 #K1 #W1 #HLK1 #HK01 #_ +elim (lfpr_inv_lref_pair_sn … HL01 … HLK0) -HL01 #K1 #W1 #HLK1 #HK01 #_ lapply (drops_isuni_fwd_drop2 … HLK1) -W1 // #HLK1 -elim (lfpr_inv_lref_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ +elim (lfpr_inv_lref_pair_sn … HL02 … HLK0) -HL02 #K2 #W2 #HLK2 #HK02 #_ lapply (drops_isuni_fwd_drop2 … HLK2) -W2 // #HLK2 -lapply (fqup_lref … G … HLK0) -HLK0 #HLK0 +lapply (fqup_lref (Ⓣ) … G … HLK0) -HLK0 #HLK0 elim (IH … HLK0 … HV01 … HV02 … HK01 … HK02) -L0 -K0 -V0 #V #HV1 #HV2 elim (cpm_lifts_sn … HV1 … HLK1 … HVT1) -K1 -V1 #T #HVT #HT1 elim (cpm_lifts_sn … HV2 … HLK2 … HVT2) -K2 -V2 #X #HX #HT2 @@ -95,7 +95,7 @@ elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) // elim (IH … HT01 … HT02 (L1.ⓑ{I}V1) … (L2.ⓑ{I}V2)) -IH -/3 width=5 by lfpr_pair_repl_dx, cpm_bind, ex2_intro/ +/3 width=5 by lfpr_bind_repl_dx, cpm_bind, ext2_pair, ex2_intro/ qed-. fact cpr_conf_lfpr_bind_zeta: @@ -113,7 +113,7 @@ fact cpr_conf_lfpr_bind_zeta: #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0 -elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -T0 #T #HT1 #HT2 +elim (IH … HT01 … HT02 (L1.ⓓV1) … (L2.ⓓV1)) -IH -HT01 -HT02 /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -T0 #T #HT1 #HT2 elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=3 by drops_refl, drops_drop, cpm_zeta, ex2_intro/ qed-. @@ -133,7 +133,7 @@ fact cpr_conf_lfpr_zeta_zeta: #T2 #HT02 #X2 #HXT2 #L1 #HL01 #L2 #HL02 elim (lfpr_inv_bind … HL01) -HL01 #H1V0 #H1T0 elim (lfpr_inv_bind … HL02) -HL02 #H2V0 #H2T0 -elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /2 width=4 by lfpr_pair_repl_dx/ -L0 -T0 #T #HT1 #HT2 +elim (IH … HT01 … HT02 (L1.ⓓV0) … (L2.ⓓV0)) -IH -HT01 -HT02 /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -T0 #T #HT1 #HT2 elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -T1 /3 width=2 by drops_refl, drops_drop/ #T1 #HT1 #HXT1 elim (cpm_inv_lifts_sn … HT2 … L2 … HXT2) -T2 /3 width=2 by drops_refl, drops_drop/ #T2 #HT2 #HXT2 lapply (lifts_inj … HT2 … HT1) -T #H destruct /2 width=3 by ex2_intro/ @@ -212,7 +212,7 @@ elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 lapply (lsubr_cpm_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ (**) (* full auto not tried *) /4 width=5 by cpm_bind, cpr_flat, cpm_beta, ex2_intro/ qed-. @@ -240,10 +240,10 @@ elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_re elim (cpm_inv_abbr1 … H) -H * [ #W1 #T1 #HW01 #HT01 #H destruct elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/ - elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 + elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -W0 -T0 /4 width=7 by cpm_bind, cpr_flat, cpm_theta, ex2_intro/ | #T1 #HT01 #HXT1 #H destruct - elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 + elim (IH … HT01 … HT02 (L1.ⓓW2) … (L2.ⓓW2)) /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 elim (cpm_inv_lifts_sn … HT1 … L1 … HXT1) -HXT1 /4 width=9 by cpr_flat, cpm_zeta, drops_refl, drops_drop, lifts_flat, ex2_intro/ ] @@ -268,7 +268,7 @@ elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1/ #W #HW1 #HW2 -elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 +elim (IH … HT01 … HT02 (L1.ⓛW1) … (L2.ⓛW2)) /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -W0 -T0 #T #HT1 #HT2 lapply (lsubr_cpm_trans … HT1 (L1.ⓓⓝW1.V1) ?) -HT1 /2 width=1 by lsubr_beta/ lapply (lsubr_cpm_trans … HT2 (L2.ⓓⓝW2.V2) ?) -HT2 /2 width=1 by lsubr_beta/ /4 width=5 by cpm_bind, cpr_flat, ex2_intro/ (**) (* full auto not tried *) @@ -296,7 +296,7 @@ elim (lfpr_inv_flat … HL02) -HL02 #H2V0 #HL02 elim (lfpr_inv_bind … HL02) -HL02 #H2W0 #H2T0 elim (IH … HV01 … HV02 … H1V0 … H2V0) -HV01 -HV02 /2 width=1 by/ #V #HV1 #HV2 elim (IH … HW01 … HW02 … H1W0 … H2W0) /2 width=1 by/ -elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /2 width=4 by lfpr_pair_repl_dx/ -L0 -V0 -W0 -T0 +elim (IH … HT01 … HT02 (L1.ⓓW1) … (L2.ⓓW2)) /3 width=4 by lfpr_bind_repl_dx, ext2_pair/ -L0 -V0 -W0 -T0 elim (cpm_lifts_sn … HV1 … (L1.ⓓW1) … HVU1) -HVU1 /3 width=2 by drops_refl, drops_drop/ #U #HVU elim (cpm_lifts_sn … HV2 … (L2.ⓓW2) … HVU2) -HVU2 /3 width=2 by drops_refl, drops_drop/ #X #HX lapply (lifts_mono … HX … HVU) -HX #H destruct @@ -304,7 +304,7 @@ lapply (lifts_mono … HX … HVU) -HX #H destruct qed-. theorem cpr_conf_lfpr: ∀h,G. R_confluent2_lfxs (cpm 0 h G) (cpm 0 h G) (cpm 0 h G) (cpm 0 h G). -#h #G #L0 #T0 @(fqup_wf_ind_eq … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] +#h #G #L0 #T0 @(fqup_wf_ind_eq (Ⓣ) … G L0 T0) -G -L0 -T0 #G #L #T #IH #G0 #L0 * [| * ] [ #I0 #HG #HL #HT #T1 #H1 #T2 #H2 #L1 #HL01 #L2 #HL02 destruct elim (cpr_inv_atom1_drops … H1) -H1 elim (cpr_inv_atom1_drops … H2) -H2 @@ -381,3 +381,17 @@ qed-. theorem lfpr_conf: ∀h,G,T. confluent … (lfpr h G T). /3 width=6 by cpr_conf_lfpr, lfpr_frees_conf, lfxs_conf/ qed-. + +theorem lfpr_bind: ∀h,G,L1,L2,V1. ⦃G, L1⦄ ⊢ ➡[h, V1] L2 → + ∀I,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡[h, T] L2.ⓑ{I}V2 → + ∀p. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V1.T] L2. +/2 width=2 by lfxs_bind/ qed. + +theorem lfpr_flat: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ➡[h, V] L2 → + ∀I,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2. +/2 width=1 by lfxs_flat/ qed. + +theorem lfpr_bind_void: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ➡[h, V] L2 → + ∀T. ⦃G, L1.ⓧ⦄ ⊢ ➡[h, T] L2.ⓧ → + ∀p,I. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2. +/2 width=1 by lfxs_bind_void/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index ac9ac42aa..537bb8bc8 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -88,11 +88,11 @@ lemma lfpx_inv_gref: ∀h,G,Y1,Y2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] Y2 → /2 width=1 by lfxs_inv_gref/ qed-. lemma lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → - ⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V. + ∧∧ ⦃G, L1⦄ ⊢ ⬈[h, V] L2 & ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. lemma lfpx_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 → - ⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1⦄ ⊢ ⬈[h, T] L2. + ∧∧ ⦃G, L1⦄ ⊢ ⬈[h, V] L2 & ⦃G, L1⦄ ⊢ ⬈[h, T] L2. /2 width=2 by lfxs_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma new file mode 100644 index 000000000..bf7dda13c --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_cpx.ma @@ -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/rt_transition/cpx_lfxs.ma". +include "basic_2/rt_transition/lfpx.ma". + +(* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) + +(* Advanced properties ******************************************************) + +lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G). +/2 width=5 by cpx_lfxs_conf/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma index 608907d5c..1ad389cd4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma @@ -31,7 +31,7 @@ lemma lfpx_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → (* Advanced inversion lemmas ************************************************) lemma lfpx_inv_bind_void: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → - ⦃G, L1⦄ ⊢ ⬈[h, V] L2 ∧ ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ. + ∧∧ ⦃G, L1⦄ ⊢ ⬈[h, V] L2 & ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ. /2 width=3 by lfxs_inv_bind_void/ qed-. (* Advanced forward lemmas **************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma index bf7dda13c..c63d7120e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfpx.ma @@ -12,12 +12,23 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/cpx_lfxs.ma". +include "basic_2/static/lfxs_lfxs.ma". include "basic_2/rt_transition/lfpx.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) -(* Advanced properties ******************************************************) +(* Main properties **********************************************************) -lemma lfpx_cpx_conf: ∀h,G. s_r_confluent1 … (cpx h G) (lfpx h G). -/2 width=5 by cpx_lfxs_conf/ qed-. +theorem lfpx_bind: ∀h,G,L1,L2,V1. ⦃G, L1⦄ ⊢ ⬈[h, V1] L2 → + ∀I,V2,T. ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V2 → + ∀p. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V1.T] L2. +/2 width=2 by lfxs_bind/ qed. + +theorem lfpx_flat: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → + ∀I,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2. +/2 width=1 by lfxs_flat/ qed. + +theorem lfpx_bind_void: ∀h,G,L1,L2,V. ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → + ∀T. ⦃G, L1.ⓧ⦄ ⊢ ⬈[h, T] L2.ⓧ → + ∀p,I. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2. +/2 width=1 by lfxs_bind_void/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 0fd7f15f7..20aead46a 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 @@ -63,15 +63,15 @@ table { } ] *) -(* class "blue" - [ { "conversion" * } { + [ { "rt-conversion" * } { [ { "context-sensitive r-conversion" * } { [ "cpc ( ⦃?,?⦄ ⊢ ? ⬌[?] ? )" "cpc_cpc" * ] } ] } ] +(* class "sky" [ { "rt-computation" * } { (* @@ -132,16 +132,17 @@ table { [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] +*) [ { "t-bound context-sensitive rt-transition" * } { [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ "cpr_ext ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" * ] [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] } ] -*) [ { "uncounted context-sensitive rt-transition" * } { [ "cnx ( ⦃?,?⦄ ⊢ ⬈[?,?] 𝐍⦃?⦄ )" "cnx_simple" + "cnx_drops" + "cnx_cnx" * ] - [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_lfpx" * ] + [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_lfdeq" + "lfpx_aaa" + "lfpx_cpx" + "lfpx_lfpx" * ] [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] } @@ -245,7 +246,7 @@ table { } ] [ { "degree-based equivalence" * } { - [ "tdeq_ext ( ? ≡[?,?] ? )" * ] + [ "tdeq_ext ( ? ≡[?,?] ? ) ( ? ⊢ ? ≡[?,?] ? )" * ] [ "tdeq ( ? ≡[?,?] ? )" "tdeq_tdeq" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 909355c60..1661bc1f1 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -6,5 +6,5 @@ basic_2/s_computation basic_2/static basic_2/i_static basic_2/rt_transition -basic_2/conversion +basic_2/rt_conversion apps_2/examples/ex_cpr_omega.ma