From 8a5a354c9ac3ef20ca01dbeb61f6b99902f172a7 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 11 Mar 2014 17:57:05 +0000 Subject: [PATCH] reaxiomatized lleq fixes a bug in it and allows to park substitution in etc --- .../basic_2/computation/cpxs_leq.ma | 24 + .../lambdadelta/basic_2/computation/fpbu.ma | 2 +- .../basic_2/computation/fpbu_fpns.ma | 1 + .../lambdadelta/basic_2/computation/fpns.ma | 2 +- .../basic_2/computation/fpns_fpns.ma | 2 +- .../basic_2/computation/lcosx_cpxs.ma | 7 +- .../basic_2/computation/lpxs_lleq.ma | 43 +- .../lambdadelta/basic_2/computation/lsx.ma | 10 +- .../basic_2/computation/lsx_ldrop.ma | 2 +- .../basic_2/computation/lsx_lpxs.ma | 20 +- .../cpx_cpys.ma => etc/lsuby/cpx_cpys.etc} | 0 .../cpxs_cpys.ma => etc/lsuby/cpxs_cpys.etc} | 0 .../{relocation/cpy.ma => etc/lsuby/cpy.etc} | 0 .../cpy_cpy.ma => etc/lsuby/cpy_cpy.etc} | 0 .../cpy_lift.ma => etc/lsuby/cpy_lift.etc} | 0 .../cpys.ma => etc/lsuby/cpys.etc} | 0 .../cpys_alt.ma => etc/lsuby/cpys_alt.etc} | 0 .../cpys_cpys.ma => etc/lsuby/cpys_cpys.etc} | 0 .../cpys_lift.ma => etc/lsuby/cpys_lift.etc} | 0 .../lsuby/extlrsubeq_4.etc} | 0 .../lsuby/lazyeqalt_4.etc} | 0 .../lleq.ma => etc/lsuby/lleq.etc} | 0 .../lleq_alt.ma => etc/lsuby/lleq_alt.etc} | 0 .../lleq_ext.ma => etc/lsuby/lleq_ext.etc} | 0 .../lleq_fqus.ma => etc/lsuby/lleq_fqus.etc} | 0 .../lsuby/lleq_ldrop.etc} | 0 .../lleq_lleq.ma => etc/lsuby/lleq_lleq.etc} | 0 .../lpx_cpys.ma => etc/lsuby/lpx_cpys.etc} | 0 .../lsuby.ma => etc/lsuby/lsuby.etc} | 0 .../lsuby/lsuby_lsuby.etc} | 0 .../psubst_6.ma => etc/lsuby/psubst_6.etc} | 0 .../lsuby/psubststar_6.etc} | 0 .../lsuby/psubststaralt_6.etc} | 0 .../lambdadelta/basic_2/reduction/cpx_leq.ma | 32 ++ .../lambdadelta/basic_2/reduction/cpx_lleq.ma | 7 +- .../lambdadelta/basic_2/reduction/lpx_lleq.ma | 4 +- .../basic_2/relocation/fqu_lleq.ma | 45 ++ .../basic_2/relocation/fquq_lleq.ma | 29 ++ .../basic_2/relocation/ldrop_leq.ma | 1 - .../lambdadelta/basic_2/relocation/lleq.ma | 3 + .../basic_2/relocation/lleq_ldrop.ma | 150 +++++++ .../basic_2/relocation/lleq_lleq.ma | 32 ++ .../basic_2/relocation/llpx_sn_ldrop.ma | 410 ++++++++++++++++++ .../basic_2/substitution/fqup_lleq.ma | 32 ++ .../basic_2/substitution/fqus_lleq.ma | 29 ++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 34 +- matita/matita/predefined_virtuals.ml | 1 + 47 files changed, 845 insertions(+), 77 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_leq.ma rename matita/matita/contribs/lambdadelta/basic_2/{reduction/cpx_cpys.ma => etc/lsuby/cpx_cpys.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{computation/cpxs_cpys.ma => etc/lsuby/cpxs_cpys.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/cpy.ma => etc/lsuby/cpy.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/cpy_cpy.ma => etc/lsuby/cpy_cpy.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/cpy_lift.ma => etc/lsuby/cpy_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpys.ma => etc/lsuby/cpys.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpys_alt.ma => etc/lsuby/cpys_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpys_cpys.ma => etc/lsuby/cpys_cpys.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/cpys_lift.ma => etc/lsuby/cpys_lift.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/extlrsubeq_4.ma => etc/lsuby/extlrsubeq_4.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/lazyeqalt_4.ma => etc/lsuby/lazyeqalt_4.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq.ma => etc/lsuby/lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_alt.ma => etc/lsuby/lleq_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_ext.ma => etc/lsuby/lleq_ext.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_fqus.ma => etc/lsuby/lleq_fqus.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_ldrop.ma => etc/lsuby/lleq_ldrop.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{substitution/lleq_lleq.ma => etc/lsuby/lleq_lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{reduction/lpx_cpys.ma => etc/lsuby/lpx_cpys.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lsuby.ma => etc/lsuby/lsuby.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lsuby_lsuby.ma => etc/lsuby/lsuby_lsuby.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubst_6.ma => etc/lsuby/psubst_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubststar_6.ma => etc/lsuby/psubststar_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/psubststaralt_6.ma => etc/lsuby/psubststaralt_6.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqup_lleq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/substitution/fqus_lleq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_leq.ma new file mode 100644 index 000000000..1d35deb53 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_leq.ma @@ -0,0 +1,24 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/reduction/cpx_leq.ma". +include "basic_2/computation/cpxs.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL COMPUTATION ON TERMS *****************) + +(* Properties on equivalence for local environments *************************) + +lemma leq_cpxs_trans: ∀h,g,G. lsub_trans … (cpxs h g G) (leq 0 (∞)). +/3 width=5 by leq_cpx_trans, LTC_lsub_trans/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma index 7165feaee..93e837f9e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredproper_8.ma". -include "basic_2/substitution/lleq.ma". +include "basic_2/relocation/lleq.ma". include "basic_2/computation/fpbs.ma". (* UNITARY "BIG TREE" PROPER PARALLEL COMPUTATION FOR CLOSURES **************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma index 9f5111ad2..863b08196 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbu_fpns.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lleq_lleq.ma". include "basic_2/computation/cpxs_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/lpxs_lpxs.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma index 6e68fef14..dce46b065 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/btpredsnstar_8.ma". -include "basic_2/substitution/lleq.ma". +include "basic_2/relocation/lleq.ma". include "basic_2/computation/lpxs.ma". (* PARALLEL COMPUTATION FOR "BIG TREE" NORMAL FORMS *************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma index 728f48df9..deaa7a967 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpns_fpns.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_lleq.ma". +include "basic_2/relocation/lleq_lleq.ma". include "basic_2/computation/lpxs_lpxs.ma". include "basic_2/computation/fpns.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma index 3ed17d258..aef5014e7 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lcosx_cpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "ground_2/ynat/ynat_max.ma". include "basic_2/computation/lsx_ldrop.ma". include "basic_2/computation/lsx_lpxs.ma". include "basic_2/computation/lcosx.ma". @@ -36,7 +37,7 @@ lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → | #a #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H elim (lsx_inv_bind … H) -H #HV1 #HT1 @lsx_bind /2 width=2 by/ (**) (* explicit constructor *) - @(lsx_leqy_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, lsuby_succ/ + @(lsx_leq_conf … (L.ⓑ{I}V1)) /3 width=1 by lcosx_pair, leq_succ/ | #I #G #L #V1 #V2 #T1 #T2 #_ #_ #IHV12 #IHT12 #d #HL #H elim (lsx_inv_flat … H) -H /3 width=1 by lsx_flat/ | #G #L #V #U1 #U2 #T2 #_ #HTU2 #IHU12 #d #HL #H @@ -50,13 +51,13 @@ lemma lsx_cpx_trans_lcosx: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡[h, g] T2 → elim (lsx_inv_flat … H) -H #HV1 #H elim (lsx_inv_bind … H) -H #HW1 #HT1 @lsx_bind /3 width=1 by lsx_flat/ (**) (* explicit constructor *) - @(lsx_leqy_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, lsuby_succ/ + @(lsx_leq_conf … (L.ⓛW1)) /3 width=1 by lcosx_pair, leq_succ/ | #a #G #L #V1 #V2 #U2 #W1 #W2 #T1 #T2 #_ #HVU2 #_ #_ #IHV12 #IHW12 #IHT12 #d #HL #H elim (lsx_inv_flat … H) -H #HV1 #H elim (lsx_inv_bind … H) -H #HW1 #HT1 @lsx_bind /2 width=1 by/ (**) (* explicit constructor *) @lsx_flat [ /3 width=7 by lsx_lift_ge, ldrop_drop/ ] - @(lsx_leqy_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, lsuby_succ/ + @(lsx_leq_conf … (L.ⓓW1)) /3 width=1 by lcosx_pair, leq_succ/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma index 2ca1e193d..e21c79912 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lpxs_lleq.ma @@ -12,8 +12,9 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lleq_leq.ma". include "basic_2/reduction/lpx_lleq.ma". -include "basic_2/computation/cpxs_cpys.ma". +include "basic_2/computation/cpxs_leq.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lpxs_cpxs.ma". @@ -37,7 +38,7 @@ lemma lpxs_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpxs_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct /2 width=4 by fqu_lref_O, ex3_intro/ | * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H [ elim (lleq_inv_bind … H) @@ -93,36 +94,32 @@ elim (fqus_inv_gen … H) -H ] qed-. -fact lsuby_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ⊑×[d, e] L0 → e = ∞ → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → - ∃∃L. L ⊑×[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +fact leq_lpxs_trans_lleq_aux: ∀h,g,G,L1,L0,d,e. L1 ≃[d, e] L0 → e = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ≃[d, e] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). #h #g #G #L1 #L0 #d #e #H elim H -L1 -L0 -d -e -[ #L1 #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H +[ #d #e #_ #L2 #H >(lpxs_inv_atom1 … H) -H /3 width=5 by ex3_intro, conj/ | #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #He destruct -| #I1 #I0 #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H +| #I #L1 #L0 #V1 #e #HL10 #IHL10 #He #Y #H elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct lapply (ysucc_inv_Y_dx … He) -He #He elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I1}V2)) /3 width=3 by lpxs_pair, lsuby_cpxs_trans, lsuby_pair/ - #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 - #H1 #H2 elim (IH T) // #HL0dx #HL0sn - @conj #H @(lleq_lsuby_repl … H) -H normalize - /3 width=1 by lsuby_sym, lsuby_pair_O_Y/ + @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, leq_cpxs_trans, leq_pair/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_pair_O_Y/ | #I1 #I0 #L1 #L0 #V1 #V0 #d #e #HL10 #IHL10 #He #Y #H elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, lsuby_succ/ - #T #H1 #H2 lapply (injective_plus_l … H1) lapply (injective_plus_l … H2) -H1 -H2 - #H1 #H2 elim (IH T) // #HL0dx #HL0sn - @conj #H @(lleq_lsuby_repl … H) -H - /3 width=1 by lsuby_sym, lsuby_succ/ normalize // + @(ex3_intro … (L.ⓑ{I1}V1)) /3 width=1 by lpxs_pair, leq_succ/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_leq_repl … H) -H /3 width=1 by leq_sym, leq_succ/ ] qed-. -lemma lsuby_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ⊑×[d, ∞] L0 → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → - ∃∃L. L ⊑×[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & - (∀T. |L1| = |L0| → |L| = |L2| → L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). -/2 width=1 by lsuby_lpxs_trans_lleq_aux/ qed-. +lemma leq_lpxs_trans_lleq: ∀h,g,G,L1,L0,d. L1 ≃[d, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, g] L2 → + ∃∃L. L ≃[d, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, g] L & + (∀T. L0 ⋕[T, d] L2 ↔ L1 ⋕[T, d] L). +/2 width=1 by leq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma index 5307af43e..59dda4e82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "basic_2/notation/relations/lazysn_6.ma". -include "basic_2/substitution/lleq.ma". +include "basic_2/relocation/lleq.ma". include "basic_2/computation/lpxs.ma". (* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) @@ -62,10 +62,10 @@ lemma lsx_gref: ∀h,g,G,L,d,p. G ⊢ ⋕⬊*[h, g, §p, d] L. /3 width=4 by lpxs_fwd_length, lleq_gref/ qed. -lemma lsx_be: ∀h,g,G,L,T,U,dt,d,e. yinj d ≤ dt → dt ≤ d + e → - ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L. -#h #g #G #L #T #U #dt #d #e #Hddt #Hdtde #HTU #H @(lsx_ind … H) -L -/5 width=7 by lsx_intro, lleq_be/ +lemma lsx_ge_up: ∀h,g,G,L,T,U,dt,d,e. dt ≤ yinj d + yinj e → + ⇧[d, e] T ≡ U → G ⊢ ⋕⬊*[h, g, U, dt] L → G ⊢ ⋕⬊*[h, g, U, d] L. +#h #g #G #L #T #U #dt #d #e #Hdtde #HTU #H @(lsx_ind … H) -L +/5 width=7 by lsx_intro, lleq_ge_up/ qed-. (* Basic forward lemmas *****************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma index 61466ca35..9bd29a5f1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_ldrop.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ldrop.ma". +include "basic_2/relocation/lleq_ldrop.ma". include "basic_2/computation/lpxs_ldrop.ma". include "basic_2/computation/lsx.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma index b3cb36781..9762de28b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/lsx_lpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/relocation/lleq_lleq.ma". include "basic_2/computation/lpxs_lleq.ma". include "basic_2/computation/lpxs_lpxs.ma". include "basic_2/computation/lsx.ma". @@ -20,15 +21,12 @@ include "basic_2/computation/lsx.ma". (* Advanced properties ******************************************************) -lemma lsx_leqy_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → - ∀L2. L1 ⊑×[d, ∞] L2 → |L1| = |L2| → G ⊢ ⋕⬊*[h, g, T, d] L2. +lemma lsx_leq_conf: ∀h,g,G,L1,T,d. G ⊢ ⋕⬊*[h, g, T, d] L1 → + ∀L2. L1 ≃[d, ∞] L2 → G ⊢ ⋕⬊*[h, g, T, d] L2. #h #g #G #L1 #T #d #H @(lsx_ind … H) -L1 -#L1 #_ #IHL1 #L2 #H1L12 #H2L12 @lsx_intro -#L3 #H1L23 #HnL23 lapply (lpxs_fwd_length … H1L23) -#H2L23 elim (lsuby_lpxs_trans_lleq … H1L12 … H1L23) -H1L12 -H1L23 -#L0 #H1L03 #H1L10 #H lapply (lpxs_fwd_length … H1L10) -#H2L10 elim (H T) -H // -#_ #H @(IHL1 … H1L10) -IHL1 -H1L10 /3 width=1 by/ +#L1 #_ #IHL1 #L2 #HL12 @lsx_intro +#L3 #HL23 #HnL23 elim (leq_lpxs_trans_lleq … HL12 … HL23) -HL12 -HL23 +#L0 #HL03 #HL10 #H elim (H T) -H /4 width=4 by/ qed-. lemma lsx_ge: ∀h,g,G,L,T,d1,d2. d1 ≤ d2 → @@ -113,10 +111,10 @@ lemma lsx_fwd_bind_dx: ∀h,g,a,I,G,L,V,T,d. G ⊢ ⋕⬊*[h, g, ⓑ{a,I}V.T, d] #L1 #_ #IHL1 @lsx_intro #Y #H #HT elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL12 #_ #H destruct -@(lsx_leqy_conf … (L2.ⓑ{I}V1)) /2 width=1 by lsuby_succ/ +@(lsx_leq_conf … (L2.ⓑ{I}V1)) /2 width=1 by leq_succ/ @IHL1 // #H @HT -IHL1 -HL12 -HT -@(lleq_lsuby_trans … (L2.ⓑ{I}V1)) -/2 width=2 by lleq_fwd_bind_dx, lsuby_succ/ +@(lleq_leq_trans … (L2.ⓑ{I}V1)) +/2 width=2 by lleq_fwd_bind_dx, leq_succ/ qed-. (* Advanced inversion lemmas ************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpx_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_cpys.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpx_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpxs_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/computation/cpxs_cpys.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpxs_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/cpy.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_cpy.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_cpy.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_cpy.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/cpy_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpy_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpys.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_cpys.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_lift.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/cpys_lift.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/cpys_lift.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/extlrsubeq_4.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/extlrsubeq_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/extlrsubeq_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lazyeqalt_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqalt_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lazyeqalt_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ext.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ext.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ext.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_fqus.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_fqus.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ldrop.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_ldrop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_ldrop.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/substitution/lleq_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lleq_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lpx_cpys.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_cpys.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lpx_cpys.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby_lsuby.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lsuby_lsuby.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/lsuby_lsuby.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubst_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubst_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubst_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststar_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststar_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststar_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststaralt_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/psubststaralt_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/lsuby/psubststaralt_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma new file mode 100644 index 000000000..7d86e027d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_leq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/ldrop_leq.ma". +include "basic_2/reduction/cpx.ma". + +(* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) + +(* Properties on equivalence for local environments *************************) + +lemma leq_cpx_trans: ∀h,g,G. lsub_trans … (cpx h g G) (leq 0 (∞)). +#h #g #G #L1 #T1 #T2 #H elim H -G -L1 -T1 -T2 +[ // +| /2 width=2 by cpx_sort/ +| #I #G #L1 #K1 #V1 #V2 #W2 #i #HLK1 #_ #HVW2 #IHV12 #L2 #HL12 + elim (leq_ldrop_trans_be … HL12 … HLK1) // -HL12 -HLK1 /3 width=7 by cpx_delta/ +|4,9: /4 width=1 by cpx_bind, cpx_beta, leq_pair_O_Y/ +|5,7,8: /3 width=1 by cpx_flat, cpx_tau, cpx_ti/ +|6,10: /4 width=3 by cpx_zeta, cpx_theta, leq_pair_O_Y/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma index 6ff6c39d0..ae6ddac78 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/cpx_lleq.ma @@ -12,7 +12,8 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ext.ma". +include "basic_2/relocation/lleq_leq.ma". +include "basic_2/relocation/lleq_ldrop.ma". include "basic_2/reduction/cpx.ma". (* CONTEXT-SENSITIVE EXTENDED PARALLEL REDUCTION FOR TERMS ******************) @@ -49,8 +50,8 @@ lemma lleq_cpx_conf_dx: ∀h,g,G,L2,T1,T2. ⦃G, L2⦄ ⊢ T1 ➡[h, g] T2 → #h #g #G #L2 #T1 #T2 #H elim H -G -L2 -T1 -T2 [ // | /3 width=3 by lleq_fwd_length, lleq_sort/ -| #I2 #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H - #I1 #K1 #HLK1 #HV1 +| #I #G #L2 #K2 #V1 #V2 #W2 #i #HLK2 #_ #HVW2 #IHV12 #L1 #H elim (lleq_inv_lref_ge_dx … H … HLK2) // -H + #K1 #HLK1 #HV1 lapply (ldrop_fwd_drop2 … HLK1) -HLK1 #HLK1 lapply (ldrop_fwd_drop2 … HLK2) -HLK2 #HLK2 @(lleq_lift_le … HLK1 HLK2 … HVW2) -HLK1 -HLK2 -HVW2 /2 width=1 by/ (**) (* full auto too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma index 9daa44656..353f810c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/lpx_lleq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/substitution/lleq_ext.ma". +include "basic_2/relocation/lleq_ldrop.ma". include "basic_2/reduction/lpx_ldrop.ma". (* SN EXTENDED PARALLEL REDUCTION FOR LOCAL ENVIRONMENTS ********************) @@ -51,7 +51,7 @@ lemma lpx_lleq_fqu_trans: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, [ #I #G1 #L1 #V1 #X #H1 #H2 elim (lpx_inv_pair2 … H1) -H1 #K0 #V0 #H1KL1 #_ #H destruct elim (lleq_inv_lref_ge_dx … H2 ? I L1 V1) -H2 // - #I1 #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct + #K1 #H #H2KL1 lapply (ldrop_inv_O2 … H) -H #H destruct /2 width=4 by fqu_lref_O, ex3_intro/ | * [ #a ] #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H [ elim (lleq_inv_bind … H) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma new file mode 100644 index 000000000..b4235ba93 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu_lleq.ma @@ -0,0 +1,45 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lleq_ldrop.ma". +include "basic_2/relocation/fqu.ma". + +(* SUPCLOSURE ***************************************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H elim H -G1 -G2 -L2 -K2 -T -U +[ #I #G #L2 #V #L1 #H elim (lleq_inv_lref_ge_dx … H … I L2 V) -H // + #K1 #H1 #H2 lapply (ldrop_inv_O2 … H1) -H1 + #H destruct /2 width=3 by fqu_lref_O, ex2_intro/ +| * [ #a ] #I #G #L2 #V #T #L1 #H + [ elim (lleq_inv_bind … H) + | elim (lleq_inv_flat … H) + ] -H + /2 width=3 by fqu_pair_sn, ex2_intro/ +| #a #I #G #L2 #V #T #L1 #H elim (lleq_inv_bind_O … H) -H + #H3 #H4 /2 width=3 by fqu_bind_dx, ex2_intro/ +| #I #G #L2 #V #T #L1 #H elim (lleq_inv_flat … H) -H + /2 width=3 by fqu_flat_dx, ex2_intro/ +| #G #L2 #K2 #T #U #e #HLK2 #HTU #L1 #HL12 + elim (ldrop_O1_le (e+1) L1) + [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ + | lapply (ldrop_fwd_length_le2 … HLK2) -K2 + lapply (lleq_fwd_length … HL12) -T -U // + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma new file mode 100644 index 000000000..880c387e4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fquq_lleq.ma @@ -0,0 +1,29 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/fqu_lleq.ma". +include "basic_2/relocation/fquq_alt.ma". + +(* OPTIONAL SUPCLOSURE ******************************************************) + +(* Properties on lazy equivalence for local environments ********************) + +lemma lleq_fquq_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊃⸮ ⦃G2, K2, U⦄ → + ∀L1. L1 ⋕[T, 0] L2 → + ∃∃K1. ⦃G1, L1, T⦄ ⊃⸮ ⦃G2, K1, U⦄ & K1 ⋕[U, 0] K2. +#G1 #G2 #L2 #K2 #T #U #H #L1 #HL12 elim(fquq_inv_gen … H) -H +[ #H elim (lleq_fqu_trans … H … HL12) -L2 /3 width=3 by fqu_fquq, ex2_intro/ +| * #HG #HL #HT destruct /2 width=3 by ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma index 1355827f7..cdca16bb5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/ldrop_leq.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/ynat/ynat_plus.ma". include "basic_2/grammar/leq_leq.ma". include "basic_2/relocation/ldrop.ma". diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma index 7a9ec530e..b431e0d18 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma @@ -25,6 +25,9 @@ interpretation "lazy equivalence (local environment)" 'LazyEq T d L1 L2 = (lleq d T L1 L2). +definition lleq_transitive: predicate (relation3 lenv term term) ≝ + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ⋕[T1, 0] L2 → R L1 T1 T2. + (* Basic inversion lemmas ***************************************************) lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma new file mode 100644 index 000000000..299412217 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_ldrop.ma @@ -0,0 +1,150 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/llpx_sn_ldrop.ma". +include "basic_2/relocation/lleq.ma". + +(* LAZY EQUIVALENCE FOR LOCAL ENVIRONMENTS **********************************) + +(* Advanced properties ******************************************************) + +lemma lleq_bind_repl_O: ∀I,L1,L2,V,T. L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → + ∀J,W. L1 ⋕[W, 0] L2 → L1.ⓑ{J}W ⋕[T, 0] L2.ⓑ{J}W. +/2 width=7 by llpx_sn_bind_repl_O/ qed-. + +lemma lleq_dec: ∀T,L1,L2,d. Decidable (L1 ⋕[T, d] L2). +/3 width=1 by llpx_sn_dec, eq_term_dec/ qed-. + +lemma lleq_llpx_sn_trans: ∀R. lleq_transitive R → + ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L. llpx_sn R d T L2 L → llpx_sn R d T L1 L. +#R #HR #L1 #L2 #T #d #H @(lleq_ind … H) -L1 -L2 -T -d +[1,2,5: /4 width=6 by llpx_sn_fwd_length, llpx_sn_gref, llpx_sn_skip, llpx_sn_sort, trans_eq/ +|4: /4 width=6 by llpx_sn_fwd_length, llpx_sn_free, le_repl_sn_conf_aux, trans_eq/ +| #I #L1 #L2 #K1 #K2 #V #d #i #Hdi #HLK1 #HLK2 #HK12 #IHK12 #L #H elim (llpx_sn_inv_lref_ge_sn … H … HLK2) -H -HLK2 + /3 width=11 by llpx_sn_lref/ +| #a #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #L #H elim (llpx_sn_inv_bind … H) -H + /3 width=1 by llpx_sn_bind/ +| #I #L1 #L2 #V #T #d #_ #_ #IHV #IHT #L #H elim (llpx_sn_inv_flat … H) -H + /3 width=1 by llpx_sn_flat/ +] +qed-. + +lemma lleq_llpx_sn_conf: ∀R. lleq_transitive R → + ∀L1,L2,T,d. L1 ⋕[T, d] L2 → + ∀L. llpx_sn R d T L1 L → llpx_sn R d T L2 L. +/3 width=3 by lleq_llpx_sn_trans, lleq_sym/ qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma lleq_inv_lref_ge_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → + ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V → + ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2. +#L1 #L2 #d #i #H #Hdi #I #K2 #V #HLK2 elim (llpx_sn_inv_lref_ge_dx … H … HLK2) -L2 +/2 width=3 by ex2_intro/ +qed-. + +lemma lleq_inv_lref_ge_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → + ∀I,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → + ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[V, 0] K2. +#L1 #L2 #d #i #H #Hdi #I1 #K1 #V #HLK1 elim (llpx_sn_inv_lref_ge_sn … H … HLK1) -L1 +/2 width=3 by ex2_intro/ +qed-. + +lemma lleq_inv_lref_ge_bi: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → + ∀I1,I2,K1,K2,V1,V2. + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & K1 ⋕[V1, 0] K2 & V1 = V2. +/2 width=8 by llpx_sn_inv_lref_ge_bi/ qed-. + +lemma lleq_inv_lref_ge: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → d ≤ i → + ∀I,K1,K2,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → ⇩[i] L2 ≡ K2.ⓑ{I}V → + K1 ⋕[V, 0] K2. +#L1 #L2 #d #i #HL12 #Hdi #I #K1 #K2 #V #HLK1 #HLK2 +elim (lleq_inv_lref_ge_bi … HL12 … HLK1 HLK2) // +qed-. + +lemma lleq_inv_S: ∀L1,L2,T,d. L1 ⋕[T, d+1] L2 → + ∀I,K1,K2,V. ⇩[d] L1 ≡ K1.ⓑ{I}V → ⇩[d] L2 ≡ K2.ⓑ{I}V → + K1 ⋕[V, 0] K2 → L1 ⋕[T, d] L2. +/2 width=9 by llpx_sn_inv_S/ qed-. + +lemma lleq_inv_bind_O: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → + L1 ⋕[V, 0] L2 ∧ L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +/2 width=2 by llpx_sn_inv_bind_O/ qed-. + +(* Advanced forward lemmas **************************************************) + +lemma lleq_fwd_lref_dx: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → + ∀I,K2,V. ⇩[i] L2 ≡ K2.ⓑ{I}V → + i < d ∨ + ∃∃K1. ⇩[i] L1 ≡ K1.ⓑ{I}V & K1 ⋕[V, 0] K2 & d ≤ i. +#L1 #L2 #d #i #H #I #K2 #V #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2 +[ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/ +qed-. + +lemma lleq_fwd_lref_sn: ∀L1,L2,d,i. L1 ⋕[#i, d] L2 → + ∀I,K1,V. ⇩[i] L1 ≡ K1.ⓑ{I}V → + i < d ∨ + ∃∃K2. ⇩[i] L2 ≡ K2.ⓑ{I}V & K1 ⋕[V, 0] K2 & d ≤ i. +#L1 #L2 #d #i #H #I #K1 #V #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1 +[ | * ] /3 width=3 by ex3_intro, or_intror, or_introl/ +qed-. + +lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ⋕[ⓑ{a,I}V.T, 0] L2 → + L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V. +/2 width=2 by llpx_sn_fwd_bind_O_dx/ qed-. + +(* Properties on relocation *************************************************) + +lemma lleq_lift_le: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → dt ≤ d → L1 ⋕[U, dt] L2. +/3 width=10 by llpx_sn_lift_le, lift_mono/ qed-. + +lemma lleq_lift_ge: ∀K1,K2,T,dt. K1 ⋕[T, dt] K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d ≤ dt → L1 ⋕[U, dt+e] L2. +/2 width=9 by llpx_sn_lift_ge/ qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma lleq_inv_lift_le: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → dt ≤ d → K1 ⋕[T, dt] K2. +/3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-. + +lemma lleq_inv_lift_be: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ dt → dt ≤ yinj d + e → K1 ⋕[T, d] K2. +/2 width=11 by llpx_sn_inv_lift_be/ qed-. + +lemma lleq_inv_lift_ge: ∀L1,L2,U,dt. L1 ⋕[U, dt] L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ dt → K1 ⋕[T, dt-e] K2. +/2 width=9 by llpx_sn_inv_lift_ge/ qed-. + +(* Inversion lemmas on negated lazy quivalence for local environments *******) + +lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,d. (L1 ⋕[ⓑ{a,I}V.T, d] L2 → ⊥) → + (L1 ⋕[V, d] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, ⫯d] L2.ⓑ{I}V → ⊥). +/3 width=2 by nllpx_sn_inv_bind, eq_term_dec/ qed-. + +lemma nlleq_inv_flat: ∀I,L1,L2,V,T,d. (L1 ⋕[ⓕ{I}V.T, d] L2 → ⊥) → + (L1 ⋕[V, d] L2 → ⊥) ∨ (L1 ⋕[T, d] L2 → ⊥). +/3 width=2 by nllpx_sn_inv_flat, eq_term_dec/ qed-. + +lemma nlleq_inv_bind_O: ∀a,I,L1,L2,V,T. (L1 ⋕[ⓑ{a,I}V.T, 0] L2 → ⊥) → + (L1 ⋕[V, 0] L2 → ⊥) ∨ (L1.ⓑ{I}V ⋕[T, 0] L2.ⓑ{I}V → ⊥). +/3 width=2 by nllpx_sn_inv_bind_O, eq_term_dec/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma new file mode 100644 index 000000000..a99b1e2f3 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma @@ -0,0 +1,32 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/lleq_ldrop.ma". + +(* Main properties **********************************************************) + +theorem lleq_trans: ∀d,T. Transitive … (lleq d T). +/2 width=3 by lleq_llpx_sn_trans/ qed-. + +theorem lleq_canc_sn: ∀L,L1,L2,T,d. L ⋕[d, T] L1→ L ⋕[d, T] L2 → L1 ⋕[d, T] L2. +/3 width=3 by lleq_trans, lleq_sym/ qed-. + +theorem lleq_canc_dx: ∀L1,L2,L,T,d. L1 ⋕[d, T] L → L2 ⋕[d, T] L → L1 ⋕[d, T] L2. +/3 width=3 by lleq_trans, lleq_sym/ qed-. + +(* Note: lleq_nlleq_trans: ∀d,T,L1,L. L1⋕[T, d] L → + ∀L2. (L ⋕[T, d] L2 → ⊥) → (L1 ⋕[T, d] L2 → ⊥). +/3 width=3 by lleq_canc_sn/ qed-. +works with /4 width=8/ so lleq_canc_sn is more convenient +*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma new file mode 100644 index 000000000..4d90e2332 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_ldrop.ma @@ -0,0 +1,410 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) + +include "basic_2/relocation/ldrop_ldrop.ma". +include "basic_2/relocation/llpx_sn_leq.ma". + +(* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Advanced forward lemmas **************************************************) + +lemma llpx_sn_fwd_lref_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → + ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → + i < d ∨ + ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & llpx_sn R 0 V1 K1 K2 & + R K1 V1 V2 & d ≤ i. +#R #L1 #L2 #d #i #H #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref … H) -H [ * || * ] +[ #_ #H elim (lt_refl_false i) + lapply (ldrop_fwd_length_lt2 … HLK2) -HLK2 + /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) +| /2 width=1 by or_introl/ +| #I #K11 #K22 #V11 #V22 #HLK11 #HLK22 #HK12 #HV12 #Hdi + lapply (ldrop_mono … HLK22 … HLK2) -L2 #H destruct + /3 width=5 by ex4_2_intro, or_intror/ +] +qed-. + +lemma llpx_sn_fwd_lref_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → + ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → + i < d ∨ + ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & llpx_sn R 0 V1 K1 K2 & + R K1 V1 V2 & d ≤ i. +#R #L1 #L2 #d #i #H #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref … H) -H [ * || * ] +[ #H #_ elim (lt_refl_false i) + lapply (ldrop_fwd_length_lt2 … HLK1) -HLK1 + /2 width=3 by lt_to_le_to_lt/ (**) (* full auto too slow *) +| /2 width=1 by or_introl/ +| #I #K11 #K22 #V11 #V22 #HLK11 #HLK22 #HK12 #HV12 #Hdi + lapply (ldrop_mono … HLK11 … HLK1) -L1 #H destruct + /3 width=5 by ex4_2_intro, or_intror/ +] +qed-. + +(* Advanced inversion lemmas ************************************************) + +lemma llpx_sn_inv_lref_ge_dx: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → + ∀I,K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 → + ∃∃K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 & + llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. +#R #L1 #L2 #d #i #H #Hdi #I #K2 #V2 #HLK2 elim (llpx_sn_fwd_lref_dx … H … HLK2) -L2 +[ #H elim (ylt_yle_false … H Hdi) +| * /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma llpx_sn_inv_lref_ge_sn: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → + ∀I,K1,V1. ⇩[i] L1 ≡ K1.ⓑ{I}V1 → + ∃∃K2,V2. ⇩[i] L2 ≡ K2.ⓑ{I}V2 & + llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. +#R #L1 #L2 #d #i #H #Hdi #I #K1 #V1 #HLK1 elim (llpx_sn_fwd_lref_sn … H … HLK1) -L1 +[ #H elim (ylt_yle_false … H Hdi) +| * /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma llpx_sn_inv_lref_ge_bi: ∀R,L1,L2,d,i. llpx_sn R d (#i) L1 L2 → d ≤ i → + ∀I1,I2,K1,K2,V1,V2. + ⇩[i] L1 ≡ K1.ⓑ{I1}V1 → ⇩[i] L2 ≡ K2.ⓑ{I2}V2 → + ∧∧ I1 = I2 & llpx_sn R 0 V1 K1 K2 & R K1 V1 V2. +#R #L1 #L2 #d #i #HL12 #Hdi #I1 #I2 #K1 #K2 #V1 #V2 #HLK1 #HLK2 +elim (llpx_sn_inv_lref_ge_sn … HL12 … HLK1) // -L1 -d +#J #Y #HY lapply (ldrop_mono … HY … HLK2) -L2 -i #H destruct /2 width=1 by and3_intro/ +qed-. + +fact llpx_sn_inv_S_aux: ∀R,L1,L2,T,d0. llpx_sn R d0 T L1 L2 → ∀d. d0 = d + 1 → + ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 → + llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2. +#R #L1 #L2 #T #d0 #H elim H -L1 -L2 -T -d0 +/2 width=1 by llpx_sn_gref, llpx_sn_free, llpx_sn_sort/ +[ #L1 #L2 #d0 #i #HL12 #Hid #d #H #K1 #K2 #I #V1 #V2 #HLK1 #HLK2 #HK12 #HV12 destruct + elim (yle_split_eq i d) /2 width=1 by llpx_sn_skip, ylt_fwd_succ2/ -HL12 -Hid + #H destruct /2 width=9 by llpx_sn_lref/ +| #I #L1 #L2 #K11 #K22 #V1 #V2 #d0 #i #Hd0i #HLK11 #HLK22 #HK12 #HV12 #_ #d #H #K1 #K2 #J #W1 #W2 #_ #_ #_ #_ destruct + /3 width=9 by llpx_sn_lref, yle_pred_sn/ +| #a #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W1 #W2 #HLK1 #HLK2 #HK12 #HW12 destruct + /4 width=9 by llpx_sn_bind, ldrop_drop/ +| #I #L1 #L2 #V #T #d0 #_ #_ #IHV #IHT #d #H #K1 #K2 #J #W1 #W2 #HLK1 #HLK2 #HK12 #HW12 destruct + /3 width=9 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_inv_S: ∀R,L1,L2,T,d. llpx_sn R (d + 1) T L1 L2 → + ∀K1,K2,I,V1,V2. ⇩[d] L1 ≡ K1.ⓑ{I}V1 → ⇩[d] L2 ≡ K2.ⓑ{I}V2 → + llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R d T L1 L2. +/2 width=9 by llpx_sn_inv_S_aux/ qed-. + +lemma llpx_sn_inv_bind_O: ∀R. (∀L. reflexive … (R L)) → + ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → + llpx_sn R 0 V L1 L2 ∧ llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind … H) -H +/3 width=9 by ldrop_pair, conj, llpx_sn_inv_S/ +qed-. + +(* More advanced forward lemmas *********************************************) + +lemma llpx_sn_fwd_bind_O_dx: ∀R. (∀L. reflexive … (R L)) → + ∀a,I,L1,L2,V,T. llpx_sn R 0 (ⓑ{a,I}V.T) L1 L2 → + llpx_sn R 0 T (L1.ⓑ{I}V) (L2.ⓑ{I}V). +#R #HR #a #I #L1 #L2 #V #T #H elim (llpx_sn_inv_bind_O … H) -H // +qed-. + +(* Advanced properties ******************************************************) + +lemma llpx_sn_bind_repl_O: ∀R,I,L1,L2,V1,V2,T. llpx_sn R 0 T (L1.ⓑ{I}V1) (L2.ⓑ{I}V2) → + ∀J,W1,W2. llpx_sn R 0 W1 L1 L2 → R L1 W1 W2 → llpx_sn R 0 T (L1.ⓑ{J}W1) (L2.ⓑ{J}W2). +/3 width=9 by llpx_sn_bind_repl_SO, llpx_sn_inv_S/ qed-. + +lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → + ∀T,L1,L2,d. Decidable (llpx_sn R d T L1 L2). +#R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T +#n #IH #L1 * * +[ #k #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/ +| #i #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) + [ #HL12 #d elim (ylt_split i d) /3 width=1 by llpx_sn_skip, or_introl/ + #Hdi elim (lt_or_ge i (|L1|)) #HiL1 + elim (lt_or_ge i (|L2|)) #HiL2 /3 width=1 by or_introl, llpx_sn_free/ + elim (ldrop_O1_lt … HiL2) #I2 #K2 #V2 #HLK2 + elim (ldrop_O1_lt … HiL1) #I1 #K1 #V1 #HLK1 + elim (eq_bind2_dec I2 I1) + [ #H2 elim (HR K1 V1 V2) -HR + [ #H3 elim (IH K1 V1 … K2 0) destruct + /3 width=9 by llpx_sn_lref, ldrop_fwd_rfw, or_introl/ + ] + ] + -IH #H3 @or_intror + #H elim (llpx_sn_fwd_lref … H) -H [1,3,4,6,7,9: * ] + [1,3,5: /3 width=4 by lt_to_le_to_lt, lt_refl_false/ + |7,8,9: /2 width=4 by ylt_yle_false/ + ] + #Z #Y1 #Y2 #X1 #X2 #HLY1 #HLY2 #HY12 #HX12 + lapply (ldrop_mono … HLY1 … HLK1) -HLY1 -HLK1 + lapply (ldrop_mono … HLY2 … HLK2) -HLY2 -HLK2 + #H #H0 destruct /2 width=1 by/ + ] +| #p #Hn #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_gref/ +| #a #I #V #T #Hn #L2 #d destruct + elim (IH L1 V … L2 d) /2 width=1 by/ + elim (IH (L1.ⓑ{I}V) T … (L2.ⓑ{I}V) (⫯d)) -IH /3 width=1 by or_introl, llpx_sn_bind/ + #H1 #H2 @or_intror + #H elim (llpx_sn_inv_bind … H) -H /2 width=1 by/ +| #I #V #T #Hn #L2 #d destruct + elim (IH L1 V … L2 d) /2 width=1 by/ + elim (IH L1 T … L2 d) -IH /3 width=1 by or_introl, llpx_sn_flat/ + #H1 #H2 @or_intror + #H elim (llpx_sn_inv_flat … H) -H /2 width=1 by/ +] +-n /4 width=4 by llpx_sn_fwd_length, or_intror/ +qed-. + +(* Properties on relocation *************************************************) + +lemma llpx_sn_lift_le: ∀R. l_liftable R → + ∀K1,K2,T,d0. llpx_sn R d0 T K1 K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 U L1 L2. +#R #HR #K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0 +[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_sort/ +| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct + [ lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_skip/ + | elim (ylt_yle_false … Hid0) -L1 -L2 -K1 -K2 -e -Hid0 + /3 width=3 by yle_trans, yle_inj/ + ] +| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hdi #H destruct [ -HK12 | -IHK12 ] + [ elim (ldrop_trans_lt … HLK1 … HK11) // -K1 + elim (ldrop_trans_lt … HLK2 … HK22) // -Hdi -K2 + /3 width=18 by llpx_sn_lref/ + | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hdi -Hd0 -K2 + /3 width=9 by llpx_sn_lref, yle_plus_dx1_trans/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d -e + /2 width=1 by llpx_sn_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_lift_ge: ∀R,K1,K2,T,d0. llpx_sn R d0 T K1 K2 → + ∀L1,L2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀U. ⇧[d, e] T ≡ U → d ≤ d0 → llpx_sn R (d0+e) U L1 L2. +#R #K1 #K2 #T #d0 #H elim H -K1 -K2 -T -d0 +[ #K1 #K2 #d0 #k #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_sort/ +| #K1 #K2 #d0 #i #HK12 #Hid0 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 + [ /3 width=3 by llpx_sn_skip, ylt_plus_dx2_trans/ + | /3 width=3 by llpx_sn_skip, monotonic_ylt_plus_dx/ + ] +| #I #K1 #K2 #K11 #K22 #V1 #V2 #d0 #i #Hid0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -e -Hid0 + /3 width=3 by ylt_yle_trans, ylt_inj/ + | lapply (ldrop_trans_ge_comm … HLK1 … HK11 ?) // -K1 + lapply (ldrop_trans_ge_comm … HLK2 … HK22 ?) // -Hid -Hd0 -K2 + /3 width=9 by llpx_sn_lref, monotonic_yle_plus_dx/ + ] +| #K1 #K2 #d0 #i #HK1 #HK2 #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref1 … H) -H + * #Hid #H destruct + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 + [ /3 width=7 by llpx_sn_free, ldrop_fwd_be/ + | lapply (ldrop_fwd_length … HLK1) -HLK1 #HLK1 + lapply (ldrop_fwd_length … HLK2) -HLK2 #HLK2 + @llpx_sn_free [ >HLK1 | >HLK2 ] -Hid -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) + ] +| #K1 #K2 #d0 #p #HK12 #L1 #L2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (ldrop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -d + /2 width=1 by llpx_sn_gref/ +| #a #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind1 … H) -H + #W #U #HVW #HTU #H destruct /4 width=5 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #K1 #K2 #V #T #d0 #_ #_ #IHV #IHT #L1 #L2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat1 … H) -H + #W #U #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/ +] +qed-. + +(* Inversion lemmas on relocation *******************************************) + +lemma llpx_sn_inv_lift_le: ∀R. l_deliftable_sn R → + ∀L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d0 ≤ d → llpx_sn R d0 T K1 K2. +#R #HR #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + [ /2 width=1 by llpx_sn_skip/ + | /3 width=3 by llpx_sn_skip, yle_ylt_trans/ + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -HK12 | -IHK12 ] + [ elim (ldrop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V1 #HKL1 #HKL11 #HVW1 + elim (ldrop_conf_lt … HLK2 … HLK22) // -Hid -L2 #L2 #V2 #HKL2 #HKL22 #HVW2 + elim (HR … HW12 … HKL11 … HVW1) -HR #V0 #HV0 #HV12 + lapply (lift_inj … HV0 … HVW2) -HV0 -HVW2 #H destruct + /3 width=10 by llpx_sn_lref/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 + elim (le_inv_plus_l … Hid) -Hid /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *) + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d -e + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, ldrop_skip, yle_succ/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → d ≤ d0 → d0 ≤ yinj d + e → llpx_sn R d T K1 K2. +#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + -Hid0 /3 width=1 by llpx_sn_skip, ylt_inj/ + | elim (ylt_yle_false … Hid0) -L1 -L2 -Hd0 -Hid0 + /3 width=3 by yle_trans, yle_inj/ (**) (* slow *) + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hd0e -Hid0 + /3 width=3 by ylt_yle_trans, ylt_inj/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hid0 -Hd0 -Hd0e + elim (le_inv_plus_l … Hid) -Hid /3 width=9 by llpx_sn_lref, yle_inj/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d0 -e + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_bind2 … H) -H + >commutative_plus #V #T #HVW #HTU #H destruct + @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) + @(IHU … HTU) -IHU -HTU /2 width=1 by ldrop_skip, yle_succ/ +| #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hd0 #Hd0e elim (lift_inv_flat2 … H) -H + #V #T #HVW #HTU #H destruct /3 width=6 by llpx_sn_flat/ +] +qed-. + +lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,d0. llpx_sn R d0 U L1 L2 → + ∀K1,K2,d,e. ⇩[Ⓕ, d, e] L1 ≡ K1 → ⇩[Ⓕ, d, e] L2 ≡ K2 → + ∀T. ⇧[d, e] T ≡ U → yinj d + e ≤ d0 → llpx_sn R (d0-e) T K1 K2. +#R #L1 #L2 #U #d0 #H elim H -L1 -L2 -U -d0 +[ #L1 #L2 #d0 #k #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #d0 #i #HL12 #Hid0 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct [ -Hid0 | -Hded0 ] + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 + [ /4 width=3 by llpx_sn_skip, yle_plus_to_minus_inj2, ylt_yle_trans, ylt_inj/ + | elim (le_inv_plus_l … Hid) -Hid #_ + /4 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx, yle_inj/ + ] +| #I #L1 #L2 #K11 #K22 #W1 #W2 #d0 #i #Hid0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #Hid #H destruct + [ elim (ylt_yle_false … Hid0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hid0 + /3 width=3 by yle_fwd_plus_sn1, ylt_yle_trans, ylt_inj/ + | lapply (ldrop_conf_ge … HLK1 … HLK11 ?) // -L1 + lapply (ldrop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hded0 -Hid + /3 width=9 by llpx_sn_lref, monotonic_yle_minus_dx/ + ] +| #L1 #L2 #d0 #i #HL1 #HL2 #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_lref2 … H) -H + * #_ #H destruct + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) + [ lapply (ldrop_fwd_length_le4 … HLK1) -HLK1 + lapply (ldrop_fwd_length_le4 … HLK2) -HLK2 + #HKL2 #HKL1 #HK12 @llpx_sn_free // /2 width=3 by transitive_le/ (**) (* full auto too slow *) + | lapply (ldrop_fwd_length … HLK1) -HLK1 #H >H in HL1; -H + lapply (ldrop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H + /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ + ] +| #L1 #L2 #d0 #p #HL12 #K1 #K2 #d #e #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (ldrop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -d + /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #d0 #_ #_ #IHW #IHU #K1 #K2 #d #e #HLK1 #HLK2 #X #H #Hded0 elim (lift_inv_bind2 … H) -H + #V #T #HVW #HTU #H destruct + @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) + "; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; ["≥"; "⪀"; "≽"; "⪴"; "⥸"; "⊒"; ]; + ["∨"; "⩖"; "⋓"; ] ; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; -- 2.39.2