From 093a2290feb8244a2397fa4767c283893a59f5e5 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 10 Feb 2016 11:20:14 +0000 Subject: [PATCH] pre commit for lexs ... --- .../lpx_sn}/lpx_sn_alt.ma | 0 .../basic_2/etc_new/lpx_sn/lpx_sn_drop.ma | 58 ++++++ .../lambdadelta/basic_2/relocation/lpx_sn.ma | 191 ++++++++++++++++++ .../basic_2/relocation/lpx_sn_drops.ma | 93 +++++++++ .../basic_2/substitution/lpx_sn.ma | 89 -------- .../basic_2/substitution/lpx_sn_drop.ma | 101 --------- .../basic_2/substitution/lpx_sn_tc.ma | 10 +- 7 files changed, 347 insertions(+), 195 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{substitution => etc_new/lpx_sn}/lpx_sn_alt.ma (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_drops.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_alt.ma 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.ma new file mode 100644 index 000000000..f69814078 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_drop.ma @@ -0,0 +1,58 @@ +definition dropable_dx: predicate (relation lenv) ≝ + λR. ∀L1,L2. R L1 L2 → ∀K2,c,k. ⬇[c, 0, k] L2 ≡ K2 → + ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & R K1 K2. + +lemma dropable_dx_TC: ∀R. dropable_dx R → dropable_dx (TC … R). +#R #HR #L1 #L2 #H elim H -L2 +[ #L2 #HL12 #K2 #c #k #HLK2 elim (HR … HL12 … HLK2) -HR -L2 + /3 width=3 by inj, ex2_intro/ +| #L #L2 #_ #HL2 #IHL1 #K2 #c #k #HLK2 elim (HR … HL2 … HLK2) -HR -L2 + #K #HLK #HK2 elim (IHL1 … HLK) -L + /3 width=5 by step, ex2_intro/ +] +qed-. + + +fact lpx_sn_dropable_aux: ∀R,L2,K2,c,l,k. ⬇[c, l, k] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → + l = 0 → ∃∃K1. ⬇[c, 0, k] L1 ≡ K1 & lpx_sn R K1 K2. +#R #L2 #K2 #c #l #k #H elim H -L2 -K2 -l -k +[ #l #k #Hm #X #H >(lpx_sn_inv_atom2 … H) -H + /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ +| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H + #K1 #V1 #HK12 #HV12 #H destruct + /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ +| #I #L2 #K2 #V2 #k #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #HL12 #HV12 #H destruct + elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #l #k #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) +] +qed-. + +lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). +/2 width=5 by lpx_sn_dropable_aux/ qed-. + +lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. + +lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → + ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. +#R #L1 #L2 #H elim H -L1 -L2 +[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct +| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H + [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ + | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 + /3 width=5 by drop_drop_lt, ex3_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma new file mode 100644 index 000000000..513d62019 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn.ma @@ -0,0 +1,191 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/nstream_sle.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 (RS,RO:relation3 lenv term term): rtmap → relation lenv ≝ +| lexs_atom: ∀f. lexs RS RO f (⋆) (⋆) +| lexs_next: ∀I,L1,L2,V1,V2,f. + lexs RS RO f L1 L2 → RS L1 V1 V2 → + lexs RS RO (⫯f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) +| lexs_push: ∀I,L1,L2,V1,V2,f. + lexs RS RO f L1 L2 → RO L1 V1 V2 → + lexs RS RO (↑f) (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) +. + +interpretation "general entrywise extension (local environment)" + 'RelationStar RS RO f L1 L2 = (lexs RS RO f L1 L2). + +(* Basic inversion lemmas ***************************************************) + +fact lexs_inv_atom1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → X = ⋆ → Y = ⋆. +#RS #RO #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: ∀RS,RO,Y,f. ⋆ ⦻*[RS, RO, f] Y → Y = ⋆. +/2 width=6 by lexs_inv_atom1_aux/ qed-. + +fact lexs_inv_next1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ⫯g → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RS #RO #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 + /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: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ⫯g] Y → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & Y = K2.ⓑ{J}W2. +/2 width=7 by lexs_inv_next1_aux/ qed-. + + +fact lexs_inv_push1_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K1,W1,g. X = K1.ⓑ{J}W1 → f = ↑g → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2. +#RS #RO #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 + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lexs_inv_push1: ∀RS,RO,J,K1,Y,W1,g. K1.ⓑ{J}W1 ⦻*[RS, RO, ↑g] Y → + ∃∃K2,W2. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & Y = K2.ⓑ{J}W2. +/2 width=7 by lexs_inv_push1_aux/ qed-. + +fact lexs_inv_atom2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → Y = ⋆ → X = ⋆. +#RS #RO #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: ∀RS,RO,X,f. X ⦻*[RS, RO, f] ⋆ → X = ⋆. +/2 width=6 by lexs_inv_atom2_aux/ qed-. + +fact lexs_inv_next2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ⫯g → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1. +#RS #RO #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 + /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: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ⫯g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RS K1 W1 W2 & X = K1.ⓑ{J}W1. +/2 width=7 by lexs_inv_next2_aux/ qed-. + +fact lexs_inv_push2_aux: ∀RS,RO,X,Y,f. X ⦻*[RS, RO, f] Y → ∀J,K2,W2,g. Y = K2.ⓑ{J}W2 → f = ↑g → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO K1 W1 W2 & X = K1.ⓑ{J}W1. +#RS #RO #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 + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lexs_inv_push2: ∀RS,RO,J,X,K2,W2,g. X ⦻*[RS, RO, ↑g] K2.ⓑ{J}W2 → + ∃∃K1,W1. K1 ⦻*[RS, RO, g] K2 & RO 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: ∀RS,RO,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RS, RO, ⫯f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RS, RO, f] L2 & RS L1 V1 V2 & I1 = I2. +#RS #RO #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: ∀RS,RO,I1,I2,L1,L2,V1,V2,f. + L1.ⓑ{I1}V1 ⦻*[RS, RO, ↑f] (L2.ⓑ{I2}V2) → + ∧∧ L1 ⦻*[RS, RO, f] L2 & RO L1 V1 V2 & I1 = I2. +#RS #RO #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: ∀RS,RO,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RS, RO, f] L2). +#RS #RO #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/ +] +qed-. + +lemma lexs_eq_repl_fwd: ∀RS,RO,L1,L2. eq_stream_repl_fwd … (λf. L1 ⦻*[RS, RO, f] L2). +#RS #RO #L1 #L2 @eq_stream_repl_sym /2 width=3 by lexs_eq_repl_back/ (**) (* full auto fails *) +qed-. + +(* Basic_2A1: includes: lpx_sn_refl *) +lemma lexs_refl: ∀RS,RO,f. + (∀L. reflexive … (RS L)) → + (∀L. reflexive … (RO L)) → + reflexive … (lexs RS RO f). +#RS #RO #f #HS #HO #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: ∀RS,RO. (∀L,T1,T2. RO L T1 T2 → RS L T1 T2) → + ∀L1,L2,f2. L1 ⦻*[RS, RO, f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ⦻*[RS, RO, f1] L2. +#RS #RO #HR #L1 #L2 #f2 #H elim H -L1 -L2 -f2 // +#I #L1 #L2 #V1 #V2 #f2 #_ #HV12 #IH +[2: * * [2: #n1 ] ] #f1 #H +[ (lpx_sn_inv_atom1 … H) -H + /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/ +| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H + #K2 #V2 #HK12 #HV12 #H destruct + lapply (lpx_sn_fwd_length … HK12) + #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) + /3 width=1 by lpx_sn_pair, lreq_O2/ +| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 + /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/ +| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H + elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct + elim (H2R … HW12 … HLK1 … HWV1) -W1 + elim (IHLK1 … HK12) -K1 + /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/ +] +qed-. +*) +include "ground_2/relocation/trace_isun.ma". + +lemma lpx_sn_dropable: ∀R,L2,K2,c,t. ⬇*[c, t] L2 ≡ K2 → 𝐔⦃t⦄ → + ∀L1,u2. lpx_sn R u2 L1 L2 → ∀u1. t ⊚ u1 ≡ u2 → + ∃∃K1. ⬇*[c, t] L1 ≡ K1 & lpx_sn R u1 K1 K2. +#R #L2 #K2 #c #t #H elim H -L2 -K2 -t +[ #t #Ht #_ #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom2 … H) -H + #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu + /4 width=3 by drops_atom, lpx_sn_atom, ex2_intro/ +| #I #L2 #K2 #V2 #t #_ #IH #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu + #u #H #Hu destruct elim (IH … HL … Hu) -L2 /3 width=3 by drops_drop, isun_inv_false, ex2_intro/ +| #I #L2 #K2 #V2 #W2 #t #_ #HWV #IHLK #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair2 … H) -H + #L1 #V1 #y2 #x #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu + #y1 #y #x2 #H1 #H2 #Hu destruct lapply (isun_inv_true … Ht) -Ht + #Ht elim (IHLK … HL … Hu) -L2 -Hu /2 width=1 by isun_id/ + #K1 #HLK1 #HK12 lapply (lifts_fwd_isid … HWV ?) // -HWV + #H destruct lapply (drops_fwd_isid … HLK1 ?) // + #H destruct + @ex2_intro + [ + | @(drops_skip … HLK1) + | @(lpx_sn_pair … HK12 … HV) + + + lapply (drops_fwd_isid … HLK1 ?) // -HLK1 + 2: + + + + + elim (HR … HV … HLK … HWV) -V1 + elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/ + + +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma deleted file mode 100644 index 82664b828..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn.ma +++ /dev/null @@ -1,89 +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/grammar/lenv_length.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -inductive lpx_sn (R:relation3 lenv term term): relation lenv ≝ -| lpx_sn_atom: lpx_sn R (⋆) (⋆) -| lpx_sn_pair: ∀I,K1,K2,V1,V2. - lpx_sn R K1 K2 → R K1 V1 V2 → - lpx_sn R (K1. ⓑ{I} V1) (K2. ⓑ{I} V2) -. - -(* Basic properties *********************************************************) - -lemma lpx_sn_refl: ∀R. (∀L. reflexive ? (R L)) → reflexive … (lpx_sn R). -#R #HR #L elim L -L /2 width=1 by lpx_sn_atom, lpx_sn_pair/ -qed-. - -(* Basic inversion lemmas ***************************************************) - -fact lpx_sn_inv_atom1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L1 = ⋆ → L2 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom1: ∀R,L2. lpx_sn R (⋆) L2 → L2 = ⋆. -/2 width=4 by lpx_sn_inv_atom1_aux/ qed-. - -fact lpx_sn_inv_pair1_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K1,V1. L1 = K1. ⓑ{I} V1 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #L1 #L2 * -L1 -L2 -[ #J #K1 #V1 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #L #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair1: ∀R,I,K1,V1,L2. lpx_sn R (K1. ⓑ{I} V1) L2 → - ∃∃K2,V2. lpx_sn R K1 K2 & R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by lpx_sn_inv_pair1_aux/ qed-. - -fact lpx_sn_inv_atom2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → L2 = ⋆ → L1 = ⋆. -#R #L1 #L2 * -L1 -L2 -[ // -| #I #K1 #K2 #V1 #V2 #_ #_ #H destruct -] -qed-. - -lemma lpx_sn_inv_atom2: ∀R,L1. lpx_sn R L1 (⋆) → L1 = ⋆. -/2 width=4 by lpx_sn_inv_atom2_aux/ qed-. - -fact lpx_sn_inv_pair2_aux: ∀R,L1,L2. lpx_sn R L1 L2 → ∀I,K2,V2. L2 = K2. ⓑ{I} V2 → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #L1 #L2 * -L1 -L2 -[ #J #K2 #V2 #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lpx_sn_inv_pair2: ∀R,I,L1,K2,V2. lpx_sn R L1 (K2. ⓑ{I} V2) → - ∃∃K1,V1. lpx_sn R K1 K2 & R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -/2 width=3 by lpx_sn_inv_pair2_aux/ qed-. - -lemma lpx_sn_inv_pair: ∀R,I1,I2,L1,L2,V1,V2. - lpx_sn R (L1.ⓑ{I1}V1) (L2.ⓑ{I2}V2) → - ∧∧ lpx_sn R L1 L2 & R L1 V1 V2 & I1 = I2. -#R #I1 #I2 #L1 #L2 #V1 #V2 #H elim (lpx_sn_inv_pair1 … H) -H -#L0 #V0 #HL10 #HV10 #H destruct /2 width=1 by and3_intro/ -qed-. - -(* Basic forward lemmas *****************************************************) - -lemma lpx_sn_fwd_length: ∀R,L1,L2. lpx_sn R L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L1 -L2 // -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma deleted file mode 100644 index 612f16a37..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_drop.ma +++ /dev/null @@ -1,101 +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/substitution/drop_lreq.ma". -include "basic_2/substitution/lpx_sn.ma". - -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) - -(* Properties on dropping ****************************************************) - -lemma lpx_sn_drop_conf: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K1,V1,i. ⬇[i] L1 ≡ K1.ⓑ{I}V1 → - ∃∃K2,V2. ⬇[i] L2 ≡ K2.ⓑ{I}V2 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_drop_trans: ∀R,L1,L2. lpx_sn R L1 L2 → - ∀I,K2,V2,i. ⬇[i] L2 ≡ K2.ⓑ{I}V2 → - ∃∃K1,V1. ⬇[i] L1 ≡ K1.ⓑ{I}V1 & lpx_sn R K1 K2 & R K1 V1 V2. -#R #L1 #L2 #H elim H -L1 -L2 -[ #I0 #K0 #V0 #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I #K1 #K2 #V1 #V2 #HK12 #HV12 #IHK12 #I0 #K0 #V0 #i #H elim (drop_inv_O1_pair1 … H) * -H - [ -IHK12 #H1 #H2 destruct /3 width=5 by drop_pair, ex3_2_intro/ - | -HK12 -HV12 #Hi #HK10 elim (IHK12 … HK10) -IHK12 -HK10 - /3 width=5 by drop_drop_lt, ex3_2_intro/ - ] -] -qed-. - -lemma lpx_sn_deliftable_dropable: ∀R. d_deliftable_sn R → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L1 #K1 #V1 #m #_ #IHLK1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #HL12 #HV12 #H destruct - elim (IHLK1 … HL12) -L1 /3 width=3 by drop_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #L2 #V2 #HL12 #HV12 #H destruct - elim (HR … HV12 … HLK1 … HWV1) -V1 - elim (IHLK1 … HL12) -L1 /3 width=5 by drop_skip, lpx_sn_pair, ex2_intro/ -] -qed-. - -lemma lpx_sn_liftable_dedropable: ∀R. (∀L. reflexive ? (R L)) → - d_liftable R → dedropable_sn (lpx_sn R). -#R #H1R #H2R #L1 #K1 #s #l #m #H elim H -L1 -K1 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom1 … H) -H - /4 width=4 by drop_atom, lpx_sn_atom, ex3_intro/ -| #I #K1 #V1 #X #H elim (lpx_sn_inv_pair1 … H) -H - #K2 #V2 #HK12 #HV12 #H destruct - lapply (lpx_sn_fwd_length … HK12) - #H @(ex3_intro … (K2.ⓑ{I}V2)) (**) (* explicit constructor *) - /3 width=1 by lpx_sn_pair, lreq_O2/ -| #I #L1 #K1 #V1 #m #_ #IHLK1 #K2 #HK12 elim (IHLK1 … HK12) -K1 - /3 width=5 by drop_drop, lreq_pair, lpx_sn_pair, ex3_intro/ -| #I #L1 #K1 #V1 #W1 #l #m #HLK1 #HWV1 #IHLK1 #X #H - elim (lpx_sn_inv_pair1 … H) -H #K2 #W2 #HK12 #HW12 #H destruct - elim (H2R … HW12 … HLK1 … HWV1) -W1 - elim (IHLK1 … HK12) -K1 - /3 width=6 by drop_skip, lreq_succ, lpx_sn_pair, ex3_intro/ -] -qed-. - -fact lpx_sn_dropable_aux: ∀R,L2,K2,s,l,m. ⬇[s, l, m] L2 ≡ K2 → ∀L1. lpx_sn R L1 L2 → - l = 0 → ∃∃K1. ⬇[s, 0, m] L1 ≡ K1 & lpx_sn R K1 K2. -#R #L2 #K2 #s #l #m #H elim H -L2 -K2 -l -m -[ #l #m #Hm #X #H >(lpx_sn_inv_atom2 … H) -H - /4 width=3 by drop_atom, lpx_sn_atom, ex2_intro/ -| #I #K2 #V2 #X #H elim (lpx_sn_inv_pair2 … H) -H - #K1 #V1 #HK12 #HV12 #H destruct - /3 width=5 by drop_pair, lpx_sn_pair, ex2_intro/ -| #I #L2 #K2 #V2 #m #_ #IHLK2 #X #H #_ elim (lpx_sn_inv_pair2 … H) -H - #L1 #V1 #HL12 #HV12 #H destruct - elim (IHLK2 … HL12) -L2 /3 width=3 by drop_drop, ex2_intro/ -| #I #L2 #K2 #V2 #W2 #l #m #_ #_ #_ #L1 #_ #H elim (ysucc_inv_O_dx … H) -] -qed-. - -lemma lpx_sn_dropable: ∀R. dropable_dx (lpx_sn R). -/2 width=5 by lpx_sn_dropable_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma index ef4419780..23eaab6ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/substitution/lpx_sn_tc.ma @@ -54,7 +54,7 @@ lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. ] qed-. -lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. #R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 @@ -65,7 +65,7 @@ lemma TC_lpx_sn_inv_pair2: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ] qed-. -lemma TC_lpx_sn_ind: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀S:relation lenv. S (⋆) (⋆) → ( ∀I,K1,K2,V1,V2. @@ -88,7 +88,7 @@ lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. ] qed-. -fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. @@ -98,12 +98,12 @@ fact TC_lpx_sn_inv_pair1_aux: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → ] qed-. -lemma TC_lpx_sn_inv_pair1: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. /2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. -lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. s_rs_transitive … R (λ_. lpx_sn R) → +lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → lpx_sn (LTC … R) L1 L2. /3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. -- 2.39.2