From 9b8d36ee041582f876543086e7659ed9e365e861 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 10 Mar 2016 21:12:43 +0000 Subject: [PATCH] partial commit in the relocation component to move some files ... --- .../{relocation => computation}/fqup.ma | 4 +- .../{relocation => computation}/fqup_fqup.ma | 0 .../{relocation => computation}/fqus.ma | 2 +- .../{relocation => computation}/fqus_alt.ma | 0 .../{relocation => computation}/fqus_fqus.ma | 0 .../basic_2/etc_new/drops/drops.etc | 35 ++--- .../lleq.ma => etc_new/lleq/lleq.etc} | 8 +- .../lleq_alt.ma => etc_new/lleq/lleq_alt.etc} | 0 .../lleq/lleq_alt_rec.etc} | 0 .../lleq/lleq_drop.etc} | 20 +-- .../lleq/lleq_fqus.etc} | 4 +- .../lleq/lleq_lleq.etc} | 0 .../lleq/lleq_llor.etc} | 4 +- .../lleq/lleq_lreq.etc} | 0 .../llpx_sn/llpx_sn.etc} | 24 ++-- .../llpx_sn/llpx_sn_alt.etc} | 2 +- .../llpx_sn/llpx_sn_alt_rec.etc} | 6 +- .../llpx_sn/llpx_sn_drop.etc} | 126 +++++++++--------- .../llpx_sn/llpx_sn_frees.etc} | 4 +- .../llpx_sn/llpx_sn_llor.etc} | 0 .../llpx_sn/llpx_sn_lpx_sn.etc} | 0 .../llpx_sn/llpx_sn_lreq.etc} | 0 .../llpx_sn/llpx_sn_tc.etc} | 0 .../basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc | 48 ------- .../basic_2/etc_new/lreq/lreq_lreq.etc | 4 +- .../lambdadelta/basic_2/relocation/drops.ma | 28 ++-- .../basic_2/relocation/drops_drops.ma | 10 +- .../{drop_lreq.ma => drops_lreq.ma} | 62 ++++----- .../basic_2/relocation/drops_lstar.ma | 8 +- .../basic_2/relocation/drops_weight.ma | 2 +- .../lambdadelta/basic_2/relocation/frees.ma | 97 +++++++++++--- .../lambdadelta/basic_2/relocation/lexs.ma | 43 ++++-- .../{lpx_sn_drops.ma => lexs_drops.ma} | 34 ++--- .../basic_2/relocation/lexs_lexs.ma | 93 +++++++++++++ .../lambdadelta/basic_2/relocation/lifts.ma | 14 +- .../basic_2/relocation/lifts_lifts.ma | 4 +- .../lambdadelta/basic_2/relocation/lreq.ma | 6 +- 37 files changed, 409 insertions(+), 283 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => computation}/fqup.ma (96%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => computation}/fqup_fqup.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => computation}/fqus.ma (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => computation}/fqus_alt.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation => computation}/fqus_fqus.ma (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq.ma => etc_new/lleq/lleq.etc} (96%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_alt.ma => etc_new/lleq/lleq_alt.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_alt_rec.ma => etc_new/lleq/lleq_alt_rec.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_drop.ma => etc_new/lleq/lleq_drop.etc} (88%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_fqus.ma => etc_new/lleq/lleq_fqus.etc} (97%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_lleq.ma => etc_new/lleq/lleq_lleq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_llor.ma => etc_new/lleq/lleq_llor.etc} (94%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/lleq_lreq.ma => etc_new/lleq/lleq_lreq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn.ma => etc_new/llpx_sn/llpx_sn.etc} (94%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_alt.ma => etc_new/llpx_sn/llpx_sn_alt.etc} (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_alt_rec.ma => etc_new/llpx_sn/llpx_sn_alt_rec.etc} (98%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_drop.ma => etc_new/llpx_sn/llpx_sn_drop.etc} (81%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_frees.ma => etc_new/llpx_sn/llpx_sn_frees.etc} (94%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_llor.ma => etc_new/llpx_sn/llpx_sn_llor.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_lpx_sn.ma => etc_new/llpx_sn/llpx_sn_lpx_sn.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_lreq.ma => etc_new/llpx_sn/llpx_sn_lreq.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{relocation/llpx_sn_tc.ma => etc_new/llpx_sn/llpx_sn_tc.etc} (100%) delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc_new/lpx_sn/lpx_sn_lpx_sn.etc rename matita/matita/contribs/lambdadelta/basic_2/relocation/{drop_lreq.ma => drops_lreq.ma} (67%) rename matita/matita/contribs/lambdadelta/basic_2/relocation/{lpx_sn_drops.ma => lexs_drops.ma} (75%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fqup.ma similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqup.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fqup.ma index b126081ba..3ac1a812d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fqup.ma @@ -37,9 +37,9 @@ lemma fqup_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄. /2 width=5 by tri_TC_strap/ qed. -lemma fqup_drop: ∀G1,G2,L1,K1,K2,T1,T2,U1,m. ⬇[m] L1 ≡ K1 → ⬆[0, m] T1 ≡ U1 → +lemma fqup_drop: ∀G1,G2,L1,K1,K2,T1,T2,U1,k. ⬇[k] L1 ≡ K1 → ⬆[0, k] T1 ≡ U1 → ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ → ⦃G1, L1, U1⦄ ⊐+ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #m #HLK1 #HTU1 #HT12 elim (eq_or_gt … m) #H destruct +#G1 #G2 #L1 #K1 #K2 #T1 #T2 #U1 #k #HLK1 #HTU1 #HT12 elim (eq_or_gt … k) #H destruct [ >(drop_inv_O2 … HLK1) -L1 <(lift_inv_O2 … HTU1) -U1 // | /3 width=5 by fqup_strap2, fqu_drop_lt/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqup_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fqup_fqup.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqup_fqup.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fqup_fqup.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fqus.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fqus.ma index 92679770e..0a2061220 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fqus.ma @@ -56,7 +56,7 @@ lemma fqus_strap2: ∀G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G, L, /2 width=5 by tri_TC_strap/ qed-. lemma fqus_drop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ → - ∀L1,U1,m. ⬇[m] L1 ≡ K1 → ⬆[0, m] T1 ≡ U1 → + ∀L1,U1,k. ⬇[k] L1 ≡ K1 → ⬆[0, k] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊐* ⦃G2, K2, T2⦄. #G1 #G2 #K1 #K2 #T1 #T2 #H @(fqus_ind … H) -G2 -K2 -T2 /3 width=5 by fqus_strap1, fquq_fqus, fquq_drop/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fqus_alt.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fqus_alt.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fqus_fqus.ma similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/fqus_fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/computation/fqus_fqus.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc index 7e53292ef..795f620cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/drops/drops.etc @@ -1,12 +1,3 @@ -lemma drop_refl_atom_O2: ∀s,l. ⬇[s, l, O] ⋆ ≡ ⋆. -/2 width=1 by drop_atom/ qed. - -(* Basic_1: was by definition: drop_refl *) -lemma drop_refl: ∀L,l,s. ⬇[s, l, 0] L ≡ L. -#L elim L -L // -#L #I #V #IHL #l #s @(nat_ind_plus … l) -l /2 width=1 by drop_pair, drop_skip/ -qed. - lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2 → ∃∃L. ⬇[s, l, m2 - m1] L1 ≡ L & ⬇[s, l, m1] L ≡ L2. #L1 #L2 #l #m2 #s #H elim H -L1 -L2 -l -m2 @@ -32,20 +23,22 @@ lemma drop_split: ∀L1,L2,l,m2,s. ⬇[s, l, m2] L1 ≡ L2 → ∀m1. m1 ≤ m2 qed-. (* Basic_2A1: includes: drop_split *) -lemma drops_split_trans: ∀L1,L2,t. ⬇*[t] L1 ≡ L2 → ∀t1,t2. t1 ⊚ t2 ≡ t → - ∃∃L. ⬇*[t1] L1 ≡ L & ⬇*[t2] L ≡ L2. -#L1 #L2 #t #H elim H -L1 -L2 -t -[ #t1 #t2 #H elim (after_inv_empty3 … H) -H - /2 width=3 by ex2_intro, drops_atom/ -| #I #L1 #L2 #V #t #HL12 #IHL12 #t1 #t2 #H elim (after_inv_false3 … H) -H * - [ #tl1 #tl2 #H1 #H2 #Ht destruct elim (IHL12 … Ht) -t - #tl #H1 #H2 - | #tl1 #H #Ht destruct elim (IHL12 … Ht) -t +lemma drops_split_trans: ∀L1,L2,f,c. ⬇*[c, f] L1 ≡ L2 → ∀f1,f2. f1 ⊚ f2 ≡ f → + ∃∃L. ⬇*[c, f1] L1 ≡ L & ⬇*[c, f2] L ≡ L2. +#L1 #L2 #f #c #H elim H -L1 -L2 -f +[ #f #Hc #f1 #f2 #Hf @(ex2_intro … (⋆)) @drops_atom + #H lapply (Hc H) -c + #H elim (after_inv_isid3 … Hf H) -f // +| #I #L1 #L2 #V #f #HL12 #IHL12 #f1 #f2 #Hf elim (after_inv_xxS … Hf) -Hf * + [ #g1 #g2 #Hf #H1 #H2 destruct elim (IHL12 … Hf) -f + #L #HL1 #HL2 @(ex2_intro … (L.ⓑ{I}V)) /2 width=1 by drops_drop/ + @drops_skip // + | #g1 #Hf #H destruct elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_drop/ ] -| #I #L1 #L2 #V1 #V2 #t #_ #HV21 #IHL12 #t1 #t2 #H elim (after_inv_true3 … H) -H - #tl1 #tl2 #H1 #H2 #Ht destruct elim (lifts_split_trans … HV21 … Ht) -HV21 - elim (IHL12 … Ht) -t /3 width=5 by ex2_intro, drops_skip/ +| #I #L1 #L2 #V1 #V2 #f #_ #HV21 #IHL12 #f1 #f2 #Hf elim (after_inv_xxO … Hf) -Hf + #g1 #g2 #Hf #H1 #H2 destruct elim (lifts_split_trans … HV21 … Hf) -HV21 + elim (IHL12 … Hf) -f /3 width=5 by ex2_intro, drops_skip/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc similarity index 96% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc index 1f57f73be..521ad356d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq.etc @@ -31,7 +31,7 @@ definition lleq_transitive: predicate (relation3 lenv term term) ≝ (* Basic inversion lemmas ***************************************************) lemma lleq_ind: ∀R:relation4 ynat term lenv lenv. ( - ∀L1,L2,l,k. |L1| = |L2| → R l (⋆k) L1 L2 + ∀L1,L2,l,s. |L1| = |L2| → R l (⋆s) L1 L2 ) → ( ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → R l (#i) L1 L2 ) → ( @@ -104,7 +104,7 @@ lemma lleq_fwd_flat_dx: ∀I,L1,L2,V,T,l. (* Basic properties *********************************************************) -lemma lleq_sort: ∀L1,L2,l,k. |L1| = |L2| → L1 ≡[⋆k, l] L2. +lemma lleq_sort: ∀L1,L2,l,s. |L1| = |L2| → L1 ≡[⋆s, l] L2. /2 width=1 by llpx_sn_sort/ qed. lemma lleq_skip: ∀L1,L2,l,i. yinj i < l → |L1| = |L2| → L1 ≡[#i, l] L2. @@ -142,8 +142,8 @@ lemma lleq_sym: ∀l,T. symmetric … (lleq l T). qed-. lemma lleq_ge_up: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀T,l,m. ⬆[l, m] T ≡ U → - lt ≤ l + m → L1 ≡[U, l] L2. + ∀T,l,k. ⬆[l, k] T ≡ U → + lt ≤ l + k → L1 ≡[U, l] L2. /2 width=6 by llpx_sn_ge_up/ qed-. lemma lleq_ge: ∀L1,L2,T,l1. L1 ≡[T, l1] L2 → ∀l2. l1 ≤ l2 → L1 ≡[T, l2] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt_rec.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_alt_rec.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_alt_rec.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_drop.etc similarity index 88% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_drop.etc index 09ee8a495..aa4fa9e8c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_drop.etc @@ -109,30 +109,30 @@ lemma lleq_fwd_bind_O_dx: ∀a,I,L1,L2,V,T. L1 ≡[ⓑ{a,I}V.T, 0] L2 → (* Properties on relocation *************************************************) lemma lleq_lift_le: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 → - ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀U. ⬆[l, m] T ≡ U → lt ≤ l → L1 ≡[U, lt] L2. + ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀U. ⬆[l, k] T ≡ U → lt ≤ l → L1 ≡[U, lt] L2. /3 width=10 by llpx_sn_lift_le, lift_mono/ qed-. lemma lleq_lift_ge: ∀K1,K2,T,lt. K1 ≡[T, lt] K2 → - ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀U. ⬆[l, m] T ≡ U → l ≤ lt → L1 ≡[U, lt+m] L2. + ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀U. ⬆[l, k] T ≡ U → l ≤ lt → L1 ≡[U, lt+k] L2. /2 width=9 by llpx_sn_lift_ge/ qed-. (* Inversion lemmas on relocation *******************************************) lemma lleq_inv_lift_le: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → lt ≤ l → K1 ≡[T, lt] K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → lt ≤ l → K1 ≡[T, lt] K2. /3 width=10 by llpx_sn_inv_lift_le, ex2_intro/ qed-. lemma lleq_inv_lift_be: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l ≤ lt → lt ≤ l + m → K1 ≡[T, l] K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → l ≤ lt → lt ≤ l + k → K1 ≡[T, l] K2. /2 width=11 by llpx_sn_inv_lift_be/ qed-. lemma lleq_inv_lift_ge: ∀L1,L2,U,lt. L1 ≡[U, lt] L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l + m ≤ lt → K1 ≡[T, lt-m] K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → l + k ≤ lt → K1 ≡[T, lt-k] K2. /2 width=9 by llpx_sn_inv_lift_ge/ qed-. (* Inversion lemmas on negated lazy quivalence for local environments *******) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_fqus.etc similarity index 97% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_fqus.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_fqus.etc index 28bb175ed..bf0cec6d2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_fqus.etc @@ -35,8 +35,8 @@ lemma lleq_fqu_trans: ∀G1,G2,L2,K2,T,U. ⦃G1, L2, T⦄ ⊐ ⦃G2, K2, U⦄ #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 #m #HLK2 #HTU #L1 #HL12 - elim (drop_O1_le (Ⓕ) (m+1) L1) +| #G #L2 #K2 #T #U #k #HLK2 #HTU #L1 #HL12 + elim (drop_O1_le (Ⓕ) (k+1) L1) [ /3 width=12 by fqu_drop, lleq_inv_lift_le, ex2_intro/ | lapply (drop_fwd_length_le2 … HLK2) -K2 lapply (lleq_fwd_length … HL12) -T -U // diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_llor.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_llor.etc similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_llor.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_llor.etc index 06893aad6..e702043ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_llor.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_llor.etc @@ -20,7 +20,7 @@ include "basic_2/multiple/lleq_alt.ma". (* Properties on pointwise union for local environments **********************) -lemma llpx_sn_llor_dx: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → +lemma llpx_sn_llor_dx: ∀R. (c_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → ∀L1,L2,T,l. llpx_sn R l T L1 L2 → ∀L. L1 ⋓[T, l] L2 ≡ L → L2 ≡[T, l] L. #R #H1R #H2R #L1 #L2 #T #l #H1 #L #H2 lapply (llpx_sn_frees_trans … H1R H2R … H1) -H1R -H2R #HR @@ -36,6 +36,6 @@ elim (IH2 … HLK1 HLK2 HLK) -IH2 -HLK1 -HLK2 -HLK * /2 width=1 by conj/ #H ] qed. -lemma llpx_sn_llor_dx_sym: ∀R. (s_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → +lemma llpx_sn_llor_dx_sym: ∀R. (c_r_confluent1 … R (llpx_sn R 0)) → (frees_trans R) → ∀L1,L2,T,l. llpx_sn R l T L1 L2 → ∀L. L1 ⋓[T, l] L2 ≡ L → L ≡[T, l] L2. /3 width=6 by llpx_sn_llor_dx, lleq_sym/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lreq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lleq_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/lleq/lleq_lreq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc similarity index 94% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc index cf6e4ad76..ffe9501f6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn.etc @@ -18,7 +18,7 @@ include "basic_2/substitution/drop.ma". (* LAZY SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) inductive llpx_sn (R:relation3 lenv term term): relation4 ynat term lenv lenv ≝ -| llpx_sn_sort: ∀L1,L2,l,k. |L1| = |L2| → llpx_sn R l (⋆k) L1 L2 +| llpx_sn_sort: ∀L1,L2,l,s. |L1| = |L2| → llpx_sn R l (⋆s) L1 L2 | llpx_sn_skip: ∀L1,L2,l,i. |L1| = |L2| → yinj i < l → llpx_sn R l (#i) L1 L2 | llpx_sn_lref: ∀I,L1,L2,K1,K2,V1,V2,l,i. l ≤ yinj i → ⬇[i] L1 ≡ K1.ⓑ{I}V1 → ⬇[i] L2 ≡ K2.ⓑ{I}V2 → @@ -38,7 +38,7 @@ fact llpx_sn_inv_bind_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → ∀a,I,V,T. X = ⓑ{a,I}V.T → llpx_sn R l V L1 L2 ∧ llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V). #R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #k #_ #b #J #W #U #H destruct +[ #L1 #L2 #l #s #_ #b #J #W #U #H destruct | #L1 #L2 #l #i #_ #_ #b #J #W #U #H destruct | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #b #J #W #U #H destruct | #L1 #L2 #l #i #_ #_ #_ #b #J #W #U #H destruct @@ -56,7 +56,7 @@ fact llpx_sn_inv_flat_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → ∀I,V,T. X = ⓕ{I}V.T → llpx_sn R l V L1 L2 ∧ llpx_sn R l T L1 L2. #R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #k #_ #J #W #U #H destruct +[ #L1 #L2 #l #s #_ #J #W #U #H destruct | #L1 #L2 #l #i #_ #_ #J #W #U #H destruct | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #_ #_ #_ #_ #_ #J #W #U #H destruct | #L1 #L2 #l #i #_ #_ #_ #J #W #U #H destruct @@ -100,7 +100,7 @@ fact llpx_sn_fwd_lref_aux: ∀R,L1,L2,X,l. llpx_sn R l X L1 L2 → ∀i. X = #i llpx_sn R (yinj 0) V1 K1 K2 & R K1 V1 V2 & l ≤ yinj i. #R #L1 #L2 #X #l * -L1 -L2 -X -l -[ #L1 #L2 #l #k #_ #j #H destruct +[ #L1 #L2 #l #s #_ #j #H destruct | #L1 #L2 #l #i #_ #Hil #j #H destruct /2 width=1 by or3_intro1/ | #I #L1 #L2 #K1 #K2 #V1 #V2 #l #i #Hli #HLK1 #HLK2 #HK12 #HV12 #j #H destruct /3 width=9 by or3_intro2, ex5_5_intro/ @@ -163,15 +163,15 @@ lemma llpx_sn_Y: ∀R,T,L1,L2. |L1| = |L2| → llpx_sn R (∞) T L1 L2. @IH -IH // normalize /2 width=1 by eq_f2/ qed-. -lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,m. ⬆[l, m] T ≡ U → - lt ≤ l + m → llpx_sn R l U L1 L2. +lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,k. ⬆[l, k] T ≡ U → + lt ≤ l + k → llpx_sn R l U L1 L2. #R #L1 #L2 #U #lt #H elim H -L1 -L2 -U -lt -[ #L1 #L2 #lt #k #HL12 #X #l #m #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #lt #i #HL12 #Hilt #X #l #m #H #Hltlm +[ #L1 #L2 #lt #s #HL12 #X #l #k #H #_ >(lift_inv_sort2 … H) -H /2 width=1 by llpx_sn_sort/ +| #L1 #L2 #lt #i #HL12 #Hilt #X #l #k #H #Hltlm elim (lift_inv_lref2 … H) -H * #Hil #H destruct /3 width=1 by llpx_sn_skip, ylt_inj/ -HL12 elim (ylt_yle_false … Hilt) -Hilt @(yle_trans … Hltlm) /2 width=1 by yle_inj/ (**) (* full auto too slow 11s *) -| #I #L1 #L2 #K1 #K2 #W1 #W2 #lt #i #Hlti #HLK1 #HLK2 #HW1 #HW12 #_ #X #l #m #H #_ +| #I #L1 #L2 #K1 #K2 #W1 #W2 #lt #i #Hlti #HLK1 #HLK2 #HW1 #HW12 #_ #X #l #k #H #_ elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ lapply (llpx_sn_fwd_length … HW1) -HW1 #HK12 lapply (drop_fwd_length … HLK1) lapply (drop_fwd_length … HLK2) @@ -179,12 +179,12 @@ lemma llpx_sn_ge_up: ∀R,L1,L2,U,lt. llpx_sn R lt U L1 L2 → ∀T,l,m. ⬆[l, | /3 width=9 by llpx_sn_lref, yle_fwd_plus_sn1/ ] | /2 width=1 by llpx_sn_free/ -| #L1 #L2 #lt #p #HL12 #X #l #m #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct +| #L1 #L2 #lt #p #HL12 #X #l #k #H #_ >(lift_inv_gref2 … H) -H /2 width=1 by llpx_sn_gref/ +| #a #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct @(llpx_sn_bind) /2 width=4 by/ (**) (* full auto fails *) @(IHT … HTU) /2 width=1 by yle_succ/ -| #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #m #H #Hltlm destruct +| #I #L1 #L2 #W #U #lt #_ #_ #IHV #IHT #X #l #k #H #Hltlm destruct elim (lift_inv_flat2 … H) -H #HVW #HTU #H destruct /3 width=4 by llpx_sn_flat/ ] diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt.etc similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt.etc index f40046c5f..ac0d12224 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt.etc @@ -54,7 +54,7 @@ lapply (drop_fwd_drop2 … HLK1) #H1 lapply (drop_fwd_drop2 … HLK2) -HLK2 #H2 @conj [ @(drop_fwd_length_eq1 … H1 H2) // ] -HL12 #Z1 #Z2 #Y1 #Y2 #X1 #X2 #j #_ ->(minus_plus_m_m j (i+1)) in ⊢ (%→?); >commutative_plus (minus_plus_k_k j (i+1)) in ⊢ (%→?); >commutative_plus yminus_SO2 #HnV1 #HKY1 #HKY2 (**) (* full auto too slow *) lapply (drop_trans_ge … H1 … HKY1 ?) -H1 -HKY1 // #HLY1 diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt_rec.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt_rec.etc similarity index 98% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt_rec.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt_rec.etc index 870a4bbef..172ccf38a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_alt_rec.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_alt_rec.etc @@ -114,9 +114,9 @@ qed-. (* Basic properties *********************************************************) -lemma llpx_sn_alt_r_sort: ∀R,L1,L2,l,k. |L1| = |L2| → llpx_sn_alt_r R l (⋆k) L1 L2. -#R #L1 #L2 #l #k #HL12 @llpx_sn_alt_r_intro_alt // -HL12 -#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆k)) // +lemma llpx_sn_alt_r_sort: ∀R,L1,L2,l,s. |L1| = |L2| → llpx_sn_alt_r R l (⋆s) L1 L2. +#R #L1 #L2 #l #s #HL12 @llpx_sn_alt_r_intro_alt // -HL12 +#I1 #I2 #K1 #K2 #V1 #V2 #i #_ #H elim (H (⋆s)) // qed. lemma llpx_sn_alt_r_gref: ∀R,L1,L2,l,p. |L1| = |L2| → llpx_sn_alt_r R l (§p) L1 L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_drop.ma b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc similarity index 81% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_drop.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc index 21e9536aa..02e70f4fd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/llpx_sn_drop.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/llpx_sn/llpx_sn_drop.etc @@ -129,7 +129,7 @@ lemma llpx_sn_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀T,L1,L2,l. Decidable (llpx_sn R l T L1 L2). #R #HR #T #L1 @(f2_ind … rfw … L1 T) -L1 -T #x #IH #L1 * * -[ #k #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/ +[ #s #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) /3 width=1 by or_introl, llpx_sn_sort/ | #i #Hx #L2 elim (eq_nat_dec (|L1|) (|L2|)) [ #HL12 #l elim (ylt_split i l) /3 width=1 by llpx_sn_skip, or_introl/ #Hli elim (lt_or_ge i (|L1|)) #HiL1 @@ -171,20 +171,20 @@ qed-. lemma llpx_sn_lift_le: ∀R. d_liftable R → ∀K1,K2,T,l0. llpx_sn R l0 T K1 K2 → - ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀U. ⬆[l, m] T ≡ U → l0 ≤ l → llpx_sn R l0 U L1 L2. + ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀U. ⬆[l, k] T ≡ U → l0 ≤ l → llpx_sn R l0 U L1 L2. #R #HR #K1 #K2 #T #l0 #H elim H -K1 -K2 -T -l0 -[ #K1 #K2 #l0 #k #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X +[ #K1 #K2 #l0 #s #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l /2 width=1 by llpx_sn_sort/ -| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H +| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H * #Hli #H destruct [ lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l /2 width=1 by llpx_sn_skip/ - | elim (ylt_yle_false … Hil0) -L1 -L2 -K1 -K2 -m -Hil0 + | elim (ylt_yle_false … Hil0) -L1 -L2 -K1 -K2 -k -Hil0 /3 width=3 by yle_trans, yle_inj/ ] -| #I #K1 #K2 #K11 #K22 #V1 #V2 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H +| #I #K1 #K2 #K11 #K22 #V1 #V2 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #IHK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H * #Hli #H destruct [ -HK12 | -IHK12 ] [ elim (drop_trans_lt … HLK1 … HK11) // -K1 elim (drop_trans_lt … HLK2 … HK22) // -Hli -K2 @@ -193,7 +193,7 @@ lemma llpx_sn_lift_le: ∀R. d_liftable R → lapply (drop_trans_ge_comm … HLK2 … HK22 ?) // -Hli -Hl0 -K2 /3 width=9 by llpx_sn_lref, yle_plus_dx1_trans/ ] -| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H +| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H * #Hil #H destruct lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 [ /3 width=7 by llpx_sn_free, drop_fwd_be/ @@ -201,38 +201,38 @@ lemma llpx_sn_lift_le: ∀R. d_liftable R → lapply (drop_fwd_length … HLK2) -HLK2 #HLK2 @llpx_sn_free [ >HLK1 | >HLK2 ] -Hil -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) ] -| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X - lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l -m +| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X + lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l -k /2 width=1 by llpx_sn_gref/ -| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H +| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat1 … H) -H +| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 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,l0. llpx_sn R l0 T K1 K2 → - ∀L1,L2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀U. ⬆[l, m] T ≡ U → l ≤ l0 → llpx_sn R (l0+m) U L1 L2. + ∀L1,L2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀U. ⬆[l, k] T ≡ U → l ≤ l0 → llpx_sn R (l0+k) U L1 L2. #R #K1 #K2 #T #l0 #H elim H -K1 -K2 -T -l0 -[ #K1 #K2 #l0 #k #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X +[ #K1 #K2 #l0 #s #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort1 … H) -X lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l /2 width=1 by llpx_sn_sort/ -| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H +| #K1 #K2 #l0 #i #HK12 #Hil0 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref1 … H) -H * #_ #H destruct lapply (drop_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 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H +| #I #K1 #K2 #K11 #K22 #V1 #V2 #l0 #i #Hil0 #HK11 #HK22 #HK12 #HV12 #_ #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H * #Hil #H destruct - [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -m -Hil0 + [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K1 -K2 -K11 -K22 -V1 -V2 -k -Hil0 /3 width=3 by ylt_yle_trans, ylt_inj/ | lapply (drop_trans_ge_comm … HLK1 … HK11 ?) // -K1 lapply (drop_trans_ge_comm … HLK2 … HK22 ?) // -Hil -Hl0 -K2 /3 width=9 by llpx_sn_lref, monotonic_yle_plus_dx/ ] -| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H +| #K1 #K2 #l0 #i #HK1 #HK2 #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref1 … H) -H * #Hil #H destruct lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -HK12 [ /3 width=7 by llpx_sn_free, drop_fwd_be/ @@ -240,12 +240,12 @@ lemma llpx_sn_lift_ge: ∀R,K1,K2,T,l0. llpx_sn R l0 T K1 K2 → lapply (drop_fwd_length … HLK2) -HLK2 #HLK2 @llpx_sn_free [ >HLK1 | >HLK2 ] -Hil -HLK1 -HLK2 /2 width=1 by monotonic_le_plus_r/ (**) (* explicit constructor *) ] -| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X +| #K1 #K2 #l0 #p #HK12 #L1 #L2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref1 … H) -X lapply (drop_fwd_length_eq2 … HLK1 HLK2 HK12) -K1 -K2 -l /2 width=1 by llpx_sn_gref/ -| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H +| #a #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind1 … H) -H #W #U #HVW #HTU #H destruct /4 width=5 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat1 … H) -H +| #I #K1 #K2 #V #T #l0 #_ #_ #IHV #IHT #L1 #L2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat1 … H) -H #W #U #HVW #HTU #H destruct /3 width=5 by llpx_sn_flat/ ] qed-. @@ -254,19 +254,19 @@ qed-. lemma llpx_sn_inv_lift_le: ∀R. d_deliftable_sn R → ∀L1,L2,U,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l0 ≤ l → llpx_sn R l0 T K1 K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → l0 ≤ l → llpx_sn R l0 T K1 K2. #R #HR #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -m +[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X + lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -k /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ elim (lift_inv_lref2 … H) -H * #_ #H destruct lapply (drop_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 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H +| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #IHK12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -HK12 | -IHK12 ] [ elim (drop_conf_lt … HLK1 … HLK11) // -L1 #L1 #V1 #HKL1 #HKL11 #HVW1 elim (drop_conf_lt … HLK2 … HLK22) // -Hil -L2 #L2 #V2 #HKL2 #HKL22 #HVW2 @@ -277,7 +277,7 @@ lemma llpx_sn_inv_lift_le: ∀R. d_deliftable_sn R → lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 elim (yle_inv_plus_inj2 … Hil) -Hil /4 width=9 by llpx_sn_lref, yle_trans, yle_inj/ (**) (* slow *) ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_lref2 … H) -H * #_ #H destruct lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 @@ -287,39 +287,39 @@ lemma llpx_sn_inv_lift_le: ∀R. d_deliftable_sn R → lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -m +| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X + lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l -k /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind2 … H) -H +| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct /4 width=6 by llpx_sn_bind, drop_skip, yle_succ/ -| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 elim (lift_inv_flat2 … H) -H +| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 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,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l ≤ l0 → l0 ≤ l + m → llpx_sn R l T K1 K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → l ≤ l0 → l0 ≤ l + k → llpx_sn R l T K1 K2. #R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m +[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_sort2 … H) -X + lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -k /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -Hil0 /3 width=1 by llpx_sn_skip, ylt_inj/ | elim (ylt_yle_false … Hil0) -L1 -L2 -Hl0 -Hil0 /3 width=3 by yle_trans, yle_inj/ (**) (* slow *) ] -| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_lref2 … H) -H +| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H * #Hil #H destruct - [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hl0m -Hil0 + [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hl0k -Hil0 /3 width=3 by ylt_yle_trans, ylt_inj/ | lapply (drop_conf_ge … HLK1 … HLK11 ?) // -L1 - lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 -Hl0 -Hl0m + lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hil0 -Hl0 -Hl0k elim (yle_inv_plus_inj2 … Hil) -Hil /3 width=9 by llpx_sn_lref, yle_inj/ ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_lref2 … H) -H * #_ #H destruct lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 @@ -329,33 +329,33 @@ lemma llpx_sn_inv_lift_be: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X - lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -m +| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ #_ >(lift_inv_gref2 … H) -X + lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l0 -k /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_bind2 … H) -H +| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) @(IHU … HTU) -IHU -HTU /2 width=1 by drop_skip, yle_succ/ -| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hl0 #Hl0m elim (lift_inv_flat2 … H) -H +| #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hl0 #Hl0k 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,l0. llpx_sn R l0 U L1 L2 → - ∀K1,K2,l,m. ⬇[Ⓕ, l, m] L1 ≡ K1 → ⬇[Ⓕ, l, m] L2 ≡ K2 → - ∀T. ⬆[l, m] T ≡ U → l + m ≤ l0 → llpx_sn R (l0-m) T K1 K2. + ∀K1,K2,l,k. ⬇[Ⓕ, l, k] L1 ≡ K1 → ⬇[Ⓕ, l, k] L2 ≡ K2 → + ∀T. ⬆[l, k] T ≡ U → l + k ≤ l0 → llpx_sn R (l0-k) T K1 K2. #R #L1 #L2 #U #l0 #H elim H -L1 -L2 -U -l0 -[ #L1 #L2 #l0 #k #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X +[ #L1 #L2 #l0 #s #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_sort2 … H) -X lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l /2 width=1 by llpx_sn_sort/ -| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL12 #Hil0 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ -Hil0 | -Hlml0 ] lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 [ /4 width=3 by llpx_sn_skip, yle_plus1_to_minus_inj2, ylt_yle_trans, ylt_inj/ | elim (yle_inv_plus_inj2 … Hil) -Hil /3 width=1 by llpx_sn_skip, monotonic_ylt_minus_dx/ ] -| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H +| #I #L1 #L2 #K11 #K22 #W1 #W2 #l0 #i #Hil0 #HLK11 #HLK22 #HK12 #HW12 #_ #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H * #Hil #H destruct [ elim (ylt_yle_false … Hil0) -I -L1 -L2 -K11 -K22 -W1 -W2 -Hil0 /3 width=3 by yle_fwd_plus_sn1, ylt_yle_trans, ylt_inj/ @@ -363,7 +363,7 @@ lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → lapply (drop_conf_ge … HLK2 … HLK22 ?) // -L2 -Hlml0 -Hil /3 width=9 by llpx_sn_lref, monotonic_yle_minus_dx/ ] -| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H +| #L1 #L2 #l0 #i #HL1 #HL2 #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_lref2 … H) -H * #_ #H destruct lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) [ lapply (drop_fwd_length_le4 … HLK1) -HLK1 @@ -373,15 +373,15 @@ lemma llpx_sn_inv_lift_ge: ∀R,L1,L2,U,l0. llpx_sn R l0 U L1 L2 → lapply (drop_fwd_length … HLK2) -HLK2 #H >H in HL2; -H /3 width=1 by llpx_sn_free, le_plus_to_minus_r/ ] -| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #m #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X +| #L1 #L2 #l0 #p #HL12 #K1 #K2 #l #k #HLK1 #HLK2 #X #H #_ >(lift_inv_gref2 … H) -X lapply (drop_fwd_length_eq1 … HLK1 HLK2 HL12) -L1 -L2 -l /2 width=1 by llpx_sn_gref/ -| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #m #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_bind2 … H) -H +| #a #I #L1 #L2 #W #U #l0 #_ #_ #IHW #IHU #K1 #K2 #l #k #HLK1 #HLK2 #X #H #Hlml0 elim (lift_inv_bind2 … H) -H #V #T #HVW #HTU #H destruct @llpx_sn_bind [ /2 width=5 by/ ] -IHW (**) (* explicit constructor *) (lpx_sn_inv_atom1 … H1) -X1 - >(lpx_sn_inv_atom1 … H2) -X2 /2 width=3 by lpx_sn_atom, ex2_intro/ -| #L0 #I #V0 #Hx #X1 #H1 #X2 #H2 destruct - elim (lpx_sn_inv_pair1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct - elim (lpx_sn_inv_pair1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct - elim (IH … HL01 … HL02) -IH /2 width=2 by ylt_succ2_refl/ #L #HL1 #HL2 - elim (HR12 … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lpx_sn_pair, ex2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc index 20d6c0002..3cb7451ec 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc_new/lreq/lreq_lreq.etc @@ -19,8 +19,8 @@ include "basic_2/grammar/lreq.ma". (* Main properties **********************************************************) -theorem lreq_trans: ∀l,m. Transitive … (lreq l m). -#l #m #L1 #L2 #H elim H -L1 -L2 -l -m +theorem lreq_trans: ∀f. Transitive … (lreq f). +#f #L1 #L2 #H elim H -L1 -L2 -l -m [ #l #m #X #H lapply (lreq_inv_atom1 … H) -H #H destruct // | #I1 #I #L1 #L #V1 #V #_ #IHL1 #X #H elim (lreq_inv_zero1 … H) -H diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index a38d5c7a5..27281ee17 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -48,9 +48,9 @@ definition d_deliftable2_sn: predicate (lenv → relation term) ≝ ∃∃T2. ⬆*[f] T2 ≡ U2 & R K T1 T2. definition dropable_sn: predicate (rtmap → relation lenv) ≝ - λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,u2. R u2 L1 L2 → - ∀u1. f ⊚ u1 ≡ u2 → - ∃∃K2. R u1 K1 K2 & ⬇*[c, f] L2 ≡ K2. + λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀L2,f2. R f2 L1 L2 → + ∀f1. f ⊚ f1 ≡ f2 → + ∃∃K2. R f1 K1 K2 & ⬇*[c, f] L2 ≡ K2. (* Basic inversion lemmas ***************************************************) @@ -117,18 +117,18 @@ lemma drops_inv_skip2: ∀I,X,K2,V2,c,f. ⬇*[c, ↑f] X ≡ K2.ⓑ{I}V2 → (* Basic properties *********************************************************) -lemma drops_eq_repl_back: ∀L1,L2,c. eq_stream_repl_back … (λf. ⬇*[c, f] L1 ≡ L2). +lemma drops_eq_repl_back: ∀L1,L2,c. eq_repl_back … (λf. ⬇*[c, f] L1 ≡ L2). #L1 #L2 #c #f1 #H elim H -L1 -L2 -f1 [ /4 width=3 by drops_atom, isid_eq_repl_back/ -| #I #L1 #L2 #V #f1 #_ #IH #f2 #H elim (next_inv_sn … H) -H - /3 width=1 by drops_drop/ -| #I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H elim (push_inv_sn … H) -H +| #I #L1 #L2 #V #f1 #_ #IH #f2 #H elim (eq_inv_nx … H) -H + /3 width=3 by drops_drop/ +| #I #L1 #L2 #V1 #v2 #f1 #_ #HV #IH #f2 #H elim (eq_inv_px … H) -H /3 width=3 by drops_skip, lifts_eq_repl_back/ ] qed-. -lemma drops_eq_repl_fwd: ∀L1,L2,c. eq_stream_repl_fwd … (λf. ⬇*[c, f] L1 ≡ L2). -#L1 #L2 #c @eq_stream_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) +lemma drops_eq_repl_fwd: ∀L1,L2,c. eq_repl_fwd … (λf. ⬇*[c, f] L1 ≡ L2). +#L1 #L2 #c @eq_repl_sym /2 width=3 by drops_eq_repl_back/ (**) (* full auto fails *) qed-. (* Basic_2A1: includes: drop_refl *) @@ -163,7 +163,7 @@ fact drops_fwd_drop2_aux: ∀X,Y,c,f2. ⬇*[c, f2] X ≡ Y → ∀I,K,V. Y = K. | #I #L1 #L2 #V #f2 #_ #IHL #J #K #W #H elim (IHL … H) -IHL /3 width=7 by after_next, ex3_2_intro, drops_drop/ | #I #L1 #L2 #V1 #V2 #f2 #HL #_ #_ #J #K #W #H destruct - lapply (isid_after_dx 𝐈𝐝 f2 ?) /3 width=9 by after_push, ex3_2_intro, drops_drop/ + lapply (isid_after_dx 𝐈𝐝 … f2) /3 width=9 by after_push, ex3_2_intro, drops_drop/ ] qed-. @@ -176,16 +176,16 @@ lemma drops_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → lemma drops_after_fwd_drop2: ∀I,X,K,V,c,f2. ⬇*[c, f2] X ≡ K.ⓑ{I}V → ∀f1,f. 𝐈⦃f1⦄ → f2 ⊚ ⫯f1 ≡ f → ⬇*[c, f] X ≡ K. #I #X #K #V #c #f2 #H #f1 #f #Hf1 #Hf elim (drops_fwd_drop2 … H) -H -#g1 #g #Hg1 #Hg #HK lapply (after_mono … Hg Hf ??) -Hg -Hf -/3 width=3 by drops_eq_repl_back, isid_inv_eq_repl, next_eq_repl/ +#g1 #g #Hg1 #Hg #HK lapply (after_mono_eq … Hg … Hf ??) -Hg -Hf +/3 width=5 by drops_eq_repl_back, isid_inv_eq_repl, eq_next/ qed-. (* Basic_1: includes: drop_gen_refl *) (* Basic_2A1: includes: drop_inv_O2 *) lemma drops_fwd_isid: ∀L1,L2,c,f. ⬇*[c, f] L1 ≡ L2 → 𝐈⦃f⦄ → L1 = L2. #L1 #L2 #c #f #H elim H -L1 -L2 -f // -[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) -| /5 width=3 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ +[ #I #L1 #L2 #V #f #_ #_ #H elim (isid_inv_next … H) // +| /5 width=5 by isid_inv_push, lifts_fwd_isid, eq_f3, sym_eq/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma index 56b39051f..1bb1ee484 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_drops.ma @@ -27,9 +27,9 @@ theorem drops_conf: ∀L1,L,c1,f1. ⬇*[c1, f1] L1 ≡ L → [ #f1 #_ #L2 #c2 #f #HL2 #f2 #Hf12 elim (drops_inv_atom1 … HL2) -c1 -HL2 #H #Hf destruct @drops_atom #H elim (after_inv_isid3 … Hf12) -Hf12 /2 width=1 by/ -| #I #K1 #K #V1 #f1 #_ #IH #L2 #c2 #f #HL2 #f2 #Hf elim (after_inv_Sxx … Hf) -Hf +| #I #K1 #K #V1 #f1 #_ #IH #L2 #c2 #f #HL2 #f2 #Hf elim (after_inv_nxx … Hf) -Hf [2,3: // ] #g #Hg #H destruct /3 width=3 by drops_inv_drop1/ -| #I #K1 #K #V1 #V #f1 #_ #HV1 #IH #L2 #c2 #f #HL2 #f2 #Hf elim (after_inv_Oxx … Hf) -Hf * +| #I #K1 #K #V1 #V #f1 #_ #HV1 #IH #L2 #c2 #f #HL2 #f2 #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*:// ] #g2 #g #Hf #H1 #H2 destruct [ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, lifts_div/ | /4 width=3 by drops_inv_drop1, drops_drop/ @@ -49,9 +49,9 @@ theorem drops_trans: ∀L1,L,c1,f1. ⬇*[c1, f1] L1 ≡ L → #H #Hf2 destruct @drops_atom #H elim (andb_inv_true_dx … H) -H #H1 #H2 lapply (after_isid_inv_sn … Hf ?) -Hf /3 width=3 by isid_eq_repl_back/ -| #I #K1 #K #V1 #f1 #_ #IH #L2 #c2 #f2 #HL2 #f #Hf elim (after_inv_Sxx … Hf) -Hf +| #I #K1 #K #V1 #f1 #_ #IH #L2 #c2 #f2 #HL2 #f #Hf elim (after_inv_nxx … Hf) -Hf /3 width=3 by drops_drop/ -| #I #K1 #K #V1 #V #f1 #_ #HV1 #IH #L2 #c2 #f2 #HL2 #f #Hf elim (after_inv_Oxx … Hf) -Hf * +| #I #K1 #K #V1 #V #f1 #_ #HV1 #IH #L2 #c2 #f2 #HL2 #f #Hf elim (after_inv_pxx … Hf) -Hf [1,3: * |*: // ] #g2 #g #Hg #H1 #H2 destruct [ elim (drops_inv_skip1 … HL2) -HL2 /3 width=6 by drops_skip, lifts_trans/ | /4 width=3 by drops_inv_drop1, drops_drop/ @@ -64,7 +64,7 @@ qed-. (* Basic_2A1: includes: drop_mono *) lemma drops_mono: ∀L,L1,c1,f. ⬇*[c1, f] L ≡ L1 → ∀L2,c2. ⬇*[c2, f] L ≡ L2 → L1 = L2. -#L #L1 #c1 #f lapply (isid_after_dx 𝐈𝐝 f ?) +#L #L1 #c1 #f lapply (isid_after_dx 𝐈𝐝 … f) /3 width=8 by drops_conf, drops_fwd_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drop_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma similarity index 67% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/drop_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index 85b93239d..5b451af83 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drop_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -12,36 +12,47 @@ (* *) (**************************************************************************) -include "basic_2/grammar/lreq_lreq.ma". -include "basic_2/substitution/drop.ma". +include "basic_2/relocation/drops.ma". +include "basic_2/relocation/lreq_lreq.ma". -(* BASIC SLICING FOR LOCAL ENVIRONMENTS *************************************) +(* GENERAL SLICING FOR LOCAL ENVIRONMENTS ***********************************) -definition dedropable_sn: predicate (relation lenv) ≝ - λR. ∀L1,K1,s,l,m. ⬇[s, l, m] L1 ≡ K1 → ∀K2. R K1 K2 → - ∃∃L2. R L1 L2 & ⬇[s, l, m] L2 ≡ K2 & L1 ⩬[l, m] L2. +definition dedropable_sn: predicate (rtmap → relation lenv) ≝ + λR. ∀L1,K1,c,f. ⬇*[c, f] L1 ≡ K1 → ∀K2,f1. R f1 K1 K2 → + ∀f2. f ⊚ f1 ≡ f2 → + ∃∃L2. R f2 L1 L2 & ⬇*[c, f] L2 ≡ K2 & L1 ≡[f] L2. (* Properties on equivalence ************************************************) -lemma lreq_drop_trans_be: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀I,K2,W,s,i. ⬇[s, 0, i] L2 ≡ K2.ⓑ{I}W → - l ≤ i → ∀m0. i + ⫯m0 = l + m → - ∃∃K1. K1 ⩬[0, m0] K2 & ⬇[s, 0, i] L1 ≡ K1.ⓑ{I}W. -#L1 #L2 #l #m #H elim H -L1 -L2 -l -m -[ #l #m #J #K2 #W #s #i #H +lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (LTC … R). +#R #HR #L1 #K1 #c #f #HLK1 #K2 #f1 #H elim H -K2 +[ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -K1 -f1 + /3 width=4 by inj, ex3_intro/ +| #K #K2 #_ #HK2 #IH #f2 #Hf elim (IH … Hf) -IH -K1 + #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2 … Hf) -HR -K -f1 + /3 width=6 by lreq_trans, step, ex3_intro/ +] +qed-. +(* +lemma lreq_drop_trans_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 → + ∀I,K2,W,c,i. ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W → + l ≤ i → ∀k0. i + ⫯k0 = l + k → + ∃∃K1. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W. +#L1 #L2 #l #k #H elim H -L1 -L2 -l -k +[ #l #k #J #K2 #W #c #i #H elim (drop_inv_atom1 … H) -H #H destruct -| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #s #i #_ #_ #m0 +| #I1 #I2 #L1 #L2 #V1 #V2 #_ #_ #J #K2 #W #c #i #_ #_ #k0 >yplus_succ2 #H elim (ysucc_inv_O_dx … H) -| #I #L1 #L2 #V #m #HL12 #IHL12 #J #K2 #W #s #i #H #_ >yplus_O1 #m0 #H0 +| #I #L1 #L2 #V #k #HL12 #IHL12 #J #K2 #W #c #i #H #_ >yplus_O1 #k0 #H0 elim (drop_inv_O1_pair1 … H) -H * #Hi #HLK1 [ -IHL12 | -HL12 ] [ destruct /2 width=3 by drop_pair, ex2_intro/ | lapply (ylt_inv_O1 … Hi) #H yplus_succ1 #H lapply (ysucc_inv_inj … H) -H <(yplus_O1 m) + >yplus_succ1 #H lapply (ysucc_inv_inj … H) -H <(yplus_O1 k) #H0 elim (IHL12 … HLK1 … H0) -IHL12 -HLK1 -H0 // /3 width=3 by drop_drop_lt, ex2_intro/ ] -| #I1 #I2 #L1 #L2 #V1 #V2 #l #m #_ #IHL12 #J #K2 #W #s #i #HLK2 #Hli #m0 +| #I1 #I2 #L1 #L2 #V1 #V2 #l #k #_ #IHL12 #J #K2 #W #c #i #HLK2 #Hli #k0 elim (yle_inv_succ1 … Hli) -Hli #Hli #Hi yplus_succ1 >yplus_succ1 #H lapply (ysucc_inv_inj … H) -H #H0 lapply (drop_inv_drop1_lt … HLK2 ?) -HLK2 /2 width=1 by ylt_O1/ @@ -50,11 +61,11 @@ lemma lreq_drop_trans_be: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → ] qed-. -lemma lreq_drop_conf_be: ∀L1,L2,l,m. L1 ⩬[l, m] L2 → - ∀I,K1,W,s,i. ⬇[s, 0, i] L1 ≡ K1.ⓑ{I}W → - l ≤ i → ∀m0. i + ⫯m0 = l + m → - ∃∃K2. K1 ⩬[0, m0] K2 & ⬇[s, 0, i] L2 ≡ K2.ⓑ{I}W. -#L1 #L2 #l #m #HL12 #I #K1 #W #s #i #HLK1 #Hli #m0 #H0 +lemma lreq_drop_conf_be: ∀L1,L2,l,k. L1 ⩬[l, k] L2 → + ∀I,K1,W,c,i. ⬇[c, 0, i] L1 ≡ K1.ⓑ{I}W → + l ≤ i → ∀k0. i + ⫯k0 = l + k → + ∃∃K2. K1 ⩬[0, k0] K2 & ⬇[c, 0, i] L2 ≡ K2.ⓑ{I}W. +#L1 #L2 #l #k #HL12 #I #K1 #W #c #i #HLK1 #Hli #k0 #H0 elim (lreq_drop_trans_be … (lreq_sym … HL12) … HLK1 … H0) // -L1 -Hli -H0 /3 width=3 by lreq_sym, ex2_intro/ qed-. @@ -73,15 +84,6 @@ lemma drop_O1_ex: ∀K2,i,L1. |L1| = |K2| + i → ] qed-. -lemma dedropable_sn_TC: ∀R. dedropable_sn R → dedropable_sn (TC … R). -#R #HR #L1 #K1 #s #l #m #HLK1 #K2 #H elim H -K2 -[ #K2 #HK12 elim (HR … HLK1 … HK12) -HR -K1 - /3 width=4 by inj, ex3_intro/ -| #K #K2 #_ #HK2 * #L #H1L1 #HLK #H2L1 elim (HR … HLK … HK2) -HR -K - /3 width=6 by lreq_trans, step, ex3_intro/ -] -qed-. - (* Inversion lemmas on equivalence ******************************************) lemma drop_O1_inj: ∀i,L1,L2,K. ⬇[i] L1 ≡ K → ⬇[i] L2 ≡ K → L1 ⩬[i, ∞] L2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma index 338ef22d5..428fcd460 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma @@ -42,11 +42,11 @@ lemma d2_deliftable_sn_LTC: ∀R. d_deliftable2_sn R → d_deliftable2_sn (LTC qed-. lemma dropable_sn_TC: ∀R. dropable_sn R → dropable_sn (LTC … R). -#R #HR #L1 #K1 #c #f #HLK1 #L2 #u2 #H elim H -L2 -[ #L2 #HL12 #u1 #H elim (HR … HLK1 … HL12 … H) -HR -L1 -u2 +#R #HR #L1 #K1 #c #f #HLK1 #L2 #f2 #H elim H -L2 +[ #L2 #HL12 #f1 #H elim (HR … HLK1 … HL12 … H) -HR -L1 -f2 /3 width=3 by inj, ex2_intro/ -| #L #L2 #_ #HL2 #IH #u1 #H elim (IH … H) -IH - #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -L -u2 +| #L #L2 #_ #HL2 #IH #f1 #H elim (IH … H) -IH + #K #HK1 #HLK elim (HR … HLK … HL2 … H) -HR -L -f2 /3 width=3 by step, ex2_intro/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma index 011625495..d0dc9e7a0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_weight.ma @@ -37,7 +37,7 @@ lemma drops_fwd_lw_lt: ∀L1,L2,f. ⬇*[Ⓣ, f] L1 ≡ L2 → [ #f #Hf #Hnf elim Hnf -Hnf /2 width=1 by/ | /3 width=3 by drops_fwd_lw, le_to_lt_to_lt/ | #I #L1 #L2 #V1 #V2 #f #_ #HV21 #IHL12 #H normalize in ⊢ (?%%); -I - >(lifts_fwd_tw … HV21) -V2 /5 width=1 by isid_push, monotonic_lt_plus_l/ + >(lifts_fwd_tw … HV21) -V2 /5 width=3 by isid_push, monotonic_lt_plus_l/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma index 15117986b..604a918c5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/frees.ma @@ -12,30 +12,95 @@ (* *) (**************************************************************************) +include "ground_2/relocation/trace_sor.ma". +include "ground_2/relocation/trace_isun.ma". include "basic_2/notation/relations/freestar_3.ma". -include "basic_2/grammar/trace_sor.ma". include "basic_2/grammar/lenv.ma". (* CONTEXT-SENSITIVE FREE VARIABLES *****************************************) inductive frees: relation3 lenv term trace ≝ | frees_atom: ∀I. frees (⋆) (⓪{I}) (◊) -| frees_sort: ∀L,k,cs. frees L (⋆k) cs → - ∀I,T. frees (L.ⓑ{I}T) (⋆k) (Ⓕ @ cs) -| frees_zero: ∀L,T,cs. frees L T cs → - ∀I. frees (L.ⓑ{I}T) (#0) (Ⓣ @ cs) -| frees_lref: ∀L,i,cs. frees L (#i) cs → - ∀I,T. frees (L.ⓑ{I}T) (#(S i)) (Ⓕ @ cs) -| frees_gref: ∀L,p,cs. frees L (§p) cs → - ∀I,T. frees (L.ⓑ{I}T) (§p) (Ⓕ @ cs) -| frees_bind: ∀cv,ct,cs. cv ⋓ ct ≡ cs → - ∀L,V. frees L V cv → ∀I,T,b. frees (L.ⓑ{I}V) T (b @ ct) → - ∀a. frees L (ⓑ{a,I}V.T) cs -| frees_flat: ∀cv,ct,cs. cv ⋓ ct ≡ cs → - ∀L,V. frees L V cv → ∀T. frees L T ct → - ∀I. frees L (ⓕ{I}V.T) cs +| frees_sort: ∀I,L,V,s,t. frees L (⋆s) t → + frees (L.ⓑ{I}V) (⋆s) (Ⓕ @ t) +| frees_zero: ∀I,L,V,t. frees L V t → + frees (L.ⓑ{I}V) (#0) (Ⓣ @ t) +| frees_lref: ∀I,L,V,i,t. frees L (#i) t → + frees (L.ⓑ{I}V) (#⫯i) (Ⓕ @ t) +| frees_gref: ∀I,L,V,p,t. frees L (§p) t → + frees (L.ⓑ{I}V) (§p) (Ⓕ @ t) +| frees_bind: ∀I,L,V,T,t1,t2,t,b,a. frees L V t1 → frees (L.ⓑ{I}V) T (b @ t2) → + t1 ⋓ t2 ≡ t → frees L (ⓑ{a,I}V.T) t +| frees_flat: ∀I,L,V,T,t1,t2,t. frees L V t1 → frees L T t2 → + t1 ⋓ t2 ≡ t → frees L (ⓕ{I}V.T) t . interpretation "context-sensitive free variables (term)" - 'FreeStar L T cs = (frees L T cs). + 'FreeStar L T t = (frees L T t). + +(* Basic forward lemmas *****************************************************) + +fact frees_fwd_sort_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = ⋆x → 𝐔⦃t⦄. +#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/ +[ #_ #L #V #t #_ #_ #x #H destruct +| #_ #L #_ #i #t #_ #_ #x #H destruct +| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct +| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct +] +qed-. + +lemma frees_fwd_sort: ∀L,t,s. L ⊢ 𝐅*⦃⋆s⦄ ≡ t → 𝐔⦃t⦄. +/2 width=5 by frees_fwd_sort_aux/ qed-. + +fact frees_fwd_gref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀x. X = §x → 𝐔⦃t⦄. +#L #X #t #H elim H -L -X -t /3 width=2 by isun_id, isun_false/ +[ #_ #L #V #t #_ #_ #x #H destruct +| #_ #L #_ #i #t #_ #_ #x #H destruct +| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #_ #_ #x #H destruct +| #I #L #V #T #t1 #t2 #t #_ #_ #_ #_ #_ #x #H destruct +] +qed-. + +lemma frees_fwd_gref: ∀L,t,p. L ⊢ 𝐅*⦃§p⦄ ≡ t → 𝐔⦃t⦄. +/2 width=5 by frees_fwd_gref_aux/ qed-. + +(* Basic inversion lemmas ***************************************************) + +fact frees_inv_zero_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → X = #0 → + (L = ⋆ ∧ t = ◊) ∨ + ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u. +#L #X #t * -L -X -t +[ /3 width=1 by or_introl, conj/ +| #I #L #V #s #t #_ #H destruct +| /3 width=7 by ex3_4_intro, or_intror/ +| #I #L #V #i #t #_ #H destruct +| #I #L #V #p #t #_ #H destruct +| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #H destruct +| #I #L #V #T #t1 #t2 #t #_ #_ #_ #H destruct +] +qed-. + +lemma frees_inv_zero: ∀L,t. L ⊢ 𝐅*⦃#0⦄ ≡ t → + (L = ⋆ ∧ t = ◊) ∨ + ∃∃I,K,V,u. K ⊢ 𝐅*⦃V⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓣ@u. +/2 width=3 by frees_inv_zero_aux/ qed-. + +fact frees_inv_lref_aux: ∀L,X,t. L ⊢ 𝐅*⦃X⦄ ≡ t → ∀j. X = #(⫯j) → + (L = ⋆ ∧ t = ◊) ∨ + ∃∃I,K,V,u. K ⊢ 𝐅*⦃#j⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u. +#L #X #t * -L -X -t +[ /3 width=1 by or_introl, conj/ +| #I #L #V #s #t #_ #j #H destruct +| #I #L #V #t #_ #j #H destruct +| #I #L #V #i #t #Ht #j #H destruct /3 width=7 by ex3_4_intro, or_intror/ +| #I #L #V #p #t #_ #j #H destruct +| #I #L #V #T #t1 #t2 #t #b #a #_ #_ #_ #j #H destruct +| #I #L #V #T #t1 #t2 #t #_ #_ #_ #j #H destruct +] +qed-. + +lemma frees_inv_lref: ∀L,i,t. L ⊢ 𝐅*⦃#(⫯i)⦄ ≡ t → + (L = ⋆ ∧ t = ◊) ∨ + ∃∃I,K,V,u. K ⊢ 𝐅*⦃#i⦄ ≡ u & L = K.ⓑ{I}V & t = Ⓕ@u. +/2 width=3 by frees_inv_lref_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma index 0bed76cfd..d89370b41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs.ma @@ -12,12 +12,18 @@ (* *) (**************************************************************************) -include "ground_2/relocation/nstream_sle.ma". +include "ground_2/relocation/rtmap_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 ****) +definition relation5 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +≝ λA,B,C,D,E.A→B→C→D→E→Prop. + +definition relation6 : Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] → Type[0] +≝ λA,B,C,D,E,F.A→B→C→D→E→F→Prop. + (* Basic_2A1: includes: lpx_sn_atom lpx_sn_pair *) inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ | lexs_atom: ∀f. lexs RN RP f (⋆) (⋆) @@ -32,6 +38,19 @@ inductive lexs (RN,RP:relation3 lenv term term): rtmap → relation lenv ≝ interpretation "general entrywise extension (local environment)" 'RelationStar RN RP f L1 L2 = (lexs RN RP f L1 L2). +definition lpx_sn_confluent: relation6 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RN1,RP1,RN2,RP2. + ∀f,L0,T0,T1. R1 L0 T0 T1 → ∀T2. R2 L0 T0 T2 → + ∀L1. L0 ⦻*[RN1, RP1, f] L1 → ∀L2. L0 ⦻*[RN2, RP2, f] L2 → + ∃∃T. R2 L1 T1 T & R1 L2 T2 T. + +definition lexs_transitive: relation4 (relation3 lenv term term) + (relation3 lenv term term) … ≝ + λR1,R2,RN,RP. + ∀f,L1,T1,T. R1 L1 T1 T → ∀L2. L1 ⦻*[RN, RP, f] L2 → + ∀T2. R2 L2 T T2 → R1 L1 T1 T2. + (* Basic inversion lemmas ***************************************************) fact lexs_inv_atom1_aux: ∀RN,RP,X,Y,f. X ⦻*[RN, RP, f] Y → X = ⋆ → Y = ⋆. @@ -128,16 +147,16 @@ qed-. (* Basic properties *********************************************************) -lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_stream_repl_back … (λf. L1 ⦻*[RN, RP, f] L2). +lemma lexs_eq_repl_back: ∀RN,RP,L1,L2. eq_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/ +[ elim (eq_inv_nx … H) -H /3 width=3 by lexs_next/ +| elim (eq_inv_px … H) -H /3 width=3 by lexs_push/ ] qed-. -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 *) +lemma lexs_eq_repl_fwd: ∀RN,RP,L1,L2. eq_repl_fwd … (λf. L1 ⦻*[RN, RP, f] L2). +#RN #RP #L1 #L2 @eq_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 *) @@ -156,9 +175,9 @@ lemma sle_lexs_trans: ∀RN,RP. (∀L,T1,T2. RN L T1 T2 → RP L T1 T2) → #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/ -| /4 width=5 by lexs_push, sle_inv_OS_aux/ -| elim (sle_inv_xO_aux … H) -H [3: // |2: skip ] +[ /4 width=5 by lexs_next, sle_inv_nn/ +| /4 width=5 by lexs_push, sle_inv_pn/ +| elim (sle_inv_xp … H) -H [2,3: // ] #g1 #H #H1 destruct /3 width=5 by lexs_push/ ] qed-. @@ -169,9 +188,9 @@ lemma sle_lexs_conf: ∀RN,RP. (∀L,T1,T2. RP L T1 T2 → RN L T1 T2) → #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/ -| /4 width=5 by lexs_push, sle_inv_OO_aux/ -| elim (sle_inv_Sx_aux … H) -H [3: // |2: skip ] +[ /4 width=5 by lexs_next, sle_inv_pn/ +| /4 width=5 by lexs_push, sle_inv_pp/ +| elim (sle_inv_nx … H) -H [2,3: // ] #g2 #H #H2 destruct /3 width=5 by lexs_next/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma similarity index 75% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_drops.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma index 081ba659b..fa066595f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lpx_sn_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_drops.ma @@ -12,25 +12,27 @@ (* *) (**************************************************************************) -include "basic_2/relocation/lpx_sn.ma". +include "basic_2/relocation/lexs.ma". include "basic_2/relocation/drops.ma". -(* SN POINTWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS *********) +(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) -(* Properties on general slicing for local environments *********************) - -lemma lpx_sn_deliftable_dropable: ∀R. (∀b. d_deliftable2_sn (R b)) → dropable_sn (lpx_sn R). -#R #HR #L1 #K1 #c #t #H elim H -L1 -K1 -t -[ #t #Ht #X #u2 #H #u1 #Hu elim (lpx_sn_inv_atom1 … H) -H - #H1 #H2 destruct elim (after_inv_empty3 … Hu) -Hu - #H1 #H2 destruct /3 width=3 by drops_atom, lpx_sn_atom, ex2_intro/ -| #I #L1 #K1 #V1 #t #_ #IH #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_false1 … Hu) -Hu - #u #H1 #Hu destruct elim (IH … HL … Hu) -L1 /3 width=3 by drops_drop, ex2_intro/ -| #I #L1 #K1 #V1 #W1 #t #HLK #HWV #IHLK #X #u2 #H #u1 #Hu elim (lpx_sn_inv_pair1 … H) -H - #L2 #V2 #y2 #x2 #HL #HV #H1 #H2 destruct elim (after_inv_true1 … Hu) -Hu - #y1 #y #x1 #H1 #H2 #Hu destruct elim (HR … HV … HLK … HWV) -V1 - elim (IHLK … HL … Hu) -L1 /3 width=5 by drops_skip, lpx_sn_pair, ex2_intro/ +(* Basic_2A1: includes: lpx_sn_deliftable_dropable *) +lemma lexs_deliftable_dropable: ∀RN,RP. d_deliftable2_sn RN → d_deliftable2_sn RP → + dropable_sn (lexs RN RP). +#RN #RP #HN #HP #L1 #K1 #c #f #H elim H -L1 -K1 -f +[ #f #Hf #X #f2 #H #f1 #Hf2 >(lexs_inv_atom1 … H) -X + /4 width=3 by lexs_atom, drops_atom, ex2_intro/ +| #I #L1 #K1 #V1 #f #_ #IH #X #f2 #H #f1 #Hf2 elim (after_inv_nxx … Hf2) -Hf2 [2,3: // ] + #g2 #Hg2 #H2 destruct elim (lexs_inv_next1 … H) -H + #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 + /3 width=3 by drops_drop, ex2_intro/ +| #I #L1 #K1 #V1 #W1 #f #HLK #HWV #IH #X #f2 #H #f1 #Hf2 elim (after_inv_pxx … Hf2) -Hf2 [1,3:* |*: // ] + #g1 #g2 #Hg2 #H1 #H2 destruct + [ elim (lexs_inv_push1 … H) | elim (lexs_inv_next1 … H) ] -H + #L2 #V2 #HL12 #HV12 #H destruct elim (IH … HL12 … Hg2) -g2 + [ elim (HP … HV12 … HLK … HWV) | elim (HN … HV12 … HLK … HWV) ] -V1 + /3 width=5 by lexs_next, lexs_push, drops_skip, ex2_intro/ ] qed-. (* diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma new file mode 100644 index 000000000..1b8aa44cb --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lexs_lexs.ma @@ -0,0 +1,93 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rtmap_sand.ma". +include "ground_2/relocation/rtmap_sor.ma". +include "basic_2/grammar/lenv_weight.ma". +include "basic_2/relocation/lexs.ma". + +(* GENERAL ENTRYWISE EXTENSION OF A CONTEXT-SENSITIVE REALTION FOR TERMS ****) + +(* Main properties **********************************************************) + +(* Basic_2A1: includes: lpx_sn_trans *) +theorem lexs_trans (RN) (RP) (f): lexs_transitive RN RN RN RP → + lexs_transitive RP RP RN RP → + Transitive … (lexs RN RP f). +#RN #RP #f #HN #HP #L1 #L0 #H elim H -L1 -L0 -f +[ #f #L2 #H >(lexs_inv_atom1 … H) -L2 // +| #I #K1 #K #V1 #V #f #HK1 #HV1 #IH #L2 #H elim (lexs_inv_next1 … H) -H + #K2 #V2 #HK2 #HV2 #H destruct /4 width=6 by lexs_next/ +| #I #K1 #K #V1 #V #f #HK1 #HV1 #IH #L2 #H elim (lexs_inv_push1 … H) -H + #K2 #V2 #HK2 #HV2 #H destruct /4 width=6 by lexs_push/ +] +qed-. + +(* Basic_2A1: includes: lpx_sn_conf *) +theorem lexs_conf: ∀RN1,RP1,RN2,RP2. + lpx_sn_confluent RN1 RN2 RN1 RP1 RN2 RP2 → + lpx_sn_confluent RP1 RP2 RN1 RP1 RN2 RP2 → + ∀f. confluent2 … (lexs RN1 RP1 f) (lexs RN2 RP2 f). +#RN1 #RP1 #RN2 #RP2 #HRN #HRP #f #L0 generalize in match f; -f +@(f_ind … lw … L0) -L0 #x #IH * +[ #_ #f #X1 #H1 #X2 #H2 -x + >(lexs_inv_atom1 … H1) -X1 + >(lexs_inv_atom1 … H2) -X2 /2 width=3 by lexs_atom, ex2_intro/ +| #L0 #I #V0 #Hx #f elim (pn_split f) * + #g #H #X1 #H1 #X2 #H2 destruct + [ elim (lexs_inv_push1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2 + elim (HRP … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_push, ex2_intro/ + | elim (lexs_inv_next1 … H1) -H1 #L1 #V1 #HL01 #HV01 #H destruct + elim (lexs_inv_next1 … H2) -H2 #L2 #V2 #HL02 #HV02 #H destruct + elim (IH … HL01 … HL02) -IH // #L #HL1 #HL2 + elim (HRN … HV01 … HV02 … HL01 … HL02) -L0 -V0 /3 width=5 by lexs_next, ex2_intro/ + ] +] +qed-. + +theorem lexs_canc_sx: ∀RN,RP,f. Transitive … (lexs RN RP f) → + symmetric … (lexs RN RP f) → + left_cancellable … (lexs RN RP f). +/3 width=3 by/ qed-. + +theorem lexs_canc_dx: ∀RN,RP,f. Transitive … (lexs RN RP f) → + symmetric … (lexs RN RP f) → + right_cancellable … (lexs RN RP f). +/3 width=3 by/ qed-. + +theorem lexs_meet: ∀RN,RP,L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f. f1 ⋒ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. +#RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // +#I #L1 #L2 #V1 #V2 #f1 #_ #H1V #IH #f2 elim (pn_split f2) * +#g2 #H #H2 #f #Hf destruct +[1,3: elim (lexs_inv_push … H2) |2,4: elim (lexs_inv_next … H2) ] -H2 +#H2 #H2V #_ +[ elim (sand_inv_npx … Hf) | elim (sand_inv_ppx … Hf) | elim (sand_inv_nnx … Hf) | elim (sand_inv_pnx … Hf) ] -Hf +/3 width=5 by lexs_next, lexs_push/ +qed-. + +theorem lexs_join: ∀RN,RP,L1,L2,f1. L1 ⦻*[RN, RP, f1] L2 → + ∀f2. L1 ⦻*[RN, RP, f2] L2 → + ∀f. f1 ⋓ f2 ≡ f → L1 ⦻*[RN, RP, f] L2. +#RN #RP #L1 #L2 #f1 #H elim H -L1 -L2 -f1 // +#I #L1 #L2 #V1 #V2 #f1 #_ #H1V #IH #f2 elim (pn_split f2) * +#g2 #H #H2 #f #Hf destruct +[1,3: elim (lexs_inv_push … H2) |2,4: elim (lexs_inv_next … H2) ] -H2 +#H2 #H2V #_ +[ elim (sor_inv_npx … Hf) | elim (sor_inv_ppx … Hf) | elim (sor_inv_nnx … Hf) | elim (sor_inv_pnx … Hf) ] -Hf +/3 width=5 by lexs_next, lexs_push/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index 45cd021eb..cae6be8f9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/relocation/nstream_id.ma". +include "ground_2/relocation/nstream_after.ma". include "basic_2/notation/relations/rliftstar_3.ma". include "basic_2/grammar/term.ma". @@ -264,20 +264,20 @@ qed-. (* Basic properties *********************************************************) -lemma lifts_eq_repl_back: ∀T1,T2. eq_stream_repl_back … (λf. ⬆*[f] T1 ≡ T2). +lemma lifts_eq_repl_back: ∀T1,T2. eq_repl_back … (λf. ⬆*[f] T1 ≡ T2). #T1 #T2 #f1 #H elim H -T1 -T2 -f1 -/4 width=3 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, push_eq_repl/ +/4 width=5 by lifts_flat, lifts_bind, lifts_lref, at_eq_repl_back, eq_push/ qed-. -lemma lifts_eq_repl_fwd: ∀T1,T2. eq_stream_repl_fwd … (λf. ⬆*[f] T1 ≡ T2). -#T1 #T2 @eq_stream_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *) +lemma lifts_eq_repl_fwd: ∀T1,T2. eq_repl_fwd … (λf. ⬆*[f] T1 ≡ T2). +#T1 #T2 @eq_repl_sym /2 width=3 by lifts_eq_repl_back/ (**) (* full auto fails *) qed-. (* Basic_1: includes: lift_r *) (* Basic_2A1: includes: lift_refl *) lemma lifts_refl: ∀T,f. 𝐈⦃f⦄ → ⬆*[f] T ≡ T. #T elim T -T * -/4 width=1 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/ +/4 width=3 by lifts_flat, lifts_bind, lifts_lref, isid_inv_at, isid_push/ qed. (* Basic_2A1: includes: lift_total *) @@ -333,7 +333,7 @@ qed-. lemma is_lifts_dec: ∀T2,f. Decidable (∃T1. ⬆*[f] T1 ≡ T2). #T1 elim T1 -T1 [ * [1,3: /3 width=2 by lifts_sort, lifts_gref, ex_intro, or_introl/ ] - #i2 #f elim (is_at_dec f i2) + #i2 #f elim (is_at_dec f i2) // [ * /4 width=3 by lifts_lref, ex_intro, or_introl/ | #H @or_intror * #X #HX elim (lifts_inv_lref2 … HX) -HX diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma index 2372488aa..109e5e973 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_lifts.ma @@ -76,12 +76,12 @@ qed-. (* Basic_2A1: includes: lift_inj *) lemma lifts_inj: ∀T1,U,f. ⬆*[f] T1 ≡ U → ∀T2. ⬆*[f] T2 ≡ U → T1 = T2. -#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝 f ?) +#T1 #U #f #H1 #T2 #H2 lapply (isid_after_dx 𝐈𝐝 … f) /3 width=6 by lifts_div, lifts_fwd_isid/ qed-. (* Basic_2A1: includes: lift_mono *) lemma lifts_mono: ∀T,U1,f. ⬆*[f] T ≡ U1 → ∀U2. ⬆*[f] T ≡ U2 → U1 = U2. -#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 f ?) +#T #U1 #f #H1 #U2 #H2 lapply (isid_after_sn 𝐈𝐝 … f) /3 width=6 by lifts_conf, lifts_fwd_isid/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index 568dad1ae..58914d3a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -27,10 +27,10 @@ interpretation (* Basic properties *********************************************************) -lemma lreq_eq_repl_back: ∀L1,L2. eq_stream_repl_back … (λf. L1 ≡[f] L2). +lemma lreq_eq_repl_back: ∀L1,L2. eq_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). +lemma lreq_eq_repl_fwd: ∀L1,L2. eq_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 → @@ -88,7 +88,7 @@ lemma lreq_inv_next: ∀I1,I2,L1,L2,V1,V2,f. 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/ +#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: -- 2.39.2