From: Ferruccio Guidi Date: Mon, 23 Oct 2017 17:15:29 +0000 (+0000) Subject: - exclusion binder in local environments: X-Git-Tag: make_still_working~428 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=21827c7db90ddb4fd30adec6becd94e201898f9c - exclusion binder in local environments: cpg, cpx, lfpx updated - notation for lazyeq: fixes and additions --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma deleted file mode 100644 index 1ffdc2b10..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.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( L1 ≡ [ break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'LazyEq $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma index c0b3b0bce..2a5cff3b3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )" +notation "hvbox( L ⊢ break term 46 T1 ≡ [ break term 46 h , break term 46 o ] break term 46 T2 )" non associative with precedence 45 - for @{ 'LazyEq $h $o $T $L1 $L2 }. + for @{ 'LazyEq $h $o $L $T1 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.ma deleted file mode 100644 index b4b796901..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_8.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 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" - non associative with precedence 45 - for @{ 'LazyEq $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma new file mode 100644 index 000000000..24b7250e5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.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( L1 ≡ [ break term 46 f ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEqSn $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.ma new file mode 100644 index 000000000..9f361b254 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_5.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( L1 ≡ [ break term 46 h , break term 46 o , break term 46 T ] break term 46 L2 )" + non associative with precedence 45 + for @{ 'LazyEqSn $h $o $T $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.ma new file mode 100644 index 000000000..7c9fbae7d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_8.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 G1, break term 46 L1, break term 46 T1 ⦄ ≡ [ break term 46 h , break term 46 o ] ⦃ break term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'LazyEqSn $h $o $G1 $L1 $T1 $G2 $L2 $T2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma index 21a642e5a..4289cde87 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cnx_drops.ma @@ -25,6 +25,11 @@ lemma cnx_lref_atom: ∀h,o,G,L,i. ⬇*[i] L ≡ ⋆ → ⦃G, L⦄ ⊢ ⬈[h, o #I #K #V1 #V2 #HLK lapply (drops_mono … Hi … HLK) -L #H destruct qed. +lemma cnx_lref_unit: ∀h,o,I,G,L,K,i. ⬇*[i] L ≡ K.ⓤ{I} → ⦃G, L⦄ ⊢ ⬈[h, o] 𝐍⦃#i⦄. +#h #o #I #G #L #K #i #HLK #X #H elim (cpx_inv_lref1_drops … H) -H // * +#Z #Y #V1 #V2 #HLY lapply (drops_mono … HLK … HLY) -L #H destruct +qed. + (* Basic_2A1: includes: cnx_lift *) lemma cnx_lifts: ∀h,o,G. d_liftable1 … (cnx h o G). #h #o #G #K #T #HT #b #f #L #HLK #U #HTU #U0 #H 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 0241664db..1517ab340 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx.ma @@ -36,9 +36,9 @@ lemma cpx_delta: ∀h,I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → /3 width=4 by cpg_delta, cpg_ell, ex_intro/ qed. -lemma cpx_lref: ∀h,I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → - ⬆*[1] T ≡ U → ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[h] U. -#h #I #G #K #V #T #U #i * +lemma cpx_lref: ∀h,I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → + ⬆*[1] T ≡ U → ⦃G, K.ⓘ{I}⦄ ⊢ #⫯i ⬈[h] U. +#h #I #G #K #T #U #i * /3 width=4 by cpg_lref, ex_intro/ qed. @@ -106,10 +106,10 @@ lemma cpx_inv_atom1: ∀h,J,G,L,T2. ⦃G, L⦄ ⊢ ⓪{J} ⬈[h] T2 → | ∃∃s. T2 = ⋆(next h s) & J = Sort s | ∃∃I,K,V1,V2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 & ⬆*[1] V2 ≡ T2 & L = K.ⓑ{I}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 * #c #H elim (cpg_inv_atom1 … H) -H * -/4 width=9 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_5_intro, ex4_4_intro, ex2_intro, ex_intro/ +/4 width=8 by or4_intro0, or4_intro1, or4_intro2, or4_intro3, ex4_4_intro, ex2_intro, ex_intro/ qed-. lemma cpx_inv_sort1: ∀h,G,L,T2,s. ⦃G, L⦄ ⊢ ⋆s ⬈[h] T2 → @@ -128,9 +128,9 @@ qed-. lemma cpx_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. + ∃∃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=7 by ex3_4_intro, ex_intro, or_introl, or_intror/ +/4 width=6 by ex3_3_intro, ex_intro, or_introl, or_intror/ qed-. lemma cpx_inv_gref1: ∀h,G,L,T2,l. ⦃G, L⦄ ⊢ §l ⬈[h] T2 → T2 = §l. @@ -194,10 +194,10 @@ lemma cpx_inv_zero1_pair: ∀h,I,G,K,V1,T2. ⦃G, K.ⓑ{I}V1⦄ ⊢ #0 ⬈[h] T2 /4 width=3 by ex2_intro, ex_intro, or_intror, or_introl/ qed-. -lemma cpx_inv_lref1_pair: ∀h,I,G,K,V,T2,i. ⦃G, K.ⓑ{I}V⦄ ⊢ #⫯i ⬈[h] T2 → +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. -#h #I #G #L #V #T2 #i * #c #H elim (cpg_inv_lref1_pair … H) -H * +#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-. @@ -238,8 +238,8 @@ lemma cpx_ind: ∀h. ∀R:relation4 genv lenv term term. (∀G,L,s. R G L (⋆s) (⋆(next h s))) → (∀I,G,K,V1,V2,W2. ⦃G, K⦄ ⊢ V1 ⬈[h] V2 → R G K V1 V2 → ⬆*[1] V2 ≡ W2 → R G (K.ⓑ{I}V1) (#0) W2 - ) → (∀I,G,K,V,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T → - ⬆*[1] T ≡ U → R G (K.ⓑ{I}V) (#⫯i) (U) + ) → (∀I,G,K,T,U,i. ⦃G, K⦄ ⊢ #i ⬈[h] T → R G K (#i) T → + ⬆*[1] T ≡ U → R G (K.ⓘ{I}) (#⫯i) (U) ) → (∀p,I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L.ⓑ{I}V1⦄ ⊢ T1 ⬈[h] T2 → R G L V1 V2 → R G (L.ⓑ{I}V1) T1 T2 → R G L (ⓑ{p,I}V1.T1) (ⓑ{p,I}V2.T2) ) → (∀I,G,L,V1,V2,T1,T2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma index 0d7a97a69..0c319c2ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_drops.ma @@ -51,23 +51,25 @@ qed-. (* Properties with generic slicing for local environments *******************) (* Basic_2A1: includes: cpx_lift *) -lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn (cpx h G). +lemma cpx_lifts_sn: ∀h,G. d_liftable2_sn … lifts (cpx h G). #h #G #K #T1 #T2 * #cT #HT12 #b #f #L #HLK #U1 #HTU1 elim (cpg_lifts_sn … HT12 … HLK … HTU1) -K -T1 /3 width=4 by ex2_intro, ex_intro/ qed-. -lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi (cpx h G). -/3 width=9 by cpx_lifts_sn, d_liftable2_sn_bi/ qed-. +lemma cpx_lifts_bi: ∀h,G. d_liftable2_bi … lifts (cpx h G). +#h #G #K #T1 #T2 * /3 width=10 by cpg_lifts_bi, ex_intro/ +qed-. (* Inversion lemmas with generic slicing for local environments *************) (* Basic_2A1: includes: cpx_inv_lift1 *) -lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn (cpx h G). +lemma cpx_inv_lifts_sn: ∀h,G. d_deliftable2_sn … lifts (cpx h G). #h #G #L #U1 #U2 * #cU #HU12 #b #f #K #HLK #T1 #HTU1 elim (cpg_inv_lifts_sn … HU12 … HLK … HTU1) -L -U1 /3 width=4 by ex2_intro, ex_intro/ qed-. -lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi (cpx h G). -/3 width=9 by cpx_inv_lifts_sn, d_deliftable2_sn_bi/ qed-. +lemma cpx_inv_lifts_bi: ∀h,G. d_deliftable2_bi …lifts (cpx h G). +#h #G #L #U1 #U2 * /3 width=10 by cpg_inv_lifts_bi, ex_intro/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_ext.ma new file mode 100644 index 000000000..e250ab490 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_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/cpx.ma". + +(* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR BINDERS ***********) + +definition cpx_ext (h) (G): relation3 lenv bind bind ≝ + cext2 (cpx h G). + +interpretation + "uncounted context-sensitive parallel rt-transition (binder)" + 'PRedTy h G L I1 I2 = (cpx_ext h G L I1 I2). diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index 453d2b5e1..147114a11 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -17,36 +17,38 @@ include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/s_computation/fqus_fqup.ma". include "basic_2/rt_transition/cpx_drops.ma". +include "basic_2/rt_transition/cpx_lsubr.ma". (* Properties on supclosure *************************************************) -lemma fqu_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → +lemma fqu_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=3 by fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, cpx_pair_sn, cpx_bind, cpx_flat, ex2_intro/ + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=3 by cpx_pair_sn, cpx_bind, cpx_flat, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex2_intro/ [ #I #G #L2 #V2 #X2 #HVX2 elim (lifts_total X2 (𝐔❴1❵)) /3 width=3 by fqu_drop, cpx_delta, ex2_intro/ -| #I #G #L2 #V #T2 #X2 #HTX2 #U2 #HTU2 - elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓑ{I}V) … HTX2) +| /5 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit, fqu_clear, ex2_intro/ +| #I #G #L2 #T2 #X2 #HTX2 #U2 #HTU2 + elim (cpx_lifts_sn … HTU2 (Ⓣ) … (L2.ⓘ{I}) … HTX2) /3 width=3 by fqu_drop, drops_refl, drops_drop, ex2_intro/ ] qed-. -lemma fquq_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → +lemma fquq_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H [ #HT12 #U2 #HTU2 elim (fqu_cpx_trans … HT12 … HTU2) /3 width=3 by fqu_fquq, ex2_intro/ | * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. -lemma fqup_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → +lemma fqup_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 [ #G2 #L2 #T2 #H12 #U2 #HTU2 elim (fqu_cpx_trans … H12 … HTU2) -T2 /3 width=3 by fqu_fqup, ex2_intro/ | #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #U2 #HTU2 @@ -55,19 +57,19 @@ lemma fqup_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T ] qed-. -lemma fqus_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → +lemma fqus_cpx_trans: ∀h,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. +#h #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim (fqus_inv_fqup … H) -H [ #HT12 #U2 #HTU2 elim (fqup_cpx_trans … HT12 … HTU2) /3 width=3 by fqup_fqus, ex2_intro/ | * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. -lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → +lemma fqu_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐[b] ⦃G2, L2, U2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 [ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵) #U2 #HVU2 @(ex3_intro … U2) [1,3: /3 width=7 by cpx_delta, fqu_drop/ @@ -82,30 +84,34 @@ lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, [1,3: /2 width=4 by fqu_bind_dx, cpx_bind/ | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] +| #p #I #G #L #V #T1 #Hb #T2 #HT12 #H0 @(ex3_intro … (ⓑ{p,I}V.T2)) + [1,3: /4 width=4 by lsubr_cpx_trans, cpx_bind, lsubr_unit, fqu_clear/ + | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] | #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ{I}V.T2)) [1,3: /2 width=4 by fqu_flat_dx, cpx_flat/ | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] -| #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0 - elim (cpx_lifts_sn … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 +| #I #G #L #T1 #U1 #HTU1 #T2 #HT12 #H0 + elim (cpx_lifts_sn … HT12 (Ⓣ) … (L.ⓘ{I}) … HTU1) -HT12 /4 width=6 by fqu_drop, drops_refl, drops_drop, tdeq_inv_lifts_bi, ex3_intro/ ] qed-. -lemma fquq_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → +lemma fquq_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮[b] ⦃G2, L2, U2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 [ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. -lemma fqup_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → +lemma fqup_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+[b] ⦃G2, L2, U2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 [ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 @@ -114,10 +120,10 @@ lemma fqup_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G ] qed-. -lemma fqus_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → +lemma fqus_cpx_trans_ntdeq: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐*[b] ⦃G2, L2, U2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 [ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ 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 172f88ed5..ac9ac42aa 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -14,7 +14,7 @@ include "basic_2/notation/relations/predtysn_5.ma". include "basic_2/static/lfxs.ma". -include "basic_2/rt_transition/cpx.ma". +include "basic_2/rt_transition/cpx_ext.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) @@ -30,27 +30,27 @@ interpretation lemma lfpx_atom: ∀h,I,G. ⦃G, ⋆⦄ ⊢ ⬈[h, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. -lemma lfpx_sort: ∀h,I,G,L1,L2,V1,V2,s. - ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, ⋆s] L2.ⓑ{I}V2. +lemma lfpx_sort: ∀h,I1,I2,G,L1,L2,s. + ⦃G, L1⦄ ⊢ ⬈[h, ⋆s] L2 → ⦃G, L1.ⓘ{I1}⦄ ⊢ ⬈[h, ⋆s] L2.ⓘ{I2}. /2 width=1 by lfxs_sort/ qed. -lemma lfpx_zero: ∀h,I,G,L1,L2,V. - ⦃G, L1⦄ ⊢ ⬈[h, V] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, #0] L2.ⓑ{I}V. -/2 width=1 by lfxs_zero/ qed. +lemma lfpx_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_pair/ qed. -lemma lfpx_lref: ∀h,I,G,L1,L2,V1,V2,i. - ⦃G, L1⦄ ⊢ ⬈[h, #i] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, #⫯i] L2.ⓑ{I}V2. +lemma lfpx_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 lfpx_gref: ∀h,I,G,L1,L2,V1,V2,l. - ⦃G, L1⦄ ⊢ ⬈[h, §l] L2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ⬈[h, §l] L2.ⓑ{I}V2. +lemma lfpx_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 lfpx_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 lfpx_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,28 +63,28 @@ lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. lemma lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_inv_bind: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → @@ -97,13 +97,13 @@ lemma lfpx_inv_flat: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 (* Advanced inversion lemmas ************************************************) -lemma lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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 lfpx_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/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma index 8c5fc717f..1b8b6d763 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma @@ -34,9 +34,9 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → [ #H destruct /3 width=1 by aaa_zero/ | -HV12 * /4 width=7 by aaa_lifts, drops_refl, drops_drop/ ] -| #I #G #L1 #V1 #B #i #_ #IH #X2 #HX #Y #HY - elim (lfpx_inv_lref_pair_sn … HY) -HY #L2 #W2 #HL12 #H destruct - elim (cpx_inv_lref1_pair … HX) -HX +| #I #G #L1 #B #i #_ #IH #X2 #HX #Y #HY + elim (lfpx_inv_lref_bind_sn … HY) -HY #I2 #L2 #HL12 #H destruct + elim (cpx_inv_lref1_bind … HX) -HX [ #H destruct /3 width=1 by aaa_lref/ | * /4 width=7 by aaa_lifts, drops_refl, drops_drop/ ] @@ -44,14 +44,14 @@ lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → elim (lfpx_inv_bind … HL12) -HL12 #HV #HT elim (cpx_inv_abbr1 … HX) -HX * [ #V2 #T2 #HV12 #HT12 #H destruct - /4 width=2 by lfpx_pair_repl_dx, aaa_abbr/ + /5 width=2 by lfpx_bind_repl_dx, aaa_abbr, ext2_pair/ | #T2 #HT12 #HXT2 #H destruct -IHV /4 width=7 by aaa_inv_lifts, drops_drop, drops_refl/ ] | #p #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12 elim (lfpx_inv_bind … HL12) -HL12 #HV #HT elim (cpx_inv_abst1 … H) -H #V2 #T2 #HV12 #HT12 #H destruct - /4 width=2 by lfpx_pair_repl_dx, aaa_abst/ + /5 width=2 by lfpx_bind_repl_dx, aaa_abst, ext2_pair/ | #G #L1 #V1 #T1 #B #A #_ #_ #IHV #IHT #X2 #H #L2 #HL12 elim (lfpx_inv_flat … HL12) -HL12 #HV #HT elim (cpx_inv_appl1 … H) -H * diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma index 53b7d2e1f..8ae0af6af 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma @@ -34,10 +34,10 @@ lemma lfpx_drops_conf: ∀h,G. dropable_sn (cpx h G). lemma lfpx_drops_trans: ∀h,G. dropable_dx (cpx h G). /2 width=5 by lfxs_dropable_dx/ qed-. -lemma lfpx_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 lfpx_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 lfpx_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 lfpx_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/lfpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma index 2967a62bb..608907d5c 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 @@ -27,3 +27,15 @@ lemma lfpx_refl: ∀h,G,T. reflexive … (lfpx h G T). lemma lfpx_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 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.ⓧ. +/2 width=3 by lfxs_inv_bind_void/ qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lfpx_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/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma index d949c0a19..15004fe7f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma @@ -17,64 +17,77 @@ include "basic_2/static/frees_drops.ma". include "basic_2/static/lsubf_frees.ma". include "basic_2/static/lfxs.ma". include "basic_2/rt_transition/cpx_drops.ma". +include "basic_2/rt_transition/cpx_ext.ma". (* UNCOUNTED PARALLEL RT-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES *****) (* Properties with context-sensitive free variables *************************) (* Basic_2A1: uses: lpx_cpx_frees_trans *) +(* check sle_refl *) lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → - ∀L2. L1 ⪤*[cpx h G, cfull, f1] L2 → + ∀L2. L1 ⪤*[cpx_ext h G, cfull, f1] L2 → ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → ∃∃f2. L2 ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1. -#h #G #L1 #T1 @(fqup_wf_ind_eq … G L1 T1) -G -L1 -T1 +#h #G #L1 #T1 @(fqup_wf_ind_eq (Ⓣ) … G L1 T1) -G -L1 -T1 #G0 #L0 #U0 #IH #G #L1 * * [ -IH #s #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct lapply (frees_inv_sort … H1) -H1 #Hg1 elim (cpx_inv_sort1 … H0) -H0 #H destruct - /3 width=3 by frees_sort_gen, sle_refl, ex2_intro/ + /3 width=3 by frees_sort, sle_refl, ex2_intro/ | #i #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct elim (frees_inv_lref_drops … H1) -H1 * - [ -IH #HL1 #Hg1 + [ -IH #f1 #HL1 #Hf1 #H destruct elim (cpx_inv_lref1_drops … H0) -H0 [ #H destruct - /5 width=9 by frees_lref_atom, drops_atom2_lexs_conf, coafter_isuni_isid, sle_refl, ex2_intro/ - | * -H2 -Hg1 #I #K1 #V1 #V2 #HLK1 + /4 width=9 by frees_atom_drops, drops_atom2_lexs_conf, sle_refl, ex2_intro/ + | * -H2 -Hf1 #I #K1 #V1 #V2 #HLK1 lapply (drops_TF … HLK1) -HLK1 #HLK1 lapply (drops_mono … HLK1 … HL1) -L1 #H destruct ] | #f1 #I #K1 #V1 #Hf1 #HLK1 #H destruct elim (cpx_inv_lref1_drops … H0) -H0 [ #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #K2 #V2 #HLK2 #HK12 #HV12 + elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #Z #K2 #HLK2 #HK12 #H + elim (ext2_inv_pair_sn … H) -H #V2 #HV12 #H destruct elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -L1 -K1 -V1 #f2 #Hf2 #Hf21 - /4 width=7 by frees_lref_pushs, frees_lref_pair, drops_refl, sle_next, ex2_intro, sle_pushs/ - | * #J #Y #X #V2 #H #HV12 #HVU2 + /4 width=7 by frees_lref_pushs, frees_pair_drops, drops_refl, sle_pushs, sle_next, ex2_intro/ + | * #Z #Y #X #V2 #H #HV12 #HVU2 lapply (drops_mono … H … HLK1) -H #H destruct - elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #K2 #V0 #HLK2 #HK12 #_ + elim (lexs_drops_conf_next … H2 … HLK1) -H2 [ |*: // ] #I2 #K2 #HLK2 #HK12 #H + elim (ext2_inv_pair_sn … H) -H #V0 #_ #H destruct lapply (drops_isuni_fwd_drop2 … HLK2) // -V0 #HLK2 elim (IH … Hf1 … HK12 … HV12) /2 width=2 by fqup_lref/ -I -L1 -K1 -V1 #f2 #Hf2 #Hf21 lapply (frees_lifts … Hf2 … HLK2 … HVU2 ??) /4 width=7 by sle_weak, ex2_intro, sle_pushs/ ] + | #f1 #I #K1 #HLK1 #Hf1 #H destruct + elim (cpx_inv_lref1_drops … H0) -H0 + [ -IH #H destruct + elim (lexs_drops_conf_next … H2 … HLK1) -H2 -HLK1 [ |*: // ] #Z #K2 #HLK2 #_ #H + lapply (ext2_inv_unit_sn … H) -H #H destruct + /3 width=3 by frees_unit_drops, sle_refl, ex2_intro/ + | * -H2 -Hf1 #Z #Y1 #X1 #X2 #HLY1 + lapply (drops_mono … HLK1 … HLY1) -L1 #H destruct + ] ] | -IH #l #HG #HL #HU #g1 #H1 #L2 #_ #U2 #H0 destruct lapply (frees_inv_gref … H1) -H1 #Hg1 lapply (cpx_inv_gref1 … H0) -H0 #H destruct - /3 width=3 by frees_gref_gen, sle_refl, ex2_intro/ + /3 width=3 by frees_gref, sle_refl, ex2_intro/ | #p #I #V1 #T1 #HG #HL #HU #g1 #H1 #L2 #H2 #U2 #H0 destruct elim (frees_inv_bind … H1) -H1 #gV1 #gT1 #HgV1 #HgT1 #Hg1 elim (cpx_inv_bind1 … H0) -H0 * [ #V2 #T2 #HV12 #HT12 #H destruct lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … I … HL12T … HV12 ?) // -HL12T #HL12T + lapply (lexs_inv_tl … (BPair I V1) (BPair I V2) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ /4 width=10 by frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ | #T2 #HT12 #HUT2 #H0 #H1 destruct -HgV1 lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … Abbr … V1 V1 HL12T ??) // -HL12T #HL12T + lapply (lexs_inv_tl … (BPair Abbr V1) (BPair Abbr V1) … HL12T ??) /2 width=1 by ext2_pair/ -HL12T #HL12T elim (IH … HgT1 … HL12T … HT12) // -L1 -T1 #gT2 #HgT2 #HgT21 lapply (frees_inv_lifts_SO (Ⓣ) … HgT2 … L2 … HUT2) [ /3 width=1 by drops_refl, drops_drop/ ] -V1 -T2 /5 width=6 by sor_inv_sle_dx, sle_trans, sle_tl, ex2_intro/ @@ -103,45 +116,43 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … Abst … HL12T … HW12 ?) // -HL12T #HL12T + lapply (lexs_inv_tl … (BPair Abst W1) (BPair Abst W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 - lapply (sor_sym … Hg0) -Hg0 #Hg0 + lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 + lapply (sor_comm … Hg0) -Hg0 #Hg0 elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 - elim (sor_isfin_ex gV2 (⫱gT2)) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ - elim (lsubf_frees_trans … HgT2 (⫯gVT2) … (L2.ⓓⓝW2.V2)) - [2: /4 width=4 by lsubf_refl, lsubf_beta, sor_inv_sle_dx, sor_inv_sle_sn, sle_inv_tl_sn/ ] - -HgT2 #gT0 #HgT0 #HgT20 + elim (sor_isfin_ex (⫱gT2) gV2) /3 width=3 by frees_fwd_isfin, isfin_tl/ #gVT2 #HgVT2 #_ + elim (lsubf_beta_tl_dx … HgV2 … HgVT2 … W2) [ |*: /1 width=3 by lsubf_refl/ ] #gT0 #HL2 #HgT02 + lapply (lsubf_frees_trans … HgT2 … HL2) -HgT2 -HL2 #HgT0 + lapply (sor_comm … HgVT2) -HgVT2 #HgVT2 (**) (* this should be removed *) elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #gV0 #HgV0 #H elim (sor_isfin_ex gV0 (⫱gT0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ - @(ex2_intro … g2) - [ @(frees_bind … Hg2) /2 width=5 by frees_flat/ - | -L2 @(sor_inv_sle … Hg2) -Hg2 - [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ - | @sle_xn_tl [2:|*: // ] @(sle_trans … HgT20) -HgT20 - /4 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl, sle_next/ - ] (**) (* full auto too slow *) - ] + @(ex2_intro … g2) /3 width=5 by frees_flat, frees_bind/ -h -p -G -L1 -L2 -V1 -V2 -W1 -W2 -T1 -T2 + @(sor_inv_sle … Hg2) -Hg2 + [ /3 width=11 by sor_inv_sle_sn_trans, monotonic_sle_sor/ + | @(sle_trans … HgT02) -HgT02 + /3 width=8 by monotonic_sle_sor, sor_inv_sle_dx_trans, sle_tl/ + ] (**) (* full auto too slow *) | #p #V2 #V #W1 #W2 #T1 #T2 #HV12 #HV2 #HW12 #HT12 #H0 #H1 #H destruct elim (frees_inv_bind … HgT0) -HgT0 #gW1 #gT1 #HgW1 #HgT1 #HgT0 lapply (sle_lexs_trans … H2 gV1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12V lapply (sle_lexs_trans … H2 gT0 ?) /2 width=2 by sor_inv_sle_dx/ -H2 #H2 lapply (sle_lexs_trans … H2 gW1 ?) /2 width=2 by sor_inv_sle_sn/ #HL12W lapply (sle_lexs_trans … H2 (⫱gT1) ?) /2 width=2 by sor_inv_sle_dx/ -H2 #HL12T - lapply (lexs_inv_tl … Abbr … HL12T … HW12 ?) // -HL12T #HL12T + lapply (lexs_inv_tl … (BPair Abbr W1) (BPair Abbr W2) … HL12T ??) /2 width=1 by ext2_pair, I/ -HL12T #HL12T elim (sor_isfin_ex gV1 gW1) /2 width=3 by frees_fwd_isfin/ #g0 #Hg0 #_ - lapply (sor_trans2 … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 + lapply (sor_assoc_sn … Hg1 … HgT0 … Hg0) -Hg1 -HgT0 #Hg1 elim (IH … HgV1 … HL12V … HV12) // -HgV1 -HL12V -HV12 #gV2 #HgV2 #HgV21 elim (IH … HgW1 … HL12W … HW12) // -HgW1 -HL12W -HW12 #gW2 #HgW2 #HgW21 elim (IH … HgT1 … HL12T … HT12) // -IH -HgT1 -HL12T -HT12 #gT2 #HgT2 #HgT21 elim (sor_isfin_ex (↑gV2) gT2) /3 width=3 by frees_fwd_isfin, isfin_push/ #gV0 #HgV0 #H elim (sor_isfin_ex gW2 (⫱gV0)) /3 width=3 by frees_fwd_isfin, isfin_tl/ -H #g2 #Hg2 #_ elim (sor_isfin_ex gW2 gV2) /2 width=3 by frees_fwd_isfin/ #g #Hg #_ - lapply (sor_trans2 … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 + lapply (sor_assoc_sn … Hg2 … (⫱gT2) … Hg) /2 width=1 by sor_tl/ #Hg2 lapply (frees_lifts (Ⓣ) … HgV2 … (L2.ⓓW2) … HV2 ??) - [4: lapply (sor_sym … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) + [4: lapply (sor_comm … Hg) |*: /3 width=3 by drops_refl, drops_drop/ ] -V2 (**) (* full auto too slow *) /4 width=10 by frees_flat, frees_bind, monotonic_sle_sor, sle_tl, ex2_intro/ ] ] @@ -149,8 +160,8 @@ qed-. (* Basic_2A1: uses: cpx_frees_trans *) lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). -/3 width=7 by cpx_frees_conf_lfpx, lexs_refl/ qed-. +/4 width=7 by cpx_frees_conf_lfpx, lexs_refl, ext2_refl/ qed-. (* Basic_2A1: uses: lpx_frees_trans *) -lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx h G) cfull. +lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx_ext h G) cfull. /2 width=7 by cpx_frees_conf_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index ec9343106..414bfddd4 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -45,17 +45,17 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (lfdeq_inv_zero_pair_sn … H2) -H2 #K2 #X2 #HK02 #HX2 #H destruct elim (IH X2 … HK01 … HK02) // -K0 -V0 #V #HV1 #HV2 elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_delta, ex2_intro/ -| #I #G #K0 #V0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2 +| #I0 #G #K0 #V1 #W1 #i #_ #IH #HVW1 #T2 #H0 #L1 #H1 #L2 #H2 >(tdeq_inv_lref1 … H0) -H0 - elim (lfpx_inv_lref_pair_sn … H1) -H1 #K1 #X1 #HK01 #H destruct - elim (lfdeq_inv_lref_pair_sn … H2) -H2 #K2 #X2 #HK02 #H destruct - elim (IH … HK01 … HK02) [|*: //] -K0 -V0 #V #HV1 #HV2 + elim (lfpx_inv_lref_bind_sn … H1) -H1 #I1 #K1 #HK01 #H destruct + elim (lfdeq_inv_lref_bind_sn … H2) -H2 #I2 #K2 #HK02 #H destruct + elim (IH … HK01 … HK02) [|*: //] -K0 #V #HV1 #HV2 elim (tdeq_lifts_sn … HV1 … HVW1) -V1 /3 width=5 by cpx_lref, ex2_intro/ | #p #I #G #L0 #V0 #V1 #T0 #T1 #_ #_ #IHV #IHT #X0 #H0 #L1 #H1 #L2 #H2 elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct elim (lfpx_inv_bind … H1) -H1 #HL01 #H1 elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2 - lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 #H2 + lapply (lfdeq_bind_repl_dx … H2 (BPair I V2) ?) -H2 /2 width=1 by ext2_pair/ #H2 elim (IHV … HV02 … HL01 … HL02) -IHV -HV02 -HL01 -HL02 elim (IHT … HT02 … H1 … H2) -L0 -T0 /3 width=5 by cpx_bind, tdeq_pair, ex2_intro/ @@ -70,7 +70,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (tdeq_inv_pair1 … H0) -H0 #V2 #T2 #HV02 #HT02 #H destruct elim (lfpx_inv_bind … H1) -H1 #HL01 #H1 elim (lfdeq_inv_bind … H2) -H2 #HL02 #H2 - lapply (lfdeq_pair_repl_dx … H2 … HV02) -H2 -HV02 #H2 + lapply (lfdeq_bind_repl_dx … H2 (BPair Abbr V2) ?) -H2 /2 width=1 by ext2_pair/ -HV02 #H2 elim (IH … HT02 … H1 … H2) -L0 -T0 #T #HT1 elim (tdeq_inv_lifts_sn … HT1 … HUT1) -T1 /3 width=5 by cpx_zeta, ex2_intro/ @@ -93,7 +93,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0 elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2 elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0 - lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0 + lapply (lfdeq_bind_repl_dx … H2LT0 (BPair Abst W2) ?) -H2LT0 /2 width=1 by ext2_pair/ #H2LT0 elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0 elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0 @@ -105,7 +105,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( elim (lfpx_inv_bind … H1) -H1 #H1LW0 #H1LT0 elim (lfdeq_inv_flat … H2) -H2 #H2LV0 #H2 elim (lfdeq_inv_bind … H2) -H2 #H2LW0 #H2LT0 - lapply (lfdeq_pair_repl_dx … H2LT0 … HW02) -H2LT0 #H2LT0 + lapply (lfdeq_bind_repl_dx … H2LT0 (BPair Abbr W2) ?) -H2LT0 /2 width=1 by ext2_pair/ #H2LT0 elim (IHV … HV02 … H1LV0 … H2LV0) -IHV -HV02 -H1LV0 -H2LV0 #V #HV1 elim (IHW … HW02 … H1LW0 … H2LW0) -IHW -HW02 -H1LW0 -H2LW0 elim (IHT … HT02 … H1LT0 … H2LT0) -L0 -V0 -T0 @@ -114,7 +114,7 @@ lemma cpx_tdeq_conf_lexs: ∀h,o,G. R_confluent2_lfxs … (cpx h G) (cdeq h o) ( ] qed-. -lemma cpx_tdeq_conf: ∀h,o,G,L,T0,T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 → +lemma cpx_tdeq_conf: ∀h,o,G,L. ∀T0:term. ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 → ∀T2. T0 ≡[h, o] T2 → ∃∃T. T1 ≡[h, o] T & ⦃G, L⦄ ⊢ T2 ⬈[h] T. #h #o #G #L #T0 #T1 #HT01 #T2 #HT02 @@ -122,7 +122,7 @@ elim (cpx_tdeq_conf_lexs … HT01 … HT02 L … L) -HT01 -HT02 /2 width=3 by lfxs_refl, ex2_intro/ qed-. -lemma tdeq_cpx_trans: ∀h,o,G,L,T2,T0. T2 ≡[h, o] T0 → +lemma tdeq_cpx_trans: ∀h,o,G,L,T2. ∀T0:term. T2 ≡[h, o] T0 → ∀T1. ⦃G, L⦄ ⊢ T0 ⬈[h] T1 → ∃∃T. ⦃G, L⦄ ⊢ T2 ⬈[h] T & T ≡[h, o] T1. #h #o #G #L #T2 #T0 #HT20 #T1 #HT01 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma index a5c11db63..fa2277996 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/ffdeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_8.ma". +include "basic_2/notation/relations/lazyeqsn_8.ma". include "basic_2/syntax/genv.ma". include "basic_2/static/lfdeq.ma". @@ -24,7 +24,7 @@ inductive ffdeq (h) (o) (G) (L1) (T): relation3 genv lenv term ≝ interpretation "degree-based equivalence on referred entries (closure)" - 'LazyEq h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). + 'LazyEqSn h o G1 L1 T1 G2 L2 T2 = (ffdeq h o G1 L1 T1 G2 L2 T2). (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma index 476a459c8..0e1ae0e21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/frees_drops.ma @@ -77,20 +77,20 @@ lemma frees_inv_lref_drops: ∀L,i,f. L ⊢ 𝐅*⦃#i⦄ ≡ f → ∨∨ ∃∃g. ⬇*[Ⓕ, 𝐔❴i❵] L ≡ ⋆ & 𝐈⦃g⦄ & f = ↑*[i] ⫯g | ∃∃g,I,K,V. K ⊢ 𝐅*⦃V⦄ ≡ g & ⬇*[i] L ≡ K.ⓑ{I}V & f = ↑*[i] ⫯g - | ∃∃g,I,K. ⬇*[i] L ≡ K.ⓤ{I} & f = ↑*[i] ⫯g. + | ∃∃g,I,K. ⬇*[i] L ≡ K.ⓤ{I} & 𝐈⦃g⦄ & f = ↑*[i] ⫯g. #L elim L -L [ #i #g | #L #I #IH * [ #g cases I -I [ #I | #I #V ] -IH | #i #g ] ] #H [ elim (frees_inv_atom … H) -H #f #Hf #H destruct /3 width=3 by or3_intro0, ex3_intro/ | elim (frees_inv_unit … H) -H #f #Hf #H destruct - /4 width=3 by drops_refl, or3_intro2, ex2_3_intro/ + /4 width=3 by drops_refl, or3_intro2, ex3_3_intro/ | elim (frees_inv_pair … H) -H #f #Hf #H destruct /4 width=7 by drops_refl, or3_intro1, ex3_4_intro/ | elim (frees_inv_lref … H) -H #f #Hf #H destruct elim (IH … Hf) -IH -Hf * [ /4 width=3 by drops_drop, or3_intro0, ex3_intro/ | /4 width=7 by drops_drop, or3_intro1, ex3_4_intro/ - | /4 width=3 by drops_drop, or3_intro2, ex2_3_intro/ + | /4 width=3 by drops_drop, or3_intro2, ex3_3_intro/ ] ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index 8ef63e0eb..2d219c5ce 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeq_5.ma". +include "basic_2/notation/relations/lazyeqsn_5.ma". include "basic_2/syntax/tdeq_ext.ma". include "basic_2/static/lfxs.ma". @@ -23,11 +23,11 @@ definition lfdeq: ∀h. sd h → relation3 term lenv lenv ≝ interpretation "degree-based equivalence on referred entries (local environment)" - 'LazyEq h o T L1 L2 = (lfdeq h o T L1 L2). + 'LazyEqSn h o T L1 L2 = (lfdeq h o T L1 L2). interpretation "degree-based ranged equivalence (local environment)" - 'LazyEq h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2). + 'LazyEqSn h o f L1 L2 = (lexs (cdeq_ext h o) cfull f L1 L2). (* definition lfdeq_transitive: predicate (relation3 lenv term term) ≝ λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[h, o, T1] L2 → R L1 T1 T2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma index b6d5abd56..62b114915 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf.ma @@ -305,13 +305,24 @@ qed. lemma lsubf_refl_eq: ∀f1,f2,L. f1 ≗ f2 → ⦃L, f1⦄ ⫃𝐅* ⦃L, f2⦄. /2 width=3 by lsubf_eq_repl_back2/ qed. -lemma lsubf_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ → - ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1. +lemma lsubf_bind_tl_dx: ∀g1,f2,I,L1,L2. ⦃L1, g1⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ → + ∃∃f1. ⦃L1.ⓘ{I}, f1⦄ ⫃𝐅* ⦃L2.ⓘ{I}, f2⦄ & g1 = ⫱f1. #g1 #f2 #I #L1 #L2 #H elim (pn_split f2) * #g2 #H2 destruct @ex2_intro [1,2,4,5: /2 width=2 by lsubf_push, lsubf_bind/ ] // (**) (* constructor needed *) qed-. +lemma lsubf_beta_tl_dx: ∀f,f0,g1,L1,V. L1 ⊢ 𝐅*⦃V⦄ ≡ f → f0 ⋓ f ≡ g1 → + ∀f2,L2,W. ⦃L1, f0⦄ ⫃𝐅* ⦃L2, ⫱f2⦄ → + ∃∃f1. ⦃L1.ⓓⓝW.V, f1⦄ ⫃𝐅* ⦃L2.ⓛW, f2⦄ & ⫱f1 ⊆ g1. +#f #f0 #g1 #L1 #V #Hf #Hg1 #f2 +elim (pn_split f2) * #x2 #H2 #L2 #W #HL12 destruct +[ /3 width=4 by lsubf_push, sor_inv_sle_sn, ex2_intro/ +| @(ex2_intro … (⫯g1)) /2 width=5 by lsubf_beta/ (**) (* full auto fails *) +] +qed-. + +(* Note: this might be moved *) lemma lsubf_inv_sor_dx: ∀f1,f2,L1,L2. ⦃L1, f1⦄ ⫃𝐅* ⦃L2, f2⦄ → ∀f2l,f2r. f2l⋓f2r ≡ f2 → ∃∃f1l,f1r. ⦃L1, f1l⦄ ⫃𝐅* ⦃L2, f2l⦄ & ⦃L1, f1r⦄ ⫃𝐅* ⦃L2, f2r⦄ & f1l⋓f1r ≡ f1. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma index 09d8339d1..b1f39c812 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lsubf_frees.ma @@ -43,7 +43,7 @@ lemma lsubf_frees_trans: ∀f2,L2,T. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 → | /3 width=5 by lsubf_fwd_isid_dx, frees_gref/ | #f2V #f2T #f2 #p #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12 elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 #f1V #g1T #HV #HT #Hf1 - elim (lsubf_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct + elim (lsubf_bind_tl_dx … (BPair I V) … HT) -HT #f1T #HT #H destruct /3 width=5 by frees_bind/ | #f2V #f2T #f2 #I #L2 #V #T #_ #_ #Hf2 #IHV #IHT #f1 #L1 #H12 elim (lsubf_inv_sor_dx … H12 … Hf2) -f2 /3 width=5 by frees_flat/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index 9cf106377..43f538794 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -26,7 +26,7 @@ inductive tdeq (h) (o): relation term ≝ . interpretation - "degree-based equivalence (terms)" + "context-free degree-based equivalence (term)" 'LazyEq h o T1 T2 = (tdeq h o T1 T2). (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma index c4ed53ed0..096f2420d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_ext.ma @@ -12,20 +12,29 @@ (* *) (**************************************************************************) +include "basic_2/notation/relations/lazyeq_5.ma". include "basic_2/syntax/tdeq.ma". include "basic_2/syntax/lenv_ext2.ma". (* EXTENDED DEGREE-BASED EQUIVALENCE ****************************************) -definition cdeq: ∀h. sd h → relation3 lenv term term ≝ - λh,o,L. tdeq h o. - definition tdeq_ext: ∀h. sd h → relation bind ≝ λh,o. ext2 (tdeq h o). +definition cdeq: ∀h. sd h → relation3 lenv term term ≝ + λh,o,L. tdeq h o. + definition cdeq_ext: ∀h. sd h → relation3 lenv bind bind ≝ λh,o. cext2 (cdeq h o). interpretation - "degree-based equivalence (binder)" + "context-free degree-based equivalence (binder)" 'LazyEq h o I1 I2 = (tdeq_ext h o I1 I2). + +interpretation + "context-dependent degree-based equivalence (term)" + 'LazyEq h o L T1 T2 = (cdeq h o L T1 T2). + +interpretation + "context-dependent degree-based equivalence (binder)" + 'LazyEq h o L I1 I2 = (cdeq_ext h o L I1 I2). 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 80e174651..0fd7f15f7 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 @@ -123,6 +123,7 @@ table { ] } ] +*) class "cyan" [ { "rt-transition" * } { (* @@ -137,13 +138,14 @@ table { [ "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" * ] + [ "cpx_ext ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" * ] [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" + "cpx_lfxs" * ] } ] -*) [ { "counted context-sensitive rt-transition" * } { [ "cpg ( ⦃?,?⦄ ⊢ ? ⬈[?,?] ? )" "cpg_simple" + "cpg_drops" + "cpg_lsubr" * ] }