From bb6e68b2cf746bb3108543807207a1ca628ab442 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Feb 2016 19:02:11 +0000 Subject: [PATCH] first commit for lreq ... --- .../lpx_sn/{lpx_sn_alt.ma => lpx_sn_alt.etc} | 0 .../{lpx_sn_drop.ma => lpx_sn_drop.etc} | 0 .../lpx_sn/lpx_sn_lpx_sn.etc} | 0 .../lpx_sn/lpx_sn_tc.etc} | 0 .../lambdadelta/basic_2/etc_new/lreq/lreq.etc | 195 ------------------ .../relations/{lazyeq_4.ma => lazyeq_3.ma} | 4 +- .../{midiso_4.ma => relationstar_5.ma} | 4 +- .../lambdadelta/basic_2/relocation/lexs.ma | 140 +++++++------ .../basic_2/relocation/lexs_length.ma | 4 +- .../lambdadelta/basic_2/relocation/lreq.ma | 96 +++++++++ .../lreq_length.ma} | 13 +- 11 files changed, 183 insertions(+), 273 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/{lpx_sn_alt.ma => lpx_sn_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/{lpx_sn_drop.ma => lpx_sn_drop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lpx_sn_lpx_sn.ma => etc_new/lpx_sn/lpx_sn_lpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lpx_sn_tc.ma => etc_new/lpx_sn/lpx_sn_tc.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeq_4.ma => lazyeq_3.ma} (90%) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{midiso_4.ma => relationstar_5.ma} (88%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/relationstar_4.ma => relocation/lreq_length.ma} (72%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_lpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_tc.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc deleted file mode 100644 index b9493ad4b..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq.etc +++ /dev/null @@ -1,195 +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 "ground_2/ynat/ynat_lt.ma". -include "basic_2/notation/relations/midiso_4.ma". -include "basic_2/grammar/lenv_length.ma". - -(* EQUIVALENCE FOR LOCAL ENVIRONMENTS ***************************************) - -inductive lreq: relation4 ynat ynat lenv lenv ≝ -| lreq_atom: ∀l,m. lreq l m (⋆) (⋆) -| lreq_zero: ∀I1,I2,L1,L2,V1,V2. - lreq 0 0 L1 L2 → lreq 0 0 (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -| lreq_pair: ∀I,L1,L2,V,m. lreq 0 m L1 L2 → - lreq 0 (⫯m) (L1.ⓑ{I}V) (L2.ⓑ{I}V) -| lreq_succ: ∀I1,I2,L1,L2,V1,V2,l,m. - lreq l m L1 L2 → lreq (⫯l) m (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) -. - -interpretation - "equivalence (local environment)" - 'MidIso l m L1 L2 = (lreq l m L1 L2). - -(* Basic properties *********************************************************) - -lemma lreq_pair_lt: ∀I,L1,L2,V,m. L1 ⩬[0, ⫰m] L2 → 0 < m → - L1.ⓑ{I}V ⩬[0, m] L2.ⓑ{I}V. -#I #L1 #L2 #V #m #HL12 #Hm <(ylt_inv_O1 … Hm) /2 width=1 by lreq_pair/ -qed. - -lemma lreq_succ_lt: ∀I1,I2,L1,L2,V1,V2,l,m. L1 ⩬[⫰l, m] L2 → 0 < l → - L1.ⓑ{I1}V1 ⩬[l, m] L2. ⓑ{I2}V2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #Hl <(ylt_inv_O1 … Hl) /2 width=1 by lreq_succ/ -qed. - -lemma lreq_pair_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → - ∀I,V. L1.ⓑ{I}V ⩬[0, ∞] L2.ⓑ{I}V. -#L1 #L2 #HL12 #I #V lapply (lreq_pair I … V … HL12) -HL12 // -qed. - -lemma lreq_refl: ∀L,l,m. L ⩬[l, m] L. -#L elim L -L // -#L #I #V #IHL #l elim (ynat_cases … l) [| * #x ] -#Hl destruct /2 width=1 by lreq_succ/ -#m elim (ynat_cases … m) [| * #x ] -#Hm destruct /2 width=1 by lreq_zero, lreq_pair/ -qed. - -lemma lreq_O2: ∀L1,L2,l. |L1| = |L2| → L1 ⩬[l, 0] L2. -#L1 elim L1 -L1 [| #L1 #I1 #V1 #IHL1 ] -* // [1,3: #L2 #I2 #V2 ] #l -[ #H elim (ysucc_inv_O_sn … H) -| >length_pair >length_pair #H - lapply (ysucc_inv_inj … H) -H #HL12 - elim (ynat_cases l) /3 width=1 by lreq_zero/ - * /3 width=1 by lreq_succ/ -| #H elim (ysucc_inv_O_dx … H) -] -qed. - -lemma lreq_sym: ∀l,m. symmetric … (lreq l m). -#l #m #L1 #L2 #H elim H -L1 -L2 -l -m -/2 width=1 by lreq_zero, lreq_pair, lreq_succ/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lreq_inv_atom1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → L1 = ⋆ → L2 = ⋆. -#L1 #L2 #l #m * -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #H destruct -| #I #L1 #L2 #V #m #_ #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #H destruct -] -qed-. - -lemma lreq_inv_atom1: ∀L2,l,m. ⋆ ⩬[l, m] L2 → L2 = ⋆. -/2 width=5 by lreq_inv_atom1_aux/ qed-. - -fact lreq_inv_zero1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → l = 0 → m = 0 → - ∃∃J2,K2,W2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #HL12 #J1 #K1 #W1 #H #_ #_ destruct - /2 width=5 by ex2_3_intro/ -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #_ #H - elim (ysucc_inv_O_dx … H) -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J1 #K1 #W1 #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_zero1: ∀I1,K1,L2,V1. K1.ⓑ{I1}V1 ⩬[0, 0] L2 → - ∃∃I2,K2,V2. K1 ⩬[0, 0] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=9 by lreq_inv_zero1_aux/ qed-. - -fact lreq_inv_pair1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J,K1,W. L1 = K1.ⓑ{J}W → l = 0 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{J}W. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J #K1 #W #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J #K1 #W #_ #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #HL12 #J #K1 #W #H #_ #_ destruct - /2 width=3 by ex2_intro/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #J #K1 #W #_ #H - elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_pair1: ∀I,K1,L2,V,m. K1.ⓑ{I}V ⩬[0, m] L2 → 0 < m → - ∃∃K2. K1 ⩬[0, ⫰m] K2 & L2 = K2.ⓑ{I}V. -/2 width=6 by lreq_inv_pair1_aux/ qed-. - -lemma lreq_inv_pair: ∀I1,I2,L1,L2,V1,V2,m. L1.ⓑ{I1}V1 ⩬[0, m] L2.ⓑ{I2}V2 → 0 < m → - ∧∧ L1 ⩬[0, ⫰m] L2 & I1 = I2 & V1 = V2. -#I1 #I2 #L1 #L2 #V1 #V2 #m #H #Hm elim (lreq_inv_pair1 … H) -H // -#Y #HL12 #H destruct /2 width=1 by and3_intro/ -qed-. - -fact lreq_inv_succ1_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀J1,K1,W1. L1 = K1.ⓑ{J1}W1 → 0 < l → - ∃∃J2,K2,W2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{J2}W2. -#L1 #L2 #l #m * -L1 -L2 -l -m -[ #l #m #J1 #K1 #W1 #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I #L1 #L2 #V #m #_ #J1 #K1 #W1 #_ #H - elim (ylt_yle_false … H) // -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #HL12 #J1 #K1 #W1 #H #_ destruct - /2 width=5 by ex2_3_intro/ -] -qed-. - -lemma lreq_inv_succ1: ∀I1,K1,L2,V1,l,m. K1.ⓑ{I1}V1 ⩬[l, m] L2 → 0 < l → - ∃∃I2,K2,V2. K1 ⩬[⫰l, m] K2 & L2 = K2.ⓑ{I2}V2. -/2 width=5 by lreq_inv_succ1_aux/ qed-. - -lemma lreq_inv_atom2: ∀L1,l,m. L1 ⩬[l, m] ⋆ → L1 = ⋆. -/3 width=3 by lreq_inv_atom1, lreq_sym/ -qed-. - -lemma lreq_inv_succ: ∀I1,I2,L1,L2,V1,V2,l,m. L1.ⓑ{I1}V1 ⩬[l, m] L2.ⓑ{I2}V2 → 0 < l → - L1 ⩬[⫰l, m] L2. -#I1 #I2 #L1 #L2 #V1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … H) -H // -#Z #Y #X #HL12 #H destruct // -qed-. - -lemma lreq_inv_zero2: ∀I2,K2,L1,V2. L1 ⩬[0, 0] K2.ⓑ{I2}V2 → - ∃∃I1,K1,V1. K1 ⩬[0, 0] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #H elim (lreq_inv_zero1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -lemma lreq_inv_pair2: ∀I,K2,L1,V,m. L1 ⩬[0, m] K2.ⓑ{I}V → 0 < m → - ∃∃K1. K1 ⩬[0, ⫰m] K2 & L1 = K1.ⓑ{I}V. -#I #K2 #L1 #V #m #H #Hm elim (lreq_inv_pair1 … (lreq_sym … H)) -H -/3 width=3 by lreq_sym, ex2_intro/ -qed-. - -lemma lreq_inv_succ2: ∀I2,K2,L1,V2,l,m. L1 ⩬[l, m] K2.ⓑ{I2}V2 → 0 < l → - ∃∃I1,K1,V1. K1 ⩬[⫰l, m] K2 & L1 = K1.ⓑ{I1}V1. -#I2 #K2 #L1 #V2 #l #m #H #Hl elim (lreq_inv_succ1 … (lreq_sym … H)) -H -/3 width=5 by lreq_sym, ex2_3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lreq_fwd_length: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → |L1| = |L2|. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -qed-. - -(* Advanced inversion lemmas ************************************************) - -fact lreq_inv_O_Y_aux: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → l = 0 → m = ∞ → L1 = L2. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m // -[ #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #_ #H destruct -| /4 width=1 by eq_f3, ysucc_inv_Y_dx/ -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lreq_inv_O_Y: ∀L1,L2. L1 ⩬[0, ∞] L2 → L1 = L2. -/2 width=5 by lreq_inv_O_Y_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma similarity index 90% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma index 0cd902ba8..e2c7c0aff 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeq_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ break [ term 46 T , break term 46 f ] break term 46 L2 )" +notation "hvbox( L1 ≡ break [ term 46 f ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEq $T $f $L1 $L2 }. + for @{ 'LazyEq $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma index 20297e517..698b130c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/midiso_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_5.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ⩬ break [ term 46 f , break term 46 m ] break term 46 L2 )" +notation "hvbox( L1 ⦻ * break [ term 46 R1 , break term 46 R2 , break term 46 f ] break term 46 L2 )" non associative with precedence 45 - for @{ 'MidIso $f $k $L1 $L2 }. + for @{ 'RelationStar $R1 $R2 $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 38fd8e785..0bed76cfd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -13,144 +13,147 @@ (**************************************************************************) include "ground_2/relocation/nstream_sle.ma". -include "basic_2/notation/relations/relationstar_4.ma". +include "basic_2/notation/relations/relationstar_5.ma". include "basic_2/grammar/lenv.ma". (* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) -inductive lexs (R:relation4 bool lenv term term): rtmap → relation lenv ≝ -| lexs_atom: ∀f. lexs R f (⋆) (⋆) +inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ +| lexs_atom: ∀f. lexs RN RP f (⋆) (⋆) | lexs_next: ∀I,L1,L2,V1,V2,f. - lexs R f L1 L2 → R (Ⓣ) L1 V1 V2 → - lexs R (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) + lexs RN RP f L1 L2 → RN L1 V1 V2 → + lexs RN RP (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) | lexs_push: ∀I,L1,L2,V1,V2,f. - lexs R f L1 L2 → R (Ⓕ) L1 V1 V2 → - lexs R (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) + lexs RN RP f L1 L2 → RP L1 V1 V2 → + lexs RN RP (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) . interpretation "general entrywise extension (local environment)" - 'RelationStar R f L1 L2 = (lexs R f L1 L2). + 'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2). (* Basic inversion lemmas ***************************************************) -fact lexs_inv_atom1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → X = ⋆ → Y = ⋆. -#R #X #Y #f * -X -Y -f // +fact lexs_inv_atom1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → X = ⋆ → Y = ⋆. +#RN #RP #X #Y #f * -X -Y -f // #I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom1 *) -lemma lexs_inv_atom1: ∀R,Y,f. ⋆ ⦻*[R, f] Y → Y = ⋆. +lemma lexs_inv_atom1: ∀RN,RP,Y,f. ⋆ ⦻*[RN, RP, f] Y → Y = ⋆. /2 width=6 by lexs_inv_atom1_aux/ qed-. -fact lexs_inv_next1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & Y = K2.ⓑ{J}W2. -#R #X #Y #f * -X -Y -f +fact lexs_inv_next1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K1 #W1 #g #H destruct -| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K1 #W1 #g #H1 #H2 <(injective_next … H2) -g destruct /2 width=5 by ex3_2_intro/ | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_push_next … H) ] qed-. (* Basic_2A1: includes lpx_sn_inv_pair1 *) -lemma lexs_inv_next1: ∀R,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[R, ⫯g] Y → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & Y = K2.ⓑ{J}W2. +lemma lexs_inv_next1: ∀RN,RP,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RN, RP, ⫯g] Y → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & Y = K2.ⓑ{J}W2. /2 width=7 by lexs_inv_next1_aux/ qed-. -fact lexs_inv_push1_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & Y = K2.ⓑ{J}W2. -#R #X #Y #f * -X -Y -f +fact lexs_inv_push1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K1 #W1 #g #H destruct | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K1 #W1 #g #_ #H elim (discr_next_push … H) -| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K1 #W1 #g #H1 #H2 <(injective_push … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lexs_inv_push1: ∀R,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[R, ↑g] Y → - ∃∃K2,W2. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & Y = K2.ⓑ{J}W2. +lemma lexs_inv_push1: ∀RN,RP,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RN, RP, ↑g] Y → + ∃∃K2,W2. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & Y = K2.ⓑ{J}W2. /2 width=7 by lexs_inv_push1_aux/ qed-. -fact lexs_inv_atom2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → Y = ⋆ → X = ⋆. -#R #X #Y #f * -X -Y -f // +fact lexs_inv_atom2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → Y = ⋆ → X = ⋆. +#RN #RP #X #Y #f * -X -Y -f // #I #L1 #L2 #V1 #V2 #f #_ #_ #H destruct qed-. (* Basic_2A1: includes lpx_sn_inv_atom2 *) -lemma lexs_inv_atom2: ∀R,X,f. X ⦻*[R, f] ⋆ → X = ⋆. +lemma lexs_inv_atom2: ∀RN,RP,X,f. X ⦻*[RN, RP, f] ⋆ → X = ⋆. /2 width=6 by lexs_inv_atom2_aux/ qed-. -fact lexs_inv_next2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & X = K1.ⓑ{J}W1. -#R #X #Y #f * -X -Y -f +fact lexs_inv_next2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & X = K1.ⓑ{J}W1. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K2 #W2 #g #H destruct -| #I #L1 #L2 #V1 #V2 #f #HL #HS #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K2 #W2 #g #H1 #H2 <(injective_next … H2) -g destruct /2 width=5 by ex3_2_intro/ | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_push_next … H) ] qed-. (* Basic_2A1: includes lpx_sn_inv_pair2 *) -lemma lexs_inv_next2: ∀R,J,X,K2,W2,g. X ⦻*[R, ⫯g] K2.ⓑ{J}W2 → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓣ) K1 W1 W2 & X = K1.ⓑ{J}W1. +lemma lexs_inv_next2: ∀RN,RP,J,X,K2,W2,g. X ⦻*[RN, RP, ⫯g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RN K1 W1 W2 & X = K1.ⓑ{J}W1. /2 width=7 by lexs_inv_next2_aux/ qed-. -fact lexs_inv_push2_aux: ∀R,X,Y,f. X ⦻*[R, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & X = K1.ⓑ{J}W1. -#R #X #Y #f * -X -Y -f +fact lexs_inv_push2_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & X = K1.ⓑ{J}W1. +#RN #RP #X #Y #f * -X -Y -f [ #f #J #K2 #W2 #g #H destruct | #I #L1 #L2 #V1 #V2 #f #_ #_ #J #K2 #W2 #g #_ #H elim (discr_next_push … H) -| #I #L1 #L2 #V1 #V2 #f #HL #HO #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct +| #I #L1 #L2 #V1 #V2 #f #HL #HV #J #K2 #W2 #g #H1 #H2 <(injective_push … H2) -g destruct /2 width=5 by ex3_2_intro/ ] qed-. -lemma lexs_inv_push2: ∀R,J,X,K2,W2,g. X ⦻*[R, ↑g] K2.ⓑ{J}W2 → - ∃∃K1,W1. K1 ⦻*[R, g] K2 & R (Ⓕ) K1 W1 W2 & X = K1.ⓑ{J}W1. +lemma lexs_inv_push2: ∀RN,RP,J,X,K2,W2,g. X ⦻*[RN, RP, ↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RN, RP, g] K2 & RP K1 W1 W2 & X = K1.ⓑ{J}W1. /2 width=7 by lexs_inv_push2_aux/ qed-. (* Basic_2A1: includes lpx_sn_inv_pair *) -lemma lexs_inv_next: ∀R,I1,I2,L1,L2,V1,V2,f. - L1.ⓑ{I1}V1 ⦻*[R, ⫯f] (L2.ⓑ{I2}V2) → - ∧∧ L1 ⦻*[R, f] L2 & R (Ⓣ) L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H +lemma lexs_inv_next: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RN, RP, ⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RN, RP, f] L2 & RN L1 V1 V2 & I1 = I2. +#RN #RP #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_next1 … H) -H #L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ qed-. -lemma lexs_inv_push: ∀R,I1,I2,L1,L2,V1,V2,f. - L1.ⓑ{I1}V1 ⦻*[R, ↑f] (L2.ⓑ{I2}V2) → - ∧∧ L1 ⦻*[R, f] L2 & R (Ⓕ) L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H +lemma lexs_inv_push: ∀RN,RP,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RN, RP, ↑f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RN, RP, f] L2 & RP L1 V1 V2 & I1 = I2. +#RN #RP #I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push1 … H) -H #L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ qed-. (* Basic properties *********************************************************) -lemma lexs_eq_repl_back: ∀R,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[R, f] L2). -#R #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // -[ #I #L1 #L2 #V1 #v2 #f1 #_ #HS #IH #f2 #H elim (next_inv_sn … H) -H /3 width=1 by lexs_next/ -| #I #L1 #L2 #V1 #v2 #f1 #_ #HO #IH #f2 #H elim (push_inv_sn … H) -H /3 width=1 by lexs_push/ +lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RN, RP, f] L2). +#RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // +#I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H +[ elim (next_inv_sn … H) -H /3 width=1 by lexs_next/ +| elim (push_inv_sn … H) -H /3 width=1 by lexs_push/ ] qed-. -lemma lexs_eq_repl_fwd: ∀R,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[R, f] L2). -#R #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) +lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[RN, RP, f] L2). +#RN #RP #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) qed-. +(* Note: fexs_sym and fexs_trans hold, but lexs_sym and lexs_trans do not *) (* Basic_2A1: includes: lpx_sn_refl *) -lemma lexs_refl: ∀R,f. - (∀b,L. reflexive … (R b L)) → - reflexive … (lexs R f). -#R #f #HR #L generalize in match f; -f elim L -L // +lemma lexs_refl: ∀RN,RP,f. + (∀L. reflexive … (RN L)) → + (∀L. reflexive … (RP L)) → + reflexive … (lexs RN RP f). +#RN #RP #f #HRN #HRP #L generalize in match f; -f elim L -L // #L #I #V #IH * * /2 width=1 by lexs_next, lexs_push/ qed. -lemma sle_lexs_trans: ∀R. (∀L,T1,T2. R (Ⓣ) L T1 T2 → R (Ⓕ) L T1 T2) → - ∀L1,L2,f2. L1 ⦻*[R, f2] L2 → - ∀f1. f1 ⊆ f2 → L1 ⦻*[R, f1] L2. -#R #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) → + ∀L1,L2,f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ⦻*[RN, RP, f1] L2. +#RN #RP #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // #I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH [ * * [2: #n1 ] ] #f1 #H [ /4 width=5 by lexs_next, sle_inv_SS_aux/ @@ -160,10 +163,10 @@ lemma sle_lexs_trans: ∀R. (∀L,T1,T2. R (Ⓣ) L T1 T2 → R (Ⓕ) L T1 T2) ] qed-. -lemma sle_lexs_conf: ∀R. (∀L,T1,T2. R (Ⓕ) L T1 T2 → R (Ⓣ) L T1 T2) → - ∀L1,L2,f1. L1 ⦻*[R, f1] L2 → - ∀f2. f1 ⊆ f2 → L1 ⦻*[R, f2] L2. -#R #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) → + ∀L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. f1 ⊆ f2 → L1 ⦻*[RN, RP, f2] L2. +#RN #RP #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // #I #L1 #L2 #V1 #V2 #f1 #_ #HV12 #IH [2: * * [2: #n2 ] ] #f2 #H [ /4 width=5 by lexs_next, sle_inv_OS_aux/ @@ -173,10 +176,11 @@ lemma sle_lexs_conf: ∀R. (∀L,T1,T2. R (Ⓕ) L T1 T2 → R (Ⓣ) L T1 T2) → ] qed-. -lemma lexs_co: ∀R1,R2. - (∀b,L1,T1,T2. R1 b L1 T1 T2 → R2 b L1 T1 T2) → - ∀L1,L2,f. L1 ⦻*[R1, f] L2 → L1 ⦻*[R2, f] L2. -#R1 #R2 #HR #L1 #L2 #f #H elim H -L1 -L2 -f +lemma lexs_co: ∀RN1,RP1,RN2,RP2. + (∀L1,T1,T2. RN1 L1 T1 T2 → RN2 L1 T1 T2) → + (∀L1,T1,T2. RP1 L1 T1 T2 → RP2 L1 T1 T2) → + ∀L1,L2,f. L1 ⦻*[RN1, RP1, f] L2 → L1 ⦻*[RN2, RP2, f] L2. +#RN1 #RP1 #RN2 #RP2 #HRN #HRP #L1 #L2 #f #H elim H -L1 -L2 -f /3 width=1 by lexs_atom, lexs_next, lexs_push/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma index c3626ee27..c8d3536de 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_length.ma @@ -20,6 +20,6 @@ include "basic_2/relocation/lexs.ma". (* Forward lemmas on length for local environments **************************) (* Basic_2A1: includes: lpx_sn_fwd_length *) -lemma lexs_fwd_length: ∀R,L1,L2,f. L1 ⦻*[R, f] L2 → |L1| = |L2|. -#R #L1 #L2 #f #H elim H -L1 -L2 -f // +lemma lexs_fwd_length: ∀RN,RP,L1,L2,f. L1 ⦻*[RN, RP, f] L2 → |L1| = |L2|. +#RM #RP #L1 #L2 #f #H elim H -L1 -L2 -f // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma new file mode 100644 index 000000000..568dad1ae --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -0,0 +1,96 @@ +(**************************************************************************) +(* ___ *) +(* ||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/lazyeq_3.ma". +include "basic_2/grammar/ceq.ma". +include "basic_2/relocation/lexs.ma". + +(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) + +(* Basic_2A1: includes: lreq_atom lreq_zero lreq_pair lreq_succ *) +definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq cfull. + +interpretation + "ranged equivalence (local environment)" + 'LazyEq f L1 L2 = (lreq f L1 L2). + +(* Basic properties *********************************************************) + +lemma lreq_eq_repl_back: ∀L1,L2. eq_stream_repl_back … (λf. L1 ≡[f] L2). +/2 width=3 by lexs_eq_repl_back/ qed-. + +lemma lreq_eq_repl_fwd: ∀L1,L2. eq_stream_repl_fwd … (λf. L1 ≡[f] L2). +/2 width=3 by lexs_eq_repl_fwd/ qed-. + +lemma sle_lreq_trans: ∀L1,L2,f2. L1 ≡[f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ≡[f1] L2. +/2 width=3 by sle_lexs_trans/ qed-. + +(* Basic_2A1: includes: lreq_refl *) +lemma lreq_refl: ∀f. reflexive … (lreq f). +/2 width=1 by lexs_refl/ qed. + +(* Basic_2A1: includes: lreq_sym *) +lemma lreq_sym: ∀f. symmetric … (lreq f). +#f #L1 #L2 #H elim H -L1 -L2 -f +/2 width=1 by lexs_next, lexs_push/ +qed-. + +(* Basic inversion lemmas ***************************************************) + +(* Basic_2A1: includes: lreq_inv_atom1 *) +lemma lreq_inv_atom1: ∀Y,f. ⋆ ≡[f] Y → Y = ⋆. +/2 width=4 by lexs_inv_atom1/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair1 *) +lemma lreq_inv_next1: ∀J,K1,Y,W1,g. K1.ⓑ{J}W1 ≡[⫯g] Y → + ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓑ{J}W1. +#J #K1 #Y #W1 #g #H elim (lexs_inv_next1 … H) -H /2 width=3 by ex2_intro/ +qed-. + +(* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *) +lemma lreq_inv_push1: ∀J,K1,Y,W1,g. K1.ⓑ{J}W1 ≡[↑g] Y → + ∃∃K2,W2. K1 ≡[g] K2 & Y = K2.ⓑ{J}W2. +#J #K1 #Y #W1 #g #H elim (lexs_inv_push1 … H) -H /2 width=4 by ex2_2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_atom2 *) +lemma lreq_inv_atom2: ∀X,f. X ≡[f] ⋆ → X = ⋆. +/2 width=4 by lexs_inv_atom2/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair2 *) +lemma lreq_inv_next2: ∀J,X,K2,W2,g. X ≡[⫯g] K2.ⓑ{J}W2 → + ∃∃K1. K1 ≡[g] K2 & X = K1.ⓑ{J}W2. +#J #X #K2 #W2 #g #H elim (lexs_inv_next2 … H) -H /2 width=3 by ex2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *) +lemma lreq_inv_push2: ∀J,X,K2,W2,g. X ≡[↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ≡[g] K2 & X = K1.ⓑ{J}W1. +#J #X #K2 #W2 #g #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/ qed-. + +(* Basic_2A1: includes: lreq_inv_pair *) +lemma lreq_inv_next: ∀I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ≡[⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ≡[f] L2 & V1 = V2 & I1 = I2. +/2 width=1 by lexs_inv_next/ qed-. + +(* Basic_2A1: includes: lreq_inv_succ *) +lemma lreq_inv_push: ∀I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ≡[↑f] (L2.ⓑ{I2}V2) → + L1 ≡[f] L2 ∧ I1 = I2. +#I1 #I2 #L1 #L2 #V1 #V2 #f #H elim (lexs_inv_push … H) -H /2 width=1 by conj/ +qed-. + +(* Basic_2A1: removed theorems 5: + lreq_pair_lt lreq_succ_lt lreq_pair_O_Y lreq_O2 lreq_inv_O_Y +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma similarity index 72% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma index 6015011d4..1b932c460 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/relationstar_4.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma @@ -12,8 +12,13 @@ (* *) (**************************************************************************) -(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) +include "basic_2/relocation/lexs_length.ma". +include "basic_2/relocation/lreq.ma". -notation "hvbox( L1 ⦻ * break [ term 46 R , break term 46 f ] break term 46 L2 )" - non associative with precedence 45 - for @{ 'RelationStar $R $f $L1 $L2 }. +(* RANGED EQUIVALENCE FOR LOCAL ENVIRONMENTS ********************************) + +(* Forward lemmas on length for local environments **************************) + +(* Basic_2A1: includes: lreq_fwd_length *) +lemma lreq_fwd_length: ∀L1,L2,f. L1 ≡[f] L2 → |L1| = |L2|. +/2 width=4 by lexs_fwd_length/ qed-. -- 2.39.2