From 58ea181757dce19b875b2f5a224fe193b2263004 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 14 Apr 2017 17:01:44 +0000 Subject: [PATCH] - lfpxs based on tc_lfxs - documentation improved with the attribute "uses" - cpre and cpxe parked for now --- .../cpre.ma => etc/cpre/cpre.etc} | 0 .../cpre_cpre.ma => etc/cpre/cpre_cpre.etc} | 0 .../predeval_4.ma => etc/cpre/predeval_4.etc} | 0 .../cpxe.ma => etc/cpxe/cpxe.etc} | 0 .../predeval_6.ma => etc/cpxe/predeval_6.etc} | 0 .../cpxs_lreq.ma => etc/cpxs/cpxs_lreq.etc} | 0 .../basic_2/etc/lfpxs/lfpxs_cpxs.etc | 1 - .../basic_2/etc/lfpxs/lfpxs_lreq.etc | 29 +++ .../basic_2/etc/lleq/lleq_drop.etc | 22 -- .../basic_2/etc/llpx_sn/llpx_sn_drop.etc | 38 ---- .../basic_2/etc/lpx_sn/lpx_sn_tc.etc | 70 ------ .../lambdadelta/basic_2/etc/tc_lfxs.etc | 118 ++++++++++ .../lambdadelta/basic_2/i_static/lfxss_etc.ma | 31 --- .../lambdadelta/basic_2/i_static/tc_lfxs.ma | 207 ++++++------------ .../basic_2/i_static/tc_lfxs_fqup.ma | 48 ++++ .../basic_2/i_static/tc_lfxs_length.ma | 29 +++ .../basic_2/rt_computation/cpxs_lfpx.ma | 3 +- .../basic_2/rt_computation/csx_cpxs.ma | 2 +- .../basic_2/rt_computation/lfpxs.ma | 38 ++-- .../basic_2/rt_computation/lfpxs_cpxs.ma | 12 +- .../basic_2/rt_computation/lfpxs_fqup.ma | 40 ++-- .../basic_2/rt_computation/lfpxs_fqus.ma | 63 ++++++ .../basic_2/rt_computation/lfpxs_length.ma | 25 ++- .../basic_2/rt_computation/lfpxs_lfdeq.ma | 48 ++++ .../{lpxs_lpxs.ma => lfpxs_lfpxs.ma} | 10 +- .../basic_2/rt_computation/lfsx.ma | 11 +- .../basic_2/rt_computation/lfsx_fqup.ma | 2 +- .../basic_2/rt_computation/lfsx_lfpxs.ma | 123 +++++++++++ .../basic_2/rt_computation/lfsx_lfsx.ma | 11 +- .../basic_2/rt_computation/lpxs_lleq.ma | 141 ------------ .../basic_2/rt_computation/lsx_alt.ma | 115 ---------- .../basic_2/rt_computation/lsx_lpxs.ma | 62 ------ .../basic_2/rt_computation/partial.txt | 2 +- .../lambdadelta/basic_2/rt_transition/lfpr.ma | 24 +- .../basic_2/rt_transition/lfpr_drops.ma | 3 + .../basic_2/rt_transition/lfpr_fqup.ma | 2 + .../basic_2/rt_transition/lfpr_fquq.ma | 2 + .../basic_2/rt_transition/lfpr_length.ma | 1 + .../basic_2/rt_transition/lfpr_lfpx.ma | 1 + .../lambdadelta/basic_2/rt_transition/lfpx.ma | 23 +- .../basic_2/rt_transition/lfpx_aaa.ma | 2 +- .../basic_2/rt_transition/lfpx_drops.ma | 3 + .../basic_2/rt_transition/lfpx_fqup.ma | 2 + .../basic_2/rt_transition/lfpx_frees.ma | 6 +- .../basic_2/rt_transition/lfpx_length.ma | 1 + .../basic_2/rt_transition/lfpx_lfdeq.ma | 6 +- .../lambdadelta/basic_2/static/lfdeq.ma | 30 +-- .../lambdadelta/basic_2/static/lfdeq_fqup.ma | 1 + .../basic_2/static/lfdeq_length.ma | 1 + .../lambdadelta/basic_2/static/lfdeq_lfdeq.ma | 32 ++- .../lambdadelta/basic_2/static/lfxs.ma | 35 ++- .../lambdadelta/basic_2/static/lfxs_fqup.ma | 1 + .../lambdadelta/basic_2/static/lfxs_length.ma | 1 + .../lambdadelta/basic_2/static/lfxs_lfxs.ma | 21 ++ .../lambdadelta/basic_2/syntax/tdeq_tdeq.ma | 2 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 57 files changed, 744 insertions(+), 765 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/cpre.ma => etc/cpre/cpre.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/cpre_cpre.ma => etc/cpre/cpre_cpre.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predeval_4.ma => etc/cpre/predeval_4.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/cpxe.ma => etc/cpxe/cpxe.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{notation/relations/predeval_6.ma => etc/cpxe/predeval_6.etc} (100%) rename matita/matita/contribs/lambdadelta/basic_2/{rt_computation/cpxs_lreq.ma => etc/cpxs/cpxs_lreq.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/tc_lfxs.etc delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_length.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma rename matita/matita/contribs/lambdadelta/basic_2/rt_computation/{lpxs_lpxs.ma => lfpxs_lfpxs.ma} (78%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre_cpre.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpre_cpre.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpre/cpre_cpre.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpre/predeval_4.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_4.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpre/predeval_4.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxe.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxe/cpxe.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxe.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpxe/cpxe.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxe/predeval_6.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/predeval_6.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpxe/predeval_6.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_lreq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lreq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/cpxs/cpxs_lreq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc index 6edda23e1..a6eb3b6ac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_cpxs.etc @@ -25,4 +25,3 @@ lemma lpxs_ind_alt: ∀h,o,G. ∀R:relation lenv. lemma lpxs_pair2: ∀h,o,I,G,L1,L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → ∀V1,V2. ⦃G, L2⦄ ⊢ V1 ➡*[h, o] V2 → ⦃G, L1.ⓑ{I}V1⦄ ⊢ ➡*[h, o] L2.ⓑ{I}V2. /3 width=3 by lpxs_pair, lpxs_cpxs_trans/ qed. - diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc new file mode 100644 index 000000000..fc77921e7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpxs/lfpxs_lreq.etc @@ -0,0 +1,29 @@ +fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → + ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & + (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). +#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k +[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H + /3 width=5 by ex3_intro, conj/ +| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct +| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H + elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct + lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm + elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH + @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/ +| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #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, lreq_succ/ + #T elim (IH T) #HL0dx #HL0sn + @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/ +] +qed-. + +lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 → + ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → + ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & + (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). +/2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc index 10e8a919a..91f7bf16f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lleq/lleq_drop.etc @@ -77,10 +77,6 @@ lemma lleq_inv_S: ∀L1,L2,T,l. L1 ≡[T, l+1] L2 → K1 ≡[V, 0] K2 → L1 ≡[T, l] 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,l,i. L1 ≡[#i, l] L2 → @@ -98,21 +94,3 @@ lemma lleq_fwd_lref_sn: ∀L1,L2,l,i. L1 ≡[#i, l] L2 → #L1 #L2 #l #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-. - -(* Inversion lemmas on negated lazy quivalence for local environments *******) - -lemma nlleq_inv_bind: ∀a,I,L1,L2,V,T,l. (L1 ≡[ⓑ{a,I}V.T, l] L2 → ⊥) → - (L1 ≡[V, l] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[T, ⫯l] L2.ⓑ{I}V → ⊥). -/3 width=2 by nllpx_sn_inv_bind, eq_term_dec/ qed-. - -lemma nlleq_inv_flat: ∀I,L1,L2,V,T,l. (L1 ≡[ⓕ{I}V.T, l] L2 → ⊥) → - (L1 ≡[V, l] L2 → ⊥) ∨ (L1 ≡[T, l] 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/etc/llpx_sn/llpx_sn_drop.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc index 34980b9f6..c523a4c02 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/llpx_sn/llpx_sn_drop.etc @@ -104,46 +104,8 @@ lemma llpx_sn_inv_S: ∀R,L1,L2,T,l. llpx_sn R (l + 1) T L1 L2 → llpx_sn R 0 V1 K1 K2 → R K1 V1 V2 → llpx_sn R l 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 drop_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-. - -(* Inversion lemmas on negated lazy pointwise extension *********************) - -lemma nllpx_sn_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → - ∀a,I,L1,L2,V,T,l. (llpx_sn R l (ⓑ{a,I}V.T) L1 L2 → ⊥) → - (llpx_sn R l V L1 L2 → ⊥) ∨ (llpx_sn R (⫯l) T (L1.ⓑ{I}V) (L2.ⓑ{I}V) → ⊥). -#R #HR #a #I #L1 #L2 #V #T #l #H elim (llpx_sn_dec … HR V L1 L2 l) -/4 width=1 by llpx_sn_bind, or_intror, or_introl/ -qed-. - -lemma nllpx_sn_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → - ∀I,L1,L2,V,T,l. (llpx_sn R l (ⓕ{I}V.T) L1 L2 → ⊥) → - (llpx_sn R l V L1 L2 → ⊥) ∨ (llpx_sn R l T L1 L2 → ⊥). -#R #HR #I #L1 #L2 #V #T #l #H elim (llpx_sn_dec … HR V L1 L2 l) -/4 width=1 by llpx_sn_flat, or_intror, or_introl/ -qed-. - -lemma nllpx_sn_inv_bind_O: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → - ∀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_dec … HR V L1 L2 0) -/4 width=1 by llpx_sn_bind_O, or_intror, or_introl/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc index 23eaab6ab..cb772458b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lpx_sn/lpx_sn_tc.etc @@ -18,26 +18,6 @@ include "basic_2/substitution/lpx_sn.ma". (* Properties on transitive_closure *****************************************) -lemma TC_lpx_sn_pair_refl: ∀R. (∀L. reflexive … (R L)) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,V. TC … (lpx_sn R) (L1. ⓑ{I} V) (L2. ⓑ{I} V). -#R #HR #L1 #L2 #H @(TC_star_ind … L2 H) -L2 -[ /2 width=1 by lpx_sn_refl/ -| /3 width=1 by TC_reflexive, lpx_sn_refl/ -| /3 width=5 by lpx_sn_pair, step/ -] -qed-. - -lemma TC_lpx_sn_pair: ∀R. (∀L. reflexive … (R L)) → - ∀I,L1,L2. TC … (lpx_sn R) L1 L2 → - ∀V1,V2. LTC … R L1 V1 V2 → - TC … (lpx_sn R) (L1. ⓑ{I} V1) (L2. ⓑ{I} V2). -#R #HR #I #L1 #L2 #HL12 #V1 #V2 #H @(TC_star_ind_dx … V1 H) -V1 // -[ /2 width=1 by TC_lpx_sn_pair_refl/ -| /4 width=3 by TC_strap, lpx_sn_pair, lpx_sn_refl/ -] -qed-. - lemma lpx_sn_LTC_TC_lpx_sn: ∀R. (∀L. reflexive … (R L)) → ∀L1,L2. lpx_sn (LTC … R) L1 L2 → TC … (lpx_sn R) L1 L2. @@ -47,24 +27,6 @@ qed-. (* Inversion lemmas on transitive closure ***********************************) -lemma TC_lpx_sn_inv_atom2: ∀R,L1. TC … (lpx_sn R) L1 (⋆) → L1 = ⋆. -#R #L1 #H @(TC_ind_dx … L1 H) -L1 -[ /2 width=2 by lpx_sn_inv_atom2/ -| #L1 #L #HL1 #_ #IHL2 destruct /2 width=2 by lpx_sn_inv_atom2/ -] -qed-. - -lemma TC_lpx_sn_inv_pair2: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀I,L1,K2,V2. TC … (lpx_sn R) L1 (K2.ⓑ{I}V2) → - ∃∃K1,V1. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L1 = K1. ⓑ{I} V1. -#R #HR #I #L1 #K2 #V2 #H @(TC_ind_dx … L1 H) -L1 -[ #L1 #H elim (lpx_sn_inv_pair2 … H) -H /3 width=5 by inj, ex3_2_intro/ -| #L1 #L #HL1 #_ * #K #V #HK2 #HV2 #H destruct - elim (lpx_sn_inv_pair2 … HL1) -HL1 #K1 #V1 #HK1 #HV1 #H destruct - lapply (HR … HV2 … HK1) -HR -HV2 /3 width=5 by TC_strap, ex3_2_intro/ -] -qed-. - lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀S:relation lenv. S (⋆) (⋆) → ( @@ -81,39 +43,7 @@ lemma TC_lpx_sn_ind: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ] qed-. -lemma TC_lpx_sn_inv_atom1: ∀R,L2. TC … (lpx_sn R) (⋆) L2 → L2 = ⋆. -#R #L2 #H elim H -L2 -[ /2 width=2 by lpx_sn_inv_atom1/ -| #L #L2 #_ #HL2 #IHL1 destruct /2 width=2 by lpx_sn_inv_atom1/ -] -qed-. - -fact TC_lpx_sn_inv_pair1_aux: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀L1,L2. TC … (lpx_sn R) L1 L2 → - ∀I,K1,V1. L1 = K1.ⓑ{I}V1 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -#R #HR #L1 #L2 #H @(TC_lpx_sn_ind … H) // -HR -L1 -L2 -[ #J #K #W #H destruct -| #I #L1 #L2 #V1 #V2 #HL12 #HV12 #_ #J #K #W #H destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma TC_lpx_sn_inv_pair1: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → - ∀I,K1,L2,V1. TC … (lpx_sn R) (K1.ⓑ{I}V1) L2 → - ∃∃K2,V2. TC … (lpx_sn R) K1 K2 & LTC … R K1 V1 V2 & L2 = K2. ⓑ{I} V2. -/2 width=3 by TC_lpx_sn_inv_pair1_aux/ qed-. - lemma TC_lpx_sn_inv_lpx_sn_LTC: ∀R. c_rs_transitive … R (λ_. lpx_sn R) → ∀L1,L2. TC … (lpx_sn R) L1 L2 → lpx_sn (LTC … R) L1 L2. /3 width=4 by TC_lpx_sn_ind, lpx_sn_pair/ qed-. - -(* Forward lemmas on transitive closure *************************************) - -lemma TC_lpx_sn_fwd_length: ∀R,L1,L2. TC … (lpx_sn R) L1 L2 → |L1| = |L2|. -#R #L1 #L2 #H elim H -L2 -[ #L2 #HL12 >(lpx_sn_fwd_length … HL12) -HL12 // -| #L #L2 #_ #HL2 #IHL1 - >IHL1 -L1 >(lpx_sn_fwd_length … HL2) -HL2 // -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/tc_lfxs.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/tc_lfxs.etc new file mode 100644 index 000000000..e2f613a87 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/tc_lfxs.etc @@ -0,0 +1,118 @@ +(* lfxs_pair_repl_dx is not generic enough **********************************) + +fact tc_lfxs_pair_repl_dx_aux: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,Y,V1,T. L1.ⓑ{I}V1 ⦻**[R, T] Y → + ∀L2,V2. Y = L2.ⓑ{I}V2 → + L1.ⓑ{I}V1 ⦻**[R, T] L2.ⓑ{I}V1. +#R #HR #I #L1 #Y #V1 #T #H elim H -Y +/3 width=6 by lfxs_pair_repl_dx, step, inj/ +#Y #Y2 #HY #HY2 #IH #L2 #V2 #H destruct +elim (lfxs_fwd_dx … HY2) #L #V #H destruct +lapply (IH ???) [4: |*: // ] -IH #HL1 +@(step … HL1) -HL1 // + +/3 width=6 by lfxs_pair_repl_dx, step, inj/ + +lemma tc_lfxs_pair_repl_dx: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2,V1,V2,T. + L1.ⓑ{I}V1 ⦻**[R, T] L2.ⓑ{I}V2 → + L1.ⓑ{I}V1 ⦻**[R, T] L2.ⓑ{I}V1. + +(* does this really hold? ***************************************************) + +lemma pippo1: ∀R. s_r_confluent1 … R (lfxs R) → + s_r_transitive … R (lfxs R) → + s_r_transitive … R (tc_lfxs R). +#R #H1R #H2R @s_r_trans_LTC2 @s_r_trans_LTC1 // +qed-. + +definition s_r_confluent2: ∀A,B. relation2 (A→relation B) (B→relation A) ≝ λA,B,R1,R2. + ∀L2,T1,T2. R1 L2 T1 T2 → ∀L1. R2 T1 L1 L2 → R2 T2 L1 L2. + + +axiom s_r_conf2_LTC2: ∀R. s_r_transitive … R (lfxs R) → + s_r_confluent1 … R (lfxs R) → + s_r_confluent2 … R (tc_lfxs R). +(* +#R #H1R #H2R #L2 #T1 #T2 #HT12 #L1 #H +@(TC_ind_dx ??????? H) -L1 /3 width=3 by inj/ +#L1 #L #HL1 #HL2 #IH @(tc_lfxs_step_sn … IH) -IH // +*) + +lemma tc_lfxs_inv_zero: ∀R. s_r_confluent1 … R (lfxs R) → + s_r_transitive … R (lfxs R) → + ∀Y1,Y2. Y1 ⦻**[R, #0] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, V1] L2 & LTC … R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #H1R #H2R #Y1 #Y2 #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_zero … H) -H * + /4 width=9 by ex4_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_zero … H) -H * + [ #H #H2 * * /3 width=9 by ex4_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #HV2 #H #H2 * * + [ #H1 #H0 destruct + | #I0 #L1 #L0 #V1 #V0 #HL10 #HV10 #H1 #H0 destruct + @or_intror @ex4_5_intro [6,7: |*: /width=7/ ] + [ + | -HL2 @(trans_TC … HV10) @(pippo1 … HV2) // -V2 @pippo2 // + + lapply (H2R … HV2 … HL2) -HL2 #HL02 + /4 width=8 by ex3_5_intro, step, or_intror/ + ] + ] +] +qed-. + +(* has no meaning without the former ****************************************) + +lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & + Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. +#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * +[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ +| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg + /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +] +qed-. + +(****************************************************************************) + +lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → + ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & + Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct + /2 width=5 by ex3_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 +→ + ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * +[ #H destruct +| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. + +lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 +→ + ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * +[ #_ #H destruct +| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma deleted file mode 100644 index f063b1816..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/lfxss_etc.ma +++ /dev/null @@ -1,31 +0,0 @@ -(* -lemma lfxss_zero: ∀R,I,L1,L2,V1. L1 ⦻**[R, V1] L2 → ∀V2. - R L1 V1 V2 → L1.ⓑ{I}V1 ⦻**[R, #0] L2.ⓑ{I}V2. -#R #I #L1 #L2 #V1 #H - -elim H -L2 /3 width=5 by lfxs_zero, inj/ -#L #L2 #H0 #HL2 #IH #V2 #HV12 -lapply (IH … HV12) -IH #HL1 -@(step … HL1) -HL1 @lfxs_zero - -axiom pippo_fwd: ∀R,I,Y1,L2,V2,T. Y1 ⦻*[R, T] L2.ⓑ{I}V2 → - ∃∃L1,V1. Y1 = L1.ⓑ{I}V1. - -fact pippo: ∀R,I,L1,Y,T,V. L1.ⓑ{I}V ⦻**[R, T] Y → - ∀L2,V1. Y = L2.ⓑ{I}V1 → - ∀V2. R L1 V V2 → - L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. -#R #I #L1 #Y #T #V #H elim H -Y -[ /3 width=2 by lfxs_pair_repl_dx, inj/ -| #L #Y #_ #HL2 #IH #L2 #V1 #H #V2 #HV2 destruct - elim (pippo_fwd … HL2) #L0 #V0 #H destruct - @step [2: @(IH … HV2) // | skip ] -IH -HV2 - -lemma lfxss_pair_repl_dx: ∀R,I,L1,L2,T,V,V1. - L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V1 → - ∀V2. R L1 V V2 → - L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V2. -#R #I #L1 #L2 #T #V #V1 * #f #Hf #HL12 #V2 #HR -/3 width=5 by lexs_pair_repl, ex2_intro/ -qed-. -*) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma index 4c30dc0a9..54fdb7119 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs.ma @@ -17,53 +17,72 @@ include "basic_2/static/lfxs.ma". (* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) -definition tc_lfxs (R) (T): relation lenv ≝ TC … (lfxs R T). +definition tc_lfxs (R): term → relation lenv ≝ LTC … (lfxs R). interpretation "iterated extension on referred entries (local environment)" 'RelationStarStar R T L1 L2 = (tc_lfxs R T L1 L2). (* Basic properties *********************************************************) +lemma tc_lfxs_step_dx: ∀R,L1,L,T. L1 ⦻**[R, T] L → + ∀L2. L ⦻*[R, T] L2 → L1 ⦻**[R, T] L2. +#R #L1 #L2 #T #HL1 #L2 @step @HL1 (**) (* auto fails *) +qed-. + +lemma tc_lfxs_step_sn: ∀R,L1,L,T. L1 ⦻*[R, T] L → + ∀L2. L ⦻**[R, T] L2 → L1 ⦻**[R, T] L2. +#R #L1 #L2 #T #HL1 #L2 @TC_strap @HL1 (**) (* auto fails *) +qed-. + lemma tc_lfxs_atom: ∀R,I. ⋆ ⦻**[R, ⓪{I}] ⋆. /2 width=1 by inj/ qed. lemma tc_lfxs_sort: ∀R,I,L1,L2,V1,V2,s. L1 ⦻**[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻**[R, ⋆s] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #s #H elim H -L2 -/3 width=4 by lfxs_sort, step, inj/ +/3 width=4 by lfxs_sort, tc_lfxs_step_dx, inj/ +qed. + +lemma tc_lfxs_zero: ∀R. (∀L. reflexive … (R L)) → + ∀I,L1,L2,V. L1 ⦻**[R, V] L2 → + L1.ⓑ{I}V ⦻**[R, #0] L2.ⓑ{I}V. +#R #HR #I #L1 #L2 #V #H elim H -L2 +/3 width=5 by lfxs_zero, tc_lfxs_step_dx, inj/ qed. lemma tc_lfxs_lref: ∀R,I,L1,L2,V1,V2,i. L1 ⦻**[R, #i] L2 → L1.ⓑ{I}V1 ⦻**[R, #⫯i] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #i #H elim H -L2 -/3 width=4 by lfxs_lref, step, inj/ +/3 width=4 by lfxs_lref, tc_lfxs_step_dx, inj/ qed. lemma tc_lfxs_gref: ∀R,I,L1,L2,V1,V2,l. L1 ⦻**[R, §l] L2 → L1.ⓑ{I}V1 ⦻**[R, §l] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #l #H elim H -L2 -/3 width=4 by lfxs_gref, step, inj/ +/3 width=4 by lfxs_gref, tc_lfxs_step_dx, inj/ qed. lemma tc_lfxs_sym: ∀R. lexs_frees_confluent R cfull → (∀L1,L2,T1,T2. R L1 T1 T2 → R L2 T2 T1) → ∀T. symmetric … (tc_lfxs R T). #R #H1R #H2R #T #L1 #L2 #H elim H -L2 -/4 width=3 by lfxs_sym, TC_strap, inj/ +/4 width=3 by lfxs_sym, tc_lfxs_step_sn, inj/ qed-. lemma tc_lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T. L1 ⦻**[R1, T] L2 → L1 ⦻**[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T #H elim H -L2 -/4 width=5 by lfxs_co, step, inj/ +/4 width=5 by lfxs_co, tc_lfxs_step_dx, inj/ qed-. (* Basic inversion lemmas ***************************************************) +(* Basic_2A1: uses: TC_lpx_sn_inv_atom1 *) lemma tc_lfxs_inv_atom_sn: ∀R,I,Y2. ⋆ ⦻**[R, ⓪{I}] Y2 → Y2 = ⋆. #R #I #Y2 #H elim H -Y2 /3 width=3 by inj, lfxs_inv_atom_sn/ qed-. +(* Basic_2A1: uses: TC_lpx_sn_inv_atom2 *) lemma tc_lfxs_inv_atom_dx: ∀R,I,Y1. Y1 ⦻**[R, ⓪{I}] ⋆ → Y1 = ⋆. #R #I #Y1 #H @(TC_ind_dx ??????? H) -Y1 /3 width=3 by inj, lfxs_inv_atom_dx/ @@ -81,144 +100,76 @@ lemma tc_lfxs_inv_sort: ∀R,Y1,Y2,s. Y1 ⦻**[R, ⋆s] Y2 → | #I #L #L2 #V #V2 #HL2 #H #H2 * * [ #H1 #H0 destruct | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct - /4 width=8 by ex3_5_intro, step, or_intror/ + /4 width=8 by ex3_5_intro, tc_lfxs_step_dx, or_intror/ ] ] ] qed-. -(* -lemma tc_lfxs_inv_zero: ∀R,Y1,Y2. Y1 ⦻**[R, #0] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, V1] L2 & R L1 V1 V2 & + +lemma tc_lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻**[R, §l] Y2 → + (Y1 = ⋆ ∧ Y2 = ⋆) ∨ + ∃∃I,L1,L2,V1,V2. L1 ⦻**[R, §l] L2 & Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R #Y1 #Y2 #H elim H -Y2 -[ #Y2 #H elim (lfxs_inv_zero … H) -H * - /4 width=9 by ex4_5_intro, inj, or_introl, or_intror, conj/ -| #Y #Y2 #_ #H elim (lfxs_inv_zero … H) -H * - [ #H #H2 * * /3 width=9 by ex4_5_intro, or_introl, or_intror, conj/ - | #I #L #L2 #V #V2 #HL2 #HV2 #H #H2 * * +#R #Y1 #Y2 #l #H elim H -Y2 +[ #Y2 #H elim (lfxs_inv_gref … H) -H * + /4 width=8 by ex3_5_intro, inj, or_introl, or_intror, conj/ +| #Y #Y2 #_ #H elim (lfxs_inv_gref … H) -H * + [ #H #H2 * * /3 width=8 by ex3_5_intro, or_introl, or_intror, conj/ + | #I #L #L2 #V #V2 #HL2 #H #H2 * * [ #H1 #H0 destruct - | #I0 #L1 #L0 #V1 #V0 #HL10 #HV10 #H1 #H0 destruct - @or_intror @ex4_5_intro [6,7: |*: /width=7/ ] - - /4 width=8 by ex3_5_intro, step, or_intror/ + | #I0 #L1 #L0 #V1 #V0 #HL10 #H1 #H0 destruct + /4 width=8 by ex3_5_intro, tc_lfxs_step_dx, or_intror/ ] ] ] qed-. - - - - -#R #Y1 #Y2 * #f #H1 #H2 elim (frees_inv_zero … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_next1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=9 by ex4_5_intro, ex2_intro, or_intror/ +lemma tc_lfxs_inv_bind: ∀R. (∀L. reflexive … (R L)) → + ∀p,I,L1,L2,V,T. L1 ⦻**[R, ⓑ{p,I}V.T] L2 → + L1 ⦻**[R, V] L2 ∧ L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V. +#R #HR #p #I #L1 #L2 #V #T #H elim H -L2 +[ #L2 #H elim (lfxs_inv_bind … V ? H) -H /3 width=1 by inj, conj/ +| #L #L2 #_ #H * elim (lfxs_inv_bind … V ? H) -H /3 width=3 by tc_lfxs_step_dx, conj/ ] qed-. -lemma lfxs_inv_lref: ∀R,Y1,Y2,i. Y1 ⦻*[R, #⫯i] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, #i] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R #Y1 #Y2 #i * #f #H1 #H2 elim (frees_inv_lref … H1) -H1 * -[ #H #_ lapply (lexs_inv_atom1_aux … H2 H) -H2 /3 width=1 by or_introl, conj/ -| #I1 #L1 #V1 #g #HV1 #HY1 #Hg elim (lexs_inv_push1_aux … H2 … HY1 Hg) -H2 -Hg - /4 width=8 by ex3_5_intro, ex2_intro, or_intror/ +lemma tc_lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ⓕ{I}V.T] L2 → + L1 ⦻**[R, V] L2 ∧ L1 ⦻**[R, T] L2. +#R #I #L1 #L2 #V #T #H elim H -L2 +[ #L2 #H elim (lfxs_inv_flat … H) -H /3 width=1 by inj, conj/ +| #L #L2 #_ #H * elim (lfxs_inv_flat … H) -H /3 width=3 by tc_lfxs_step_dx, conj/ ] qed-. -lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → - (Y1 = ⋆ ∧ Y2 = ⋆) ∨ - ∃∃I,L1,L2,V1,V2. L1 ⦻*[R, §l] L2 & - Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. -#R * [ | #Y1 #I #V1 ] #Y2 #l * #f #H1 #H2 -[ lapply (lexs_inv_atom1 … H2) -H2 /3 width=1 by or_introl, conj/ -| lapply (frees_inv_gref … H1) -H1 #Hf - elim (isid_inv_gen … Hf) -Hf #g #Hg #H destruct - elim (lexs_inv_push1 … H2) -H2 #L2 #V2 #H12 #_ #H destruct - /5 width=8 by frees_gref_gen, ex3_5_intro, ex2_intro, or_intror/ -] -qed-. - -lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → - L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. -#R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf -/6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ -qed-. - -lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → - L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. -#R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf -/5 width=6 by sle_lexs_trans, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ -qed-. - (* Advanced inversion lemmas ************************************************) -lemma lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻*[R, ⋆s] Y2 → - ∃∃L2,V2. L1 ⦻*[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #s #H elim (lfxs_inv_sort … H) -H * +lemma tc_lfxs_inv_sort_pair_sn: ∀R,I,Y2,L1,V1,s. L1.ⓑ{I}V1 ⦻**[R, ⋆s] Y2 → + ∃∃L2,V2. L1 ⦻**[R, ⋆s] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #s #H elim (tc_lfxs_inv_sort … H) -H * [ #H destruct | #J #Y1 #L2 #X1 #V2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻*[R, ⋆s] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #s #H elim (lfxs_inv_sort … H) -H * +lemma tc_lfxs_inv_sort_pair_dx: ∀R,I,Y1,L2,V2,s. Y1 ⦻**[R, ⋆s] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻**[R, ⋆s] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #s #H elim (tc_lfxs_inv_sort … H) -H * [ #_ #H destruct | #J #L1 #Y2 #V1 #X2 #Hs #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_zero_pair_sn: ∀R,I,Y2,L1,V1. L1.ⓑ{I}V1 ⦻*[R, #0] Y2 → - ∃∃L2,V2. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #H elim (lfxs_inv_zero … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_zero_pair_dx: ∀R,I,Y1,L2,V2. Y1 ⦻*[R, #0] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, V1] L2 & R L1 V1 V2 & - Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #H elim (lfxs_inv_zero … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #HV1 #HV12 #H1 #H2 destruct - /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_sn: ∀R,I,Y2,L1,V1,i. L1.ⓑ{I}V1 ⦻*[R, #⫯i] Y2 → - ∃∃L2,V2. L1 ⦻*[R, #i] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #i #H elim (lfxs_inv_lref … H) -H * -[ #H destruct -| #J #Y1 #L2 #X1 #V2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_lref_pair_dx: ∀R,I,Y1,L2,V2,i. Y1 ⦻*[R, #⫯i] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, #i] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #i #H elim (lfxs_inv_lref … H) -H * -[ #_ #H destruct -| #J #L1 #Y2 #V1 #X2 #Hi #H1 #H2 destruct /2 width=4 by ex2_2_intro/ -] -qed-. - -lemma lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻*[R, §l] Y2 → - ∃∃L2,V2. L1 ⦻*[R, §l] L2 & Y2 = L2.ⓑ{I}V2. -#R #I #Y2 #L1 #V1 #l #H elim (lfxs_inv_gref … H) -H * +lemma tc_lfxs_inv_gref_pair_sn: ∀R,I,Y2,L1,V1,l. L1.ⓑ{I}V1 ⦻**[R, §l] Y2 → + ∃∃L2,V2. L1 ⦻**[R, §l] L2 & Y2 = L2.ⓑ{I}V2. +#R #I #Y2 #L1 #V1 #l #H elim (tc_lfxs_inv_gref … H) -H * [ #H destruct | #J #Y1 #L2 #X1 #V2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] qed-. -lemma lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻*[R, §l] L2.ⓑ{I}V2 → - ∃∃L1,V1. L1 ⦻*[R, §l] L2 & Y1 = L1.ⓑ{I}V1. -#R #I #Y1 #L2 #V2 #l #H elim (lfxs_inv_gref … H) -H * +lemma tc_lfxs_inv_gref_pair_dx: ∀R,I,Y1,L2,V2,l. Y1 ⦻**[R, §l] L2.ⓑ{I}V2 → + ∃∃L1,V1. L1 ⦻**[R, §l] L2 & Y1 = L1.ⓑ{I}V1. +#R #I #Y1 #L2 #V2 #l #H elim (tc_lfxs_inv_gref … H) -H * [ #_ #H destruct | #J #L1 #Y2 #V1 #X2 #Hl #H1 #H2 destruct /2 width=4 by ex2_2_intro/ ] @@ -226,35 +177,21 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf -/4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ +lemma tc_lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ②{I}V.T] L2 → L1 ⦻**[R, V] L2. +#R #I #L1 #L2 #V #T #H elim H -L2 +/3 width=5 by lfxs_fwd_pair_sn, tc_lfxs_step_dx, inj/ qed-. -lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → - R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. -#R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // +lemma tc_lfxs_fwd_bind_dx: ∀R. (∀L. reflexive … (R L)) → + ∀p,I,L1,L2,V,T. L1 ⦻**[R, ⓑ{p,I}V.T] L2 → + L1.ⓑ{I}V ⦻**[R, T] L2.ⓑ{I}V. +#R #HR #p #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_bind … H) -H // qed-. -lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // +lemma tc_lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻**[R, ⓕ{I}V.T] L2 → L1 ⦻**[R, T] L2. +#R #I #L1 #L2 #V #T #H elim (tc_lfxs_inv_flat … H) -H // qed-. -lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // -qed-. - -lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ -qed-. - -(* Basic_2A1: removed theorems 24: - llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref - llpx_sn_bind llpx_sn_flat - llpx_sn_inv_bind llpx_sn_inv_flat - llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length - llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx - llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx -*) +(* Basic_2A1: removed theorems 2: + TC_lpx_sn_inv_pair1 TC_lpx_sn_inv_pair2 *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma new file mode 100644 index 000000000..e17a1c85d --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_fqup.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfxs_fqup.ma". +include "basic_2/i_static/tc_lfxs.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +(* Advanced properties ******************************************************) + +lemma tc_lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀T. reflexive … (tc_lfxs R T). +/3 width=1 by lfxs_refl, inj/ qed. + +(* Basic_2A1: uses: TC_lpx_sn_pair TC_lpx_sn_pair_refl *) +lemma tc_lfxs_pair: ∀R. (∀L. reflexive … (R L)) → + ∀L,V1,V2. LTC … R L V1 V2 → ∀I,T. L.ⓑ{I}V1 ⦻**[R, T] L.ⓑ{I}V2. +#R #HR #L #V1 #V2 #H elim H -V2 +/3 width=3 by tc_lfxs_step_dx, lfxs_pair, inj/ +qed. + +(* Advanced eliminators *****************************************************) + +lemma tc_lfxs_ind_sn: ∀R. (∀L. reflexive … (R L)) → + ∀L1,T. ∀R0:predicate …. R0 L1 → + (∀L,L2. L1 ⦻**[R, T] L → L ⦻*[R, T] L2 → R0 L → R0 L2) → + ∀L2. L1 ⦻**[R, T] L2 → R0 L2. +#R #HR #L1 #T #R0 #HL1 #IHL1 #L2 #HL12 +@(TC_star_ind … HL1 IHL1 … HL12) /2 width=1 by lfxs_refl/ +qed-. + +lemma tc_lfxs_ind_dx: ∀R. (∀L. reflexive … (R L)) → + ∀L2,T. ∀R0:predicate …. R0 L2 → + (∀L1,L. L1 ⦻*[R, T] L → L ⦻**[R, T] L2 → R0 L → R0 L1) → + ∀L1. L1 ⦻**[R, T] L2 → R0 L1. +#R #HR #L2 #R0 #HL2 #IHL2 #L1 #HL12 +@(TC_star_ind_dx … HL2 IHL2 … HL12) /2 width=4 by lfxs_refl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_length.ma new file mode 100644 index 000000000..414acd7da --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_length.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/static/lfxs_length.ma". +include "basic_2/i_static/tc_lfxs.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +(* Forward lemmas with length for local environments ************************) + +(* Basic_2A1: uses: TC_lpx_sn_fwd_length *) +lemma tc_lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻**[R, T] L2 → |L1| = |L2|. +#R #L1 #L2 #T #H elim H -L2 +[ #L2 #HL12 >(lfxs_fwd_length … HL12) -HL12 // +| #L #L2 #_ #HL2 #IHL1 + >IHL1 -L1 >(lfxs_fwd_length … HL2) -HL2 // +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma index 8c92f3742..66196f726 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_lfpx.ma @@ -53,8 +53,7 @@ lemma lfpx_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpx h G). qed. lemma lfpx_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpx h G). -#h #G #L2 #T1 #T2 #H #L1 #HL12 @(cpxs_ind … H) -T2 -/4 width=7 by lfpx_cpx_trans, cpxs_trans, lfpx_cpxs_conf/ (**) (* lfpx_fqup slows this down *) +/3 width=6 by lfpx_cpx_conf, lfpx_cpx_trans, s_r_trans_LTC1/ qed-. (* Advanced properties ******************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma index ae3d9a889..8d066e53b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_cpxs.ma @@ -46,7 +46,7 @@ lemma csx_ind_cpxs_tdeq: ∀h,o,G,L. ∀R:predicate term. @IH -IH /3 width=3 by csx_cpxs_trans, csx_tdeq_trans/ -HT1 #V2 #HTV2 #HnTV2 lapply (tdeq_tdneq_trans … HT02 … HnTV2) -HnTV2 #H elim (tdeq_cpxs_trans … HT02 … HTV2) -T2 #V0 #HTV0 #HV02 -lapply (tndeq_tdeq_canc_dx … H … HV02) -H #HnTV0 +lapply (tdneq_tdeq_canc_dx … H … HV02) -H #HnTV0 elim (tdeq_dec h o T1 T0) #H [ lapply (tdeq_tdneq_trans … H … HnTV0) -H -HnTV0 #Hn10 lapply (cpxs_trans … HT10 … HTV0) -T0 #H10 diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma index bfee0b286..507f4d979 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs.ma @@ -13,12 +13,13 @@ (**************************************************************************) include "basic_2/notation/relations/predtysnstar_5.ma". +include "basic_2/i_static/tc_lfxs.ma". include "basic_2/rt_transition/lfpx.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) definition lfpxs: ∀h. relation4 genv term lenv lenv ≝ - λh,G,T. TC … (lfpx h G T). + λh,G. tc_lfxs (cpx h G). interpretation "uncounted parallel rt-computation on referred entries (local environment)" @@ -31,28 +32,27 @@ lemma lfpx_lfpxs: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ /2 width=1 by inj/ qed. (* Basic_2A1: was just: lpxs_strap1 *) -lemma lfpxs_strap1: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by step/ qed. +lemma lfpxs_step_dx: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_step_dx/ qed. (* Basic_2A1: was just: lpxs_strap2 *) -lemma lfpxs_strap2: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. -/2 width=3 by TC_strap/ qed. -(* -(* Basic_2A1: was just: lpxs_pair_refl *) -lemma lfpxs_pair_refl: ∀h,G,T,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → ∀I,V. ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. -/2 width=1 by TC_lpx_sn_pair_refl/ qed. +lemma lfpxs_step_sn: ∀h,G,T,L1,L,L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_step_sn/ qed. (* Basic inversion lemmas ***************************************************) -(* Basic_2A1: was just: lpxs_inv_atom1 *) -lemma lfpxs_inv_atom1: ∀h,G,L2.T. ⦃G, ⋆⦄ ⊢ ⬈*[h, T] L2 → L2 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom1/ qed-. +(* Basic_2A1: uses: lpxs_inv_atom1 *) +lemma lfpxs_inv_atom1: ∀h,I,G,L2. ⦃G, ⋆⦄ ⊢ ⬈*[h, ⓪{I}] L2 → L2 = ⋆. +/2 width=3 by tc_lfxs_inv_atom_sn/ qed-. -(* Basic_2A1: was just: lpxs_inv_atom2 *) -lemma lfpxs_inv_atom2: ∀h,G,L1,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] ⋆ → L1 = ⋆. -/2 width=2 by TC_lpx_sn_inv_atom2/ qed-. -*) +(* Basic_2A1: uses: lpxs_inv_atom2 *) +lemma lfpxs_inv_atom2: ∀h,I,G,L1. ⦃G, L1⦄ ⊢ ⬈*[h, ⓪{I}] ⋆ → L1 = ⋆. +/2 width=3 by tc_lfxs_inv_atom_dx/ qed-. -(* Basic_2A1: removed theorems 1: - lpxs_pair -*) +(* Basic forward lemmas *****************************************************) + +lemma lfpxs_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, V] L2. +/2 width=3 by tc_lfxs_fwd_pair_sn/ qed-. + +lemma lfpxs_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. +/2 width=3 by tc_lfxs_fwd_flat_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma index e5e5ea562..898aac863 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_cpxs.ma @@ -19,18 +19,18 @@ include "basic_2/rt_computation/lfpxs_fqup.ma". (* Properties with uncounted context-sensitive rt-computation for terms *****) +(* Basic_2A1: uses: lpxs_pair lpxs_pair_refl *) lemma lfpxs_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈*[h] V2 → ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈*[h, T] L.ⓑ{I}V2. -#h #G #L #V1 #V2 #H @(cpxs_ind … H) -V2 -/3 width=3 by lfpxs_strap1, lfpx_pair/ -qed. +/2 width=1 by tc_lfxs_pair/ qed. -(* Basic_2A1: was just: lpxs_cpx_trans *) +(* Basic_2A1: uses: lpxs_cpx_trans *) lemma lfpxs_cpx_trans: ∀h,G. s_r_transitive … (cpx h G) (lfpxs h G). -/3 width=5 by s_r_trans_LTC2, lfpx_cpxs_trans/ qed-. +#h #G @s_r_trans_LTC2 @lfpx_cpxs_trans (**) (* auto fails *) +qed-. (* Note: lfpxs_cpx_conf does not hold, thus we cannot invoke s_r_trans_LTC1 *) -(* Basic_2A1: was just: lpxs_cpxs_trans *) +(* Basic_2A1: uses: lpxs_cpxs_trans *) lemma lfpxs_cpxs_trans: ∀h,G. s_rs_transitive … (cpx h G) (lfpxs h G). #h #G @s_r_to_s_rs_trans @s_r_trans_LTC2 @s_rs_trans_TC1 /2 width=3 by lfpx_cpxs_trans/ (**) (* full auto too slow *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma index ce2496b91..52159d8cd 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqup.ma @@ -12,31 +12,35 @@ (* *) (**************************************************************************) -include "basic_2/rt_transition/lfpx_fqup.ma". +include "basic_2/i_static/tc_lfxs_fqup.ma". include "basic_2/rt_computation/lfpxs.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) +(* Advanced properties ******************************************************) + +(* Basic_2A1: uses: lpxs_refl *) +lemma lfpxs_refl: ∀h,G,T. reflexive … (lfpxs h G T). +/2 width=1 by tc_lfxs_refl/ qed. + +(* Advanced forward lemmas **************************************************) + +lemma lfpxs_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈*[h, T] L2.ⓑ{I}V. +/2 width=2 by tc_lfxs_fwd_bind_dx/ qed-. + (* Advanced eliminators *****************************************************) -(* Basic_2A1: was just: lpxs_ind *) -lemma lfpxs_ind: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → - (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → - ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. -#h #G #L1 #T #R #HL1 #IHL1 #L2 #HL12 -@(TC_star_ind … HL1 IHL1 … HL12) // -qed-. +(* Basic_2A1: uses: lpxs_ind *) +lemma lfpxs_ind_sn: ∀h,G,L1,T. ∀R:predicate lenv. R L1 → + (∀L,L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L → ⦃G, L⦄ ⊢ ⬈[h, T] L2 → R L → R L2) → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L2. +#h #G @tc_lfxs_ind_sn // (**) (* auto fails *) +qed-. -(* Basic_2A1: was just: lpxs_ind_dx *) +(* Basic_2A1: uses: lpxs_ind_dx *) lemma lfpxs_ind_dx: ∀h,G,L2,T. ∀R:predicate lenv. R L2 → (∀L1,L. ⦃G, L1⦄ ⊢ ⬈[h, T] L → ⦃G, L⦄ ⊢ ⬈*[h, T] L2 → R L → R L1) → ∀L1. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → R L1. -#h #o #G #L2 #R #HL2 #IHL2 #L1 #HL12 -@(TC_star_ind_dx … HL2 IHL2 … HL12) // -qed-. - -(* Advanced properties ******************************************************) - -(* Basic_2A1: was just: lpxs_refl *) -lemma lfpxs_refl: ∀h,G,L,T. ⦃G, L⦄ ⊢ ⬈*[h, T] L. -/2 width=1 by lfpx_lfpxs/ qed. +#h #G @tc_lfxs_ind_dx // (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma index 17e063b6d..dd559526f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_fqus.ma @@ -56,3 +56,66 @@ lemma lpxs_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2 #L #T3 #HT3 #HT32 #HL2 elim (fqus_cpxs_trans … HT3 … HT0) -T /3 width=7 by cpxs_trans, fqus_strap1, ex3_2_intro/ qed-. + +lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #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 // + #K1 #H #H2KL1 lapply (drop_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) + | elim (lleq_inv_flat … H) + ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ +| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H + /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ +| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H + /2 width=4 by fqu_flat_dx, ex3_intro/ +| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 + elim (drop_O1_le (Ⓕ) (k+1) K1) + [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // + #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1 + #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct + /3 width=4 by fqu_drop, ex3_intro/ + | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o + lapply (lleq_fwd_length … H2KL1) // + ] +] +qed-. + +lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fquq_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fquq, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqu_fqup, ex3_intro/ +| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 + #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L + /3 width=5 by fqup_strap1, ex3_intro/ +] +qed-. + +lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → + ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 +elim (fqus_inv_gen … H) -H +[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 + /3 width=4 by fqup_fqus, ex3_intro/ +| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma index ac2f64dc5..ce1bb6d13 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_length.ma @@ -1,7 +1,24 @@ -(* Basic forward lemmas *****************************************************) +(**************************************************************************) +(* ___ *) +(* ||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/i_static/tc_lfxs_length.ma". +include "basic_2/rt_computation/lfpxs.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) (* Forward lemmas with length for local environments ************************) -(* Basic_2A1: was just: lpxs_fwd_length *) -lemma lfpxs_fwd_length: ∀h,o,G,L1,L2. ⦃G, L1⦄ ⊢ ⬈*[h, o] L2 → |L1| = |L2|. -/2 width=2 by TC_lpx_sn_fwd_length/ qed-. +(* Basic_2A1: uses: lpxs_fwd_length *) +lemma lfpxs_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → |L1| = |L2|. +/2 width=3 by tc_lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma new file mode 100644 index 000000000..9389dd099 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfdeq.ma @@ -0,0 +1,48 @@ +(**************************************************************************) +(* ___ *) +(* ||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/static/lfdeq_lfdeq.ma". +include "basic_2/rt_transition/lfpx_lfdeq.ma". +include "basic_2/rt_computation/lfpxs_fqup.ma". + +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) + +(* Properties with degree-based equivalence on referred entries *************) + +(* Basic_2A1: was: lleq_lpxs_trans *) +lemma lfdeq_lfpxs_trans: ∀h,o,G,L2,K2,T. ⦃G, L2⦄ ⊢ ⬈*[h, T] K2 → + ∀L1. L1 ≡[h, o, T] L2 → + ∃∃K1. ⦃G, L1⦄ ⊢ ⬈*[h, T] K1 & K1 ≡[h, o, T] K2. +#h #o #G #L2 #K2 #T #H @(lfpxs_ind_sn … H) -K2 /2 width=3 by ex2_intro/ +#K #K2 #_ #HK2 #IH #L1 #HT elim (IH … HT) -L2 +#L #HL1 #HT elim (lfdeq_lfpx_trans … HK2 … HT) -K +/3 width=3 by lfpxs_step_dx, ex2_intro/ +qed-. + +(* Basic_2A1: was: lpxs_nlleq_inv_step_sn *) +lemma lfpxs_lfdneq_inv_step_sn: ∀h,o,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → + ∃∃L,L0. ⦃G, L1⦄ ⊢ ⬈[h, T] L & L1 ≡[h, o, T] L → ⊥ & ⦃G, L⦄ ⊢ ⬈*[h, T] L0 & L0 ≡[h, o, T] L2. +#h #o #G #L1 #L2 #T #H @(lfpxs_ind_dx … H) -L1 +[ #H elim H -H // +| #L1 #L #H1 #H2 #IH2 #H12 elim (lfdeq_dec h o L1 L T) #H + [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lfdeq_trans/ -H12 + #L0 #L3 #H1 #H2 #H3 #H4 lapply (lfdeq_lfdneq_trans … H … H2) -H2 + #H2 elim (lfdeq_lfpx_trans … H1 … H) -L + #L #H1 #H lapply (lfdneq_lfdeq_div … H … H2) -H2 + #H2 elim (lfdeq_lfpxs_trans … H3 … H) -L0 + /3 width=8 by lfdeq_trans, ex4_2_intro/ + | -H12 -IH2 /3 width=6 by ex4_2_intro/ + ] +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma similarity index 78% rename from matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma rename to matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma index 2e0c14570..e2a5ee4d9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma @@ -12,11 +12,13 @@ (* *) (**************************************************************************) -include "basic_2/computation/lpxs.ma". +include "basic_2/rt_computation/lfpxs.ma". -(* SN EXTENDED PARALLEL COMPUTATION ON LOCAL ENVIRONMENTS *******************) +(* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) (* Main properties **********************************************************) -theorem lpxs_trans: ∀h,o,G. Transitive … (lpxs h o G). -/2 width=3 by trans_TC/ qed-. +(* Basic_2A1: uses: lpxs_trans *) +theorem lfpxs_trans: ∀h,G,T. Transitive … (lfpxs h G T). +#h #G #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma index 2311f424c..24fa630b6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx.ma @@ -27,7 +27,7 @@ interpretation (* Basic eliminators ********************************************************) -(* Basic_2A1: was: lsx_ind *) +(* Basic_2A1: uses: lsx_ind *) lemma lfsx_ind: ∀h,o,G,T. ∀R:predicate lenv. (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → @@ -40,13 +40,13 @@ qed-. (* Basic properties *********************************************************) -(* Basic_2A1: was: lsx_intro *) +(* Basic_2A1: uses: lsx_intro *) lemma lfsx_intro: ∀h,o,G,L1,T. (∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. /5 width=1 by lfdeq_sym, SN_intro/ qed. -(* Basic_2A1: was: lsx_sort *) +(* Basic_2A1: uses: lsx_sort *) lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_sort … H) -H * @@ -56,7 +56,7 @@ lemma lfsx_sort: ∀h,o,G,L,s. G ⊢ ⬈*[h, o, ⋆s] 𝐒⦃L⦄. ] qed. -(* Basic_2A1: was: lsx_gref *) +(* Basic_2A1: uses: lsx_gref *) lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. #h #o #G #L1 #s @lfsx_intro #L2 #H #Hs elim Hs -Hs elim (lfpx_inv_gref … H) -H * @@ -66,6 +66,7 @@ lemma lfsx_gref: ∀h,o,G,L,p. G ⊢ ⬈*[h, o, §p] 𝐒⦃L⦄. ] qed. -(* Basic_2A1: removed theorems 2: +(* Basic_2A1: removed theorems 9: lsx_ge_up lsx_ge + lsxa_ind lsxa_intro lsxa_lleq_trans lsxa_lpxs_trans lsxa_intro_lpx lsx_lsxa lsxa_inv_lsx *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma index 10bcdd59c..e9879a17c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_fqup.ma @@ -19,7 +19,7 @@ include "basic_2/rt_computation/lfsx.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: was: lsx_atom *) +(* Basic_2A1: uses: lsx_atom *) lemma lfsx_atom: ∀h,o,G,T. G ⊢ ⬈*[h, o, T] 𝐒⦃⋆⦄. #h #o #G #T @lfsx_intro #Y #H #HI lapply (lfpx_inv_atom_sn … H) -H diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma new file mode 100644 index 000000000..d1e4f4de8 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfpxs.ma @@ -0,0 +1,123 @@ +(**************************************************************************) +(* ___ *) +(* ||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/rt_computation/lfpxs_lfdeq.ma". +include "basic_2/rt_computation/lfpxs_cpxs.ma". +include "basic_2/rt_computation/lfpxs_lfpxs.ma". +include "basic_2/rt_computation/lfsx_lfsx.ma". + +(* STRONGLY NORMALIZING LOCAL ENV.S FOR UNCOUNTED PARALLEL RT-TRANSITION ****) + +(* Properties with uncounted rt-computation on referred entries *************) + +(* Basic_2A1: uses: lsx_intro_alt *) +lemma lfsx_intro_lfpxs: ∀h,o,G,L1,T. + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄) → + G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄. +/4 width=1 by lfpx_lfpxs, lfsx_intro/ qed-. + +(* Basic_2A1: uses: lsx_lpxs_trans *) +lemma lfsx_lfpxs_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. +#h #o #G #L1 #T #HL1 #L2 #H @(lfpxs_ind … H) -L2 +/2 width=3 by lfsx_lfpx_trans/ +qed-. + +(* Eliminators with uncounted rt-computation on referred entries ************) + +lemma lfsx_ind_lfpxs_lfdeq: ∀h,o,G,T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + ∀L0. ⦃G, L1⦄ ⊢ ⬈*[h, T] L0 → ∀L2. L0 ≡[h, o, T] L2 → R L2. +#h #o #G #T #R #IH #L1 #H @(lfsx_ind … H) -L1 +#L1 #HL1 #IH1 #L0 #HL10 #L2 #HL02 +@IH -IH /3 width=3 by lfsx_lfpxs_trans, lfsx_lfdeq_trans/ -HL1 #K2 #HLK2 #HnLK2 +lapply (lfdeq_lfdneq_trans … HL02 … HnLK2) -HnLK2 #H +elim (lfdeq_lfpxs_trans … HLK2 … HL02) -L2 #K0 #HLK0 #HK02 +lapply (lfdneq_lfdeq_canc_dx … H … HK02) -H #HnLK0 +elim (lfdeq_dec h o L1 L0 T) #H +[ lapply (lfdeq_lfdneq_trans … H … HnLK0) -H -HnLK0 #Hn10 + lapply (lfpxs_trans … HL10 … HLK0) -L0 #H10 + elim (lfpxs_lfdneq_inv_step_sn … H10 … Hn10) -H10 -Hn10 + /3 width=8 by lfdeq_trans/ +| elim (lfpxs_lfdneq_inv_step_sn … HL10 … H) -HL10 -H #L #K #HL1 #HnL1 #HLK #HKL0 + elim (lfdeq_lfpxs_trans … HLK0 … HKL0) -L0 + /3 width=8 by lfpxs_trans, lfdeq_trans/ +] +qed-. + +(* Basic_2A1: uses: lsx_ind_alt *) +lemma lfsx_ind_lfpxs: ∀h,o,G,T. ∀R:predicate lenv. + (∀L1. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → + (∀L2. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → (L1 ≡[h, o, T] L2 → ⊥) → R L2) → + R L1 + ) → + ∀L. G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄ → R L. +#h #o #G #T #R #IH #L #HL +@(lfsx_ind_lfpxs_lfdeq … IH … HL) -IH -HL // (**) (* full auto fails *) +qed-. + +(* Advanced properties ******************************************************) + +fact lsx_bind_lpxs_aux: ∀h,o,p,I,G,L1,V. G ⊢ ⬈*[h, o, V] 𝐒⦃L1⦄ → + ∀Y,T. G ⊢ ⬈*[h, o, T] 𝐒⦃Y⦄ → + ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ⬈*[h, ⓑ{p,I}V.T] L2 → + G ⊢ ⬈*[h, o, ⓑ{p,I}V.T] 𝐒⦃L2⦄. +#h #o #p #I #G #L1 #V #H @(lfsx_ind_lfpxs … H) -L1 +#L1 #HL1 #IHL1 #Y #T #H @(lfsx_ind_lfpxs … H) -Y +#Y #HY #IHY #L2 #H #HL12 destruct @lfsx_intro_lfpxs +#L0 #HL20 lapply (lfpxs_trans … HL12 … HL20) +#HL10 #H elim (lfdneq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ] +[ #HnV elim (lfdeq_dec h o L1 L2 V) + [ #HV @(IHL1 … L0) -IHL1 + [2: /3 width=5 by lfdeq_canc_sn/ + |5: // |3: skip + |6: // + + lfdeq_lfdneq_trans/ + + /3 width=5 by lfsx_lfpxs_trans, lfpxs_pair, lfdeq_canc_sn/ (**) (* full auto too slow *) + | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/ + ] +| /3 width=4 by lpxs_pair/ +] +qed-. + +lemma lsx_bind: ∀h,o,a,I,G,L,V,l. G ⊢ ⬈*[h, o, V, l] L → + ∀T. G ⊢ ⬈*[h, o, T, ⫯l] L.ⓑ{I}V → + G ⊢ ⬈*[h, o, ⓑ{a,I}V.T, l] L. +/2 width=3 by lsx_bind_lpxs_aux/ qed. + +lemma lsx_flat_lpxs: ∀h,o,I,G,L1,V,l. G ⊢ ⬈*[h, o, V, l] L1 → + ∀L2,T. G ⊢ ⬈*[h, o, T, l] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, o] L2 → + G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L2. +#h #o #I #G #L1 #V #l #H @(lsx_ind_lfpxs … H) -L1 +#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind_lfpxs … H) -L2 +#L2 #HL2 #IHL2 #HL12 @lsx_intro_lfpxs +#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) +#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ] +[ #HnV elim (lleq_dec V L1 L2 l) + [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *) + | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/ + ] +| /3 width=1 by/ +] +qed-. + +lemma lsx_flat: ∀h,o,I,G,L,V,l. G ⊢ ⬈*[h, o, V, l] L → + ∀T. G ⊢ ⬈*[h, o, T, l] L → G ⊢ ⬈*[h, o, ⓕ{I}V.T, l] L. +/2 width=3 by lsx_flat_lpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma index 7e1d5cffb..9664ec0a3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfsx_lfsx.ma @@ -20,7 +20,7 @@ include "basic_2/rt_computation/lfsx.ma". (* Advanced properties ******************************************************) -(* Basic_2A1: was just: lsx_lleq_trans *) +(* Basic_2A1: uses: lsx_lleq_trans *) lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → ∀L2. L1 ≡[h, o, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. #h #o #G #L1 #T #H @(lfsx_ind … H) -L1 @@ -29,7 +29,7 @@ lemma lfsx_lfdeq_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → /4 width=5 by lfdeq_repl/ qed-. -(* Basic_2A1: was: lsx_lpx_trans *) +(* Basic_2A1: uses: lsx_lpx_trans *) lemma lfsx_lfpx_trans: ∀h,o,G,L1,T. G ⊢ ⬈*[h, o, T] 𝐒⦃L1⦄ → ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → G ⊢ ⬈*[h, o, T] 𝐒⦃L2⦄. #h #o #G #L1 #T #H @(lfsx_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 @@ -38,8 +38,7 @@ qed-. (* Advanced forward lemmas **************************************************) -(* Basic_2A1: includes: lsx_fwd_bind_sn lsx_fwd_flat_sn *) -(* Basic_2A1: was: lsx_fwd_pair_sn *) +(* Basic_2A1: uses: lsx_fwd_pair_sn lsx_fwd_bind_sn lsx_fwd_flat_sn *) lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄. #h #o #I #G #L #V #T #H @(lfsx_ind … H) -L @@ -48,7 +47,7 @@ lemma lfsx_fwd_pair_sn: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ②{I}V.T] 𝐒⦃L /6 width=4 by lfsx_lfdeq_trans, lfdeq_trans, lfdeq_fwd_pair_sn/ qed-. -(* Basic_2A1: was: lsx_fwd_flat_dx *) +(* Basic_2A1: uses: lsx_fwd_flat_dx *) lemma lfsx_fwd_flat_dx: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. #h #o #I #G #L #V #T #H @(lfsx_ind … H) -L @@ -59,7 +58,7 @@ qed-. (* Advanced inversion lemmas ************************************************) -(* Basic_2A1: was: lsx_inv_flat *) +(* Basic_2A1: uses: lsx_inv_flat *) lemma lfsx_inv_flat: ∀h,o,I,G,L,V,T. G ⊢ ⬈*[h, o, ⓕ{I}V.T] 𝐒⦃L⦄ → G ⊢ ⬈*[h, o, V] 𝐒⦃L⦄ ∧ G ⊢ ⬈*[h, o, T] 𝐒⦃L⦄. /3 width=3 by lfsx_fwd_pair_sn, lfsx_fwd_flat_dx, conj/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma deleted file mode 100644 index 159c84f81..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lpxs_lleq.ma +++ /dev/null @@ -1,141 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/multiple/lleq_lleq.ma". -include "basic_2/reduction/lpx_lleq.ma". -include "basic_2/computation/cpxs_lreq.ma". -include "basic_2/computation/lpxs_drop.ma". -include "basic_2/computation/lpxs_cpxs.ma". - -(* SN EXTENDED PARALLEL COMPUTATION FOR LOCAL ENVIRONMENTS ******************) - -(* Properties on lazy equivalence for local environments ********************) - -lemma lleq_lpxs_trans: ∀h,o,G,L2,K2. ⦃G, L2⦄ ⊢ ➡*[h, o] K2 → - ∀L1,T,l. L1 ≡[T, l] L2 → - ∃∃K1. ⦃G, L1⦄ ⊢ ➡*[h, o] K1 & K1 ≡[T, l] K2. -#h #o #G #L2 #K2 #H @(lpxs_ind … H) -K2 /2 width=3 by ex2_intro/ -#K #K2 #_ #HK2 #IH #L1 #T #l #HT elim (IH … HT) -L2 -#L #HL1 #HT elim (lleq_lpx_trans … HK2 … HT) -K -/3 width=3 by lpxs_strap1, ex2_intro/ -qed-. - -lemma lpxs_nlleq_inv_step_sn: ∀h,o,G,L1,L2,T,l. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → - ∃∃L,L0. ⦃G, L1⦄ ⊢ ➡[h, o] L & L1 ≡[T, l] L → ⊥ & ⦃G, L⦄ ⊢ ➡*[h, o] L0 & L0 ≡[T, l] L2. -#h #o #G #L1 #L2 #T #l #H @(lpxs_ind_dx … H) -L1 -[ #H elim H -H // -| #L1 #L #H1 #H2 #IH2 #H12 elim (lleq_dec T L1 L l) #H - [ -H1 -H2 elim IH2 -IH2 /3 width=3 by lleq_trans/ -H12 - #L0 #L3 #H1 #H2 #H3 #H4 lapply (lleq_nlleq_trans … H … H2) -H2 - #H2 elim (lleq_lpx_trans … H1 … H) -L - #L #H1 #H lapply (nlleq_lleq_div … H … H2) -H2 - #H2 elim (lleq_lpxs_trans … H3 … H) -L0 - /3 width=8 by lleq_trans, ex4_2_intro/ - | -H12 -IH2 /3 width=6 by ex4_2_intro/ - ] -] -qed-. - -lemma lpxs_lleq_fqu_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #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 // - #K1 #H #H2KL1 lapply (drop_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) - | elim (lleq_inv_flat … H) - ] -H /2 width=4 by fqu_pair_sn, ex3_intro/ -| #a #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_bind_O … H) -H - /3 width=4 by lpxs_pair, fqu_bind_dx, ex3_intro/ -| #I #G1 #L1 #V1 #T1 #K1 #HLK1 #H elim (lleq_inv_flat … H) -H - /2 width=4 by fqu_flat_dx, ex3_intro/ -| #G1 #L1 #L #T1 #U1 #k #HL1 #HTU1 #K1 #H1KL1 #H2KL1 - elim (drop_O1_le (Ⓕ) (k+1) K1) - [ #K #HK1 lapply (lleq_inv_lift_le … H2KL1 … HK1 HL1 … HTU1 ?) -H2KL1 // - #H2KL elim (lpxs_drop_trans_O1 … H1KL1 … HL1) -L1 - #K0 #HK10 #H1KL lapply (drop_mono … HK10 … HK1) -HK10 #H destruct - /3 width=4 by fqu_drop, ex3_intro/ - | lapply (drop_fwd_length_le2 … HL1) -L -T1 -o - lapply (lleq_fwd_length … H2KL1) // - ] -] -qed-. - -lemma lpxs_lleq_fquq_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐⸮ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fquq_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fquq, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqup_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐+ ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -[ #G2 #L2 #T2 #H #K1 #H1KL1 #H2KL1 elim (lpxs_lleq_fqu_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqu_fqup, ex3_intro/ -| #G #G2 #L #L2 #T #T2 #_ #HT2 #IHT1 #K1 #H1KL1 #H2KL1 elim (IHT1 … H2KL1) // -L1 - #K #HT1 #H1KL #H2KL elim (lpxs_lleq_fqu_trans … HT2 … H1KL H2KL) -L - /3 width=5 by fqup_strap1, ex3_intro/ -] -qed-. - -lemma lpxs_lleq_fqus_trans: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀K1. ⦃G1, K1⦄ ⊢ ➡*[h, o] L1 → K1 ≡[T1, 0] L1 → - ∃∃K2. ⦃G1, K1, T1⦄ ⊐* ⦃G2, K2, T2⦄ & ⦃G2, K2⦄ ⊢ ➡*[h, o] L2 & K2 ≡[T2, 0] L2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H #K1 #H1KL1 #H2KL1 -elim (fqus_inv_gen … H) -H -[ #H elim (lpxs_lleq_fqup_trans … H … H1KL1 H2KL1) -L1 - /3 width=4 by fqup_fqus, ex3_intro/ -| * #HG #HL #HT destruct /2 width=4 by ex3_intro/ -] -qed-. - -fact lreq_lpxs_trans_lleq_aux: ∀h,o,G,L1,L0,l,k. L1 ⩬[l, k] L0 → k = ∞ → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → - ∃∃L. L ⩬[l, k] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & - (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). -#h #o #G #L1 #L0 #l #k #H elim H -L1 -L0 -l -k -[ #l #k #_ #L2 #H >(lpxs_inv_atom1 … H) -H - /3 width=5 by ex3_intro, conj/ -| #I1 #I0 #L1 #L0 #V1 #V0 #_ #_ #Hm destruct -| #I #L1 #L0 #V1 #k #HL10 #IHL10 #Hm #Y #H - elim (lpxs_inv_pair1 … H) -H #L2 #V2 #HL02 #HV02 #H destruct - lapply (ysucc_inv_Y_dx … Hm) -Hm #Hm - elim (IHL10 … HL02) // -IHL10 -HL02 #L #HL2 #HL1 #IH - @(ex3_intro … (L.ⓑ{I}V2)) /3 width=3 by lpxs_pair, lreq_cpxs_trans, lreq_pair/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_pair_O_Y/ -| #I1 #I0 #L1 #L0 #V1 #V0 #l #k #HL10 #IHL10 #Hm #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, lreq_succ/ - #T elim (IH T) #HL0dx #HL0sn - @conj #H @(lleq_lreq_repl … H) -H /3 width=1 by lreq_sym, lreq_succ/ -] -qed-. - -lemma lreq_lpxs_trans_lleq: ∀h,o,G,L1,L0,l. L1 ⩬[l, ∞] L0 → - ∀L2. ⦃G, L0⦄ ⊢ ➡*[h, o] L2 → - ∃∃L. L ⩬[l, ∞] L2 & ⦃G, L1⦄ ⊢ ➡*[h, o] L & - (∀T. L0 ≡[T, l] L2 ↔ L1 ≡[T, l] L). -/2 width=1 by lreq_lpxs_trans_lleq_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma deleted file mode 100644 index 07f3d94b2..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_alt.ma +++ /dev/null @@ -1,115 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/notation/relations/snalt_6.ma". -include "basic_2/computation/lpxs_lleq.ma". -include "basic_2/computation/lsx.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* alternative definition of lsx *) -definition lsxa: ∀h. sd h → relation4 ynat term genv lenv ≝ - λh,o,l,T,G. SN … (lpxs h o G) (lleq l T). - -interpretation - "extended strong normalization (local environment) alternative" - 'SNAlt h o l T G L = (lsxa h o T l G L). - -(* Basic eliminators ********************************************************) - -lemma lsxa_ind: ∀h,o,G,T,l. ∀R:predicate lenv. - (∀L1. G ⊢ ⬊⬊*[h, o, T, l] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → R L2) → - R L1 - ) → - ∀L. G ⊢ ⬊⬊*[h, o, T, l] L → R L. -#h #o #G #T #l #R #H0 #L1 #H elim H -L1 -/5 width=1 by lleq_sym, SN_intro/ -qed-. - -(* Basic properties *********************************************************) - -lemma lsxa_intro: ∀h,o,G,L1,T,l. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊⬊*[h, o, T, l] L2) → - G ⊢ ⬊⬊*[h, o, T, l] L1. -/5 width=1 by lleq_sym, SN_intro/ qed. - -fact lsxa_intro_aux: ∀h,o,G,L1,T,l. - (∀L,L2. ⦃G, L⦄ ⊢ ➡*[h, o] L2 → L1 ≡[T, l] L → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊⬊*[h, o, T, l] L2) → - G ⊢ ⬊⬊*[h, o, T, l] L1. -/4 width=3 by lsxa_intro/ qed-. - -lemma lsxa_lleq_trans: ∀h,o,T,G,L1,l. G ⊢ ⬊⬊*[h, o, T, l] L1 → - ∀L2. L1 ≡[T, l] L2 → G ⊢ ⬊⬊*[h, o, T, l] L2. -#h #o #T #G #L1 #l #H @(lsxa_ind … H) -L1 -#L1 #_ #IHL1 #L2 #HL12 @lsxa_intro -#K2 #HLK2 #HnLK2 elim (lleq_lpxs_trans … HLK2 … HL12) -HLK2 -/5 width=4 by lleq_canc_sn, lleq_trans/ -qed-. - -lemma lsxa_lpxs_trans: ∀h,o,T,G,L1,l. G ⊢ ⬊⬊*[h, o, T, l] L1 → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → G ⊢ ⬊⬊*[h, o, T, l] L2. -#h #o #T #G #L1 #l #H @(lsxa_ind … H) -L1 #L1 #HL1 #IHL1 #L2 #HL12 -elim (lleq_dec T L1 L2 l) /3 width=4 by lsxa_lleq_trans/ -qed-. - -lemma lsxa_intro_lpx: ∀h,o,G,L1,T,l. - (∀L2. ⦃G, L1⦄ ⊢ ➡[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊⬊*[h, o, T, l] L2) → - G ⊢ ⬊⬊*[h, o, T, l] L1. -#h #o #G #L1 #T #l #IH @lsxa_intro_aux -#L #L2 #H @(lpxs_ind_dx … H) -L -[ #H destruct #H elim H // -| #L0 #L elim (lleq_dec T L1 L l) /3 width=1 by/ - #HnT #HL0 #HL2 #_ #HT #_ elim (lleq_lpx_trans … HL0 … HT) -L0 - #L0 #HL10 #HL0 @(lsxa_lpxs_trans … HL2) -HL2 - /5 width=3 by lsxa_lleq_trans, lleq_trans/ -] -qed-. - -(* Main properties **********************************************************) - -theorem lsx_lsxa: ∀h,o,G,L,T,l. G ⊢ ⬊*[h, o, T, l] L → G ⊢ ⬊⬊*[h, o, T, l] L. -#h #o #G #L #T #l #H @(lsx_ind … H) -L -/4 width=1 by lsxa_intro_lpx/ -qed. - -(* Main inversion lemmas ****************************************************) - -theorem lsxa_inv_lsx: ∀h,o,G,L,T,l. G ⊢ ⬊⬊*[h, o, T, l] L → G ⊢ ⬊*[h, o, T, l] L. -#h #o #G #L #T #l #H @(lsxa_ind … H) -L -/4 width=1 by lsx_intro, lpx_lpxs/ -qed-. - -(* Advanced properties ******************************************************) - -lemma lsx_intro_alt: ∀h,o,G,L1,T,l. - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → G ⊢ ⬊*[h, o, T, l] L2) → - G ⊢ ⬊*[h, o, T, l] L1. -/6 width=1 by lsxa_inv_lsx, lsx_lsxa, lsxa_intro/ qed. - -lemma lsx_lpxs_trans: ∀h,o,G,L1,T,l. G ⊢ ⬊*[h, o, T, l] L1 → - ∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → G ⊢ ⬊*[h, o, T, l] L2. -/4 width=3 by lsxa_inv_lsx, lsx_lsxa, lsxa_lpxs_trans/ qed-. - -(* Advanced eliminators *****************************************************) - -lemma lsx_ind_alt: ∀h,o,G,T,l. ∀R:predicate lenv. - (∀L1. G ⊢ ⬊*[h, o, T, l] L1 → - (∀L2. ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → (L1 ≡[T, l] L2 → ⊥) → R L2) → - R L1 - ) → - ∀L. G ⊢ ⬊*[h, o, T, l] L → R L. -#h #o #G #T #l #R #IH #L #H @(lsxa_ind h o G T l … L) -/4 width=1 by lsxa_inv_lsx, lsx_lsxa/ -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma deleted file mode 100644 index 2e6da2ed4..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lsx_lpxs.ma +++ /dev/null @@ -1,62 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||M|| *) -(* ||A|| A project by Andrea Asperti *) -(* ||T|| *) -(* ||I|| Developers: *) -(* ||T|| The HELM team. *) -(* ||A|| http://helm.cs.unibo.it *) -(* \ / *) -(* \ / This file is distributed under the terms of the *) -(* v GNU General Public License Version 2 *) -(* *) -(**************************************************************************) - -include "basic_2/computation/lpxs_lpxs.ma". -include "basic_2/computation/lsx_alt.ma". - -(* SN EXTENDED STRONGLY NORMALIZING LOCAL ENVIRONMENTS **********************) - -(* Advanced properties ******************************************************) - -fact lsx_bind_lpxs_aux: ∀h,o,a,I,G,L1,V,l. G ⊢ ⬊*[h, o, V, l] L1 → - ∀Y,T. G ⊢ ⬊*[h, o, T, ⫯l] Y → - ∀L2. Y = L2.ⓑ{I}V → ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - G ⊢ ⬊*[h, o, ⓑ{a,I}V.T, l] L2. -#h #o #a #I #G #L1 #V #l #H @(lsx_ind_alt … H) -L1 -#L1 #HL1 #IHL1 #Y #T #H @(lsx_ind_alt … H) -Y -#Y #HY #IHY #L2 #H #HL12 destruct @lsx_intro_alt -#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) -#HL10 #H elim (nlleq_inv_bind … H) -H [ -HL1 -IHY | -HY -IHL1 ] -[ #HnV elim (lleq_dec V L1 L2 l) - [ #HV @(IHL1 … L0) /3 width=5 by lsx_lpxs_trans, lpxs_pair, lleq_canc_sn/ (**) (* full auto too slow *) - | -HnV -HL10 /4 width=5 by lsx_lpxs_trans, lpxs_pair/ - ] -| /3 width=4 by lpxs_pair/ -] -qed-. - -lemma lsx_bind: ∀h,o,a,I,G,L,V,l. G ⊢ ⬊*[h, o, V, l] L → - ∀T. G ⊢ ⬊*[h, o, T, ⫯l] L.ⓑ{I}V → - G ⊢ ⬊*[h, o, ⓑ{a,I}V.T, l] L. -/2 width=3 by lsx_bind_lpxs_aux/ qed. - -lemma lsx_flat_lpxs: ∀h,o,I,G,L1,V,l. G ⊢ ⬊*[h, o, V, l] L1 → - ∀L2,T. G ⊢ ⬊*[h, o, T, l] L2 → ⦃G, L1⦄ ⊢ ➡*[h, o] L2 → - G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L2. -#h #o #I #G #L1 #V #l #H @(lsx_ind_alt … H) -L1 -#L1 #HL1 #IHL1 #L2 #T #H @(lsx_ind_alt … H) -L2 -#L2 #HL2 #IHL2 #HL12 @lsx_intro_alt -#L0 #HL20 lapply (lpxs_trans … HL12 … HL20) -#HL10 #H elim (nlleq_inv_flat … H) -H [ -HL1 -IHL2 | -HL2 -IHL1 ] -[ #HnV elim (lleq_dec V L1 L2 l) - [ #HV @(IHL1 … L0) /3 width=3 by lsx_lpxs_trans, lleq_canc_sn/ (**) (* full auto too slow: 47s *) - | -HnV -HL10 /3 width=4 by lsx_lpxs_trans/ - ] -| /3 width=1 by/ -] -qed-. - -lemma lsx_flat: ∀h,o,I,G,L,V,l. G ⊢ ⬊*[h, o, V, l] L → - ∀T. G ⊢ ⬊*[h, o, T, l] L → G ⊢ ⬊*[h, o, ⓕ{I}V.T, l] L. -/2 width=3 by lsx_flat_lpxs/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index 610a54f77..832e88f69 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -1,5 +1,5 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_lsubr.ma cpxs_aaa.ma cpxs_lfpx.ma cpxs_cnx.ma cpxs_cpxs.ma -lfpxs.ma lfpxs_fqup.ma lfpxs_cpxs.ma +lfpxs.ma lfpxs_length.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_cpxs.ma lfpxs_lfpxs.ma csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_fqup.ma lfsx_lfsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma index 61fc781b2..cc8550d21 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma @@ -54,9 +54,11 @@ lemma lfpr_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1. (* Basic inversion lemmas ***************************************************) +(* Basic_2A1: uses: lpr_inv_atom1 *) lemma lfpr_inv_atom_sn: ∀h,I,G,Y2. ⦃G, ⋆⦄ ⊢ ➡[h, ⓪{I}] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. +(* Basic_2A1: uses: lpr_inv_atom2 *) lemma lfpr_inv_atom_dx: ∀h,I,G,Y1. ⦃G, Y1⦄ ⊢ ➡[h, ⓪{I}] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. @@ -131,33 +133,21 @@ lemma lfpr_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ➡[h, §l] L2 (* Basic forward lemmas *****************************************************) -lemma lfpr_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2. -/2 width=4 by lfxs_fwd_bind_sn/ qed-. +lemma lfpr_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. + ⦃G, L1⦄ ⊢ ➡[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2. +/2 width=3 by lfxs_fwd_pair_sn/ qed-. lemma lfpr_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓑ{p,I}V.T] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ➡[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_fwd_bind_dx/ qed-. -lemma lfpr_fwd_flat_sn: ∀h,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2. -/2 width=3 by lfxs_fwd_flat_sn/ qed-. - lemma lfpr_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ➡[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, T] L2. /2 width=3 by lfxs_fwd_flat_dx/ qed-. -lemma lfpr_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ➡[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ➡[h, V] L2. -/2 width=3 by lfxs_fwd_pair_sn/ qed-. - -(* Basic_2A1: removed theorems 16: - lpr_inv_atom1 lpr_inv_pair1 lpr_inv_atom2 lpr_inv_pair2 - lpr_refl lpr_pair - lpr_fwd_length lpr_lpx - lpr_drop_conf drop_lpr_trans lpr_drop_trans_O1 +(* Basic_2A1: removed theorems 5: + lpr_inv_pair1 lpr_inv_pair2 cpr_conf_lpr lpr_cpr_conf_dx lpr_cpr_conf_sn - fqu_lpr_trans fquq_lpr_trans *) (* Basic_1: removed theorems 7: wcpr0_gen_sort wcpr0_gen_head diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma index 7d23f3b0f..7c630638c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_drops.ma @@ -20,14 +20,17 @@ include "basic_2/rt_transition/lfpr.ma". (* Properties with generic slicing for local environments *******************) +(* Basic_2A1: uses: drop_lpr_trans *) lemma drops_lfpr_trans: ∀h,G. dedropable_sn (cpm 0 h G). /3 width=6 by lfxs_liftable_dedropable_sn, cpm_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) +(* Basic_2A1: uses: lpr_drop_conf *) lemma lfpr_drops_conf: ∀h,G. dropable_sn (cpm 0 h G). /2 width=5 by lfxs_dropable_sn/ qed-. +(* Basic_2A1: uses: lpr_drop_trans_O1 *) lemma lfpr_drops_trans: ∀h,G. dropable_dx (cpm 0 h G). /2 width=5 by lfxs_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma index d0be90869..a0f5b490d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fqup.ma @@ -20,9 +20,11 @@ include "basic_2/rt_transition/lfpr.ma". (* Advanced properties ******************************************************) (* Note: lemma 250 *) +(* Basic_2A1: uses: lpr_refl *) lemma lfpr_refl: ∀h,G,T. reflexive … (lfpr h G T). /2 width=1 by lfxs_refl/ qed. +(* Basic_2A1: uses: lpr_pair *) lemma lfpr_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ➡[h] V2 → ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ➡[h, T] L.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma index 66d9580db..72c313796 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma @@ -30,6 +30,7 @@ lemma fqu_cpr_trans_dx: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, /3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ qed-. +(* Basic_2A1: uses: fqu_lpr_trans *) lemma fqu_cpr_trans_sn: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. @@ -50,6 +51,7 @@ lemma fquq_cpr_trans_dx: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, ] qed-. +(* Basic_2A1: uses: fquq_lpr_trans *) lemma fquq_cpr_trans_sn: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡[h] U2 → ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡[h, T1] L & ⦃G1, L1⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_length.ma index 19db3f337..2f7b3231a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_length.ma @@ -19,5 +19,6 @@ include "basic_2/rt_transition/lfpr.ma". (* Forward lemmas with length for local environments ************************) +(* Basic_2A1: uses: lpr_fwd_length *) lemma lfpr_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma index 47323a86d..e2414b916 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_lfpx.ma @@ -20,5 +20,6 @@ include "basic_2/rt_transition/lfpr.ma". (* Fwd. lemmas with unc. rt-transition for local env.s on referred entries **) +(* Basic_2A1: uses: lpr_lpx *) lemma lfpr_fwd_lfpx: ∀h,T,G,L1,L2. ⦃G, L1⦄ ⊢ ➡[h, T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2. /3 width=3 by cpm_fwd_cpx, lfxs_co/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma index 0fc26a744..172f88ed5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx.ma @@ -54,9 +54,11 @@ lemma lfpx_pair_repl_dx: ∀h,I,G,L1,L2,T,V,V1. (* Basic inversion lemmas ***************************************************) +(* Basic_2A1: uses: lpx_inv_atom1 *) lemma lfpx_inv_atom_sn: ∀h,G,Y2,T. ⦃G, ⋆⦄ ⊢ ⬈[h, T] Y2 → Y2 = ⋆. /2 width=3 by lfxs_inv_atom_sn/ qed-. +(* Basic_2A1: uses: lpx_inv_atom2 *) lemma lfpx_inv_atom_dx: ∀h,G,Y1,T. ⦃G, Y1⦄ ⊢ ⬈[h, T] ⋆ → Y1 = ⋆. /2 width=3 by lfxs_inv_atom_dx/ qed-. @@ -131,29 +133,18 @@ lemma lfpx_inv_gref_pair_dx: ∀h,I,G,Y1,L2,V2,l. ⦃G, Y1⦄ ⊢ ⬈[h, §l] L2 (* Basic forward lemmas *****************************************************) -lemma lfpx_fwd_bind_sn: ∀h,p,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2. -/2 width=4 by lfxs_fwd_bind_sn/ qed-. +lemma lfpx_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. + ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2. +/2 width=3 by lfxs_fwd_pair_sn/ qed-. lemma lfpx_fwd_bind_dx: ∀h,p,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓑ{p,I}V.T] L2 → ⦃G, L1.ⓑ{I}V⦄ ⊢ ⬈[h, T] L2.ⓑ{I}V. /2 width=2 by lfxs_fwd_bind_dx/ qed-. -lemma lfpx_fwd_flat_sn: ∀h,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2. -/2 width=3 by lfxs_fwd_flat_sn/ qed-. - lemma lfpx_fwd_flat_dx: ∀h,I,G,L1,L2,V,T. ⦃G, L1⦄ ⊢ ⬈[h, ⓕ{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, T] L2. /2 width=3 by lfxs_fwd_flat_dx/ qed-. -lemma lfpx_fwd_pair_sn: ∀h,I,G,L1,L2,V,T. - ⦃G, L1⦄ ⊢ ⬈[h, ②{I}V.T] L2 → ⦃G, L1⦄ ⊢ ⬈[h, V] L2. -/2 width=3 by lfxs_fwd_pair_sn/ qed-. - -(* Basic_2A1: removed theorems 14: - lpx_refl lpx_pair lpx_fwd_length - lpx_inv_atom1 lpx_inv_pair1 lpx_inv_atom2 lpx_inv_pair2 lpx_inv_pair - lpx_drop_conf drop_lpx_trans lpx_drop_trans_O1 - lpx_cpx_frees_trans cpx_frees_trans lpx_frees_trans +(* Basic_2A1: removed theorems 3: + lpx_inv_pair1 lpx_inv_pair2 lpx_inv_pair *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma index 2f90bf27e..bc6e8a43a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_aaa.ma @@ -21,7 +21,7 @@ include "basic_2/rt_transition/lfpx_fqup.ma". (* Properties with atomic arity assignment for terms ************************) (* Note: lemma 500 *) -(* Basic_2A1: was: cpx_lpx_aaa_conf *) +(* Basic_2A1: uses: cpx_lpx_aaa_conf *) lemma cpx_aaa_conf_lfpx: ∀h,G,L1,T1,A. ⦃G, L1⦄ ⊢ T1 ⁝ A → ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → ∀L2. ⦃G, L1⦄ ⊢ ⬈[h, T1] L2 → ⦃G, L2⦄ ⊢ T2 ⁝ A. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma index d49e4e01d..53b7d2e1f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_drops.ma @@ -20,14 +20,17 @@ include "basic_2/rt_transition/lfpx.ma". (* Properties with generic slicing for local environments *******************) +(* Basic_2A1: uses: drop_lpx_trans *) lemma drops_lfpx_trans: ∀h,G. dedropable_sn (cpx h G). /3 width=6 by lfxs_liftable_dedropable_sn, cpx_lifts_sn/ qed-. (* Inversion lemmas with generic slicing for local environments *************) +(* Basic_2A1: uses: lpx_drop_conf *) lemma lfpx_drops_conf: ∀h,G. dropable_sn (cpx h G). /2 width=5 by lfxs_dropable_sn/ qed-. +(* Basic_2A1: uses: lpx_drop_trans_O1 *) lemma lfpx_drops_trans: ∀h,G. dropable_dx (cpx h G). /2 width=5 by lfxs_dropable_dx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma index f7d15c1d2..2967a62bb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_fqup.ma @@ -19,9 +19,11 @@ include "basic_2/rt_transition/lfpx.ma". (* Advanced properties ******************************************************) +(* Basic_2A1: uses: lpx_refl lpx_pair *) lemma lfpx_refl: ∀h,G,T. reflexive … (lfpx h G T). /2 width=1 by lfxs_refl/ qed. +(* Basic_2A1: uses: lpx_refl lpx_pair *) lemma lfpx_pair: ∀h,G,L,V1,V2. ⦃G, L⦄ ⊢ V1 ⬈[h] V2 → ∀I,T. ⦃G, L.ⓑ{I}V1⦄ ⊢ ⬈[h, T] L.ⓑ{I}V2. /2 width=1 by lfxs_pair/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma index 46fd8a229..1ec892cbf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_frees.ma @@ -22,7 +22,7 @@ include "basic_2/rt_transition/cpx_drops.ma". (* Properties with context-sensitive free variables *************************) -(* Basic_2A1: was: lpx_cpx_frees_trans *) +(* Basic_2A1: uses: lpx_cpx_frees_trans *) lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀L2. L1 ⦻*[cpx h G, cfull, f1] L2 → ∀T2. ⦃G, L1⦄ ⊢ T1 ⬈[h] T2 → @@ -147,10 +147,10 @@ lemma cpx_frees_conf_lfpx: ∀h,G,L1,T1,f1. L1 ⊢ 𝐅*⦃T1⦄ ≡ f1 → ] qed-. -(* Basic_2A1: was: cpx_frees_trans *) +(* Basic_2A1: uses: cpx_frees_trans *) lemma cpx_frees_conf: ∀h,G. R_frees_confluent (cpx h G). /3 width=7 by cpx_frees_conf_lfpx, lexs_refl/ qed-. -(* Basic_2A1: was: lpx_frees_trans *) +(* Basic_2A1: uses: lpx_frees_trans *) lemma lfpx_frees_conf: ∀h,G. lexs_frees_confluent (cpx h G) cfull. /2 width=7 by cpx_frees_conf_lfpx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma index 6e4acfac4..d0ca2b90c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_length.ma @@ -19,5 +19,6 @@ include "basic_2/rt_transition/lfpx.ma". (* Forward lemmas with length for local environments ************************) +(* Basic_2A1: uses: lpx_fwd_length *) lemma lfpx_fwd_length: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma index 020bd81c5..ea1e66bad 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lfdeq.ma @@ -125,7 +125,7 @@ lemma tdeq_cpx_trans: ∀h,o,G,L,T2,T0. T2 ≡[h, o] T0 → elim (cpx_tdeq_conf … HT01 T2) -HT01 /3 width=3 by tdeq_sym, ex2_intro/ qed-. -(* Basic_2A1: was just: cpx_lleq_conf *) +(* Basic_2A1: uses: cpx_lleq_conf *) lemma cpx_lfdeq_conf: ∀h,o,G,L0,T0,T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → ∀L2. L0 ≡[h, o, T0] L2 → ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T1 ≡[h, o] T. @@ -134,7 +134,7 @@ elim (cpx_tdeq_conf_lexs … HT01 T0 … L0 … HL02) -HT01 -HL02 /2 width=3 by lfxs_refl, ex2_intro/ qed-. -(* Basic_2A1: was just: lleq_cpx_trans *) +(* Basic_2A1: uses: lleq_cpx_trans *) lemma lfdeq_cpx_trans: ∀h,o,G,L2,L0,T0. L2 ≡[h, o, T0] L0 → ∀T1. ⦃G, L0⦄ ⊢ T0 ⬈[h] T1 → ∃∃T. ⦃G, L2⦄ ⊢ T0 ⬈[h] T & T ≡[h, o] T1. @@ -146,7 +146,7 @@ qed-. lemma lfpx_lfdeq_conf: ∀h,o,G,T. confluent2 … (lfpx h G T) (lfdeq h o T). /3 width=6 by lfpx_frees_conf, cpx_tdeq_conf_lexs, frees_lfdeq_conf_lexs, lfxs_conf/ qed-. -(* Basic_2A1: was just: lleq_lpx_trans *) +(* Basic_2A1: uses: lleq_lpx_trans *) lemma lfdeq_lfpx_trans: ∀h,o,G,T,L2,K2. ⦃G, L2⦄ ⊢ ⬈[h, T] K2 → ∀L1. L1 ≡[h, o, T] L2 → ∃∃K1. ⦃G, L1⦄ ⊢ ⬈[h, T] K1 & K1 ≡[h, o, T] K2. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma index f6bc891d7..6fb68863e 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq.ma @@ -73,6 +73,7 @@ lemma tdeq_lfdeq_conf_sn: ∀h,o. s_r_confluent1 … (cdeq h o) (lfdeq h o). /3 width=5 by frees_tdeq_conf, ex2_intro/ qed-. +(* Basic_2A1: uses: lleq_sym *) lemma lfdeq_sym: ∀h,o,T. symmetric … (lfdeq h o T). #h #o #T #L1 #L2 * /4 width=7 by frees_tdeq_conf_lexs, lfxs_sym, tdeq_sym, ex2_intro/ @@ -81,6 +82,7 @@ qed-. lemma lfdeq_atom: ∀h,o,I. ⋆ ≡[h, o, ⓪{I}] ⋆. /2 width=1 by lfxs_atom/ qed. +(* Basic_2A1: uses: lleq_sort *) lemma lfdeq_sort: ∀h,o,I,L1,L2,V1,V2,s. L1 ≡[h, o, ⋆s] L2 → L1.ⓑ{I}V1 ≡[h, o, ⋆s] L2.ⓑ{I}V2. /2 width=1 by lfxs_sort/ qed. @@ -93,6 +95,7 @@ lemma lfdeq_lref: ∀h,o,I,L1,L2,V1,V2,i. L1 ≡[h, o, #i] L2 → L1.ⓑ{I}V1 ≡[h, o, #⫯i] L2.ⓑ{I}V2. /2 width=1 by lfxs_lref/ qed. +(* Basic_2A1: uses: lleq_gref *) lemma lfdeq_gref: ∀h,o,I,L1,L2,V1,V2,l. L1 ≡[h, o, §l] L2 → L1.ⓑ{I}V1 ≡[h, o, §l] L2.ⓑ{I}V2. /2 width=1 by lfxs_gref/ qed. @@ -125,10 +128,12 @@ lemma lfdeq_inv_lref: ∀h,o,Y1,Y2,i. Y1 ≡[h, o, #⫯i] Y2 → Y1 = L1.ⓑ{I}V1 & Y2 = L2.ⓑ{I}V2. /2 width=1 by lfxs_inv_lref/ qed-. +(* Basic_2A1: uses: lleq_inv_bind lleq_inv_bind_O *) lemma lfdeq_inv_bind: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1 ≡[h, o, V] L2 ∧ L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. +(* Basic_2A1: uses: lleq_inv_flat *) lemma lfdeq_inv_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, V] L2 ∧ L1 ≡[h, o, T] L2. /2 width=2 by lfxs_inv_flat/ qed-. @@ -156,32 +161,27 @@ lemma lfdeq_inv_lref_pair_dx: ∀h,o,I,Y1,L2,V2,i. Y1 ≡[h, o, #⫯i] L2.ⓑ{I} (* Basic forward lemmas *****************************************************) -lemma lfdeq_fwd_bind_sn: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1 ≡[h, o, V] L2. -/2 width=4 by lfxs_fwd_bind_sn/ qed-. +(* Basic_2A1: uses: lleq_fwd_bind_sn lleq_fwd_flat_sn *) +lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. +/2 width=3 by lfxs_fwd_pair_sn/ qed-. +(* Basic_2A1: uses: lleq_fwd_bind_dx lleq_fwd_bind_O_dx *) lemma lfdeq_fwd_bind_dx: ∀h,o,p,I,L1,L2,V,T. L1 ≡[h, o, ⓑ{p,I}V.T] L2 → L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V. /2 width=2 by lfxs_fwd_bind_dx/ qed-. -lemma lfdeq_fwd_flat_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, V] L2. -/2 width=3 by lfxs_fwd_flat_sn/ qed-. - +(* Basic_2A1: uses: lleq_fwd_flat_dx *) lemma lfdeq_fwd_flat_dx: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ⓕ{I}V.T] L2 → L1 ≡[h, o, T] L2. /2 width=3 by lfxs_fwd_flat_dx/ qed-. -lemma lfdeq_fwd_pair_sn: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, ②{I}V.T] L2 → L1 ≡[h, o, V] L2. -/2 width=3 by lfxs_fwd_pair_sn/ qed-. - lemma lfdeq_fwd_dx: ∀h,o,I,L1,K2,V2. ∀T:term. L1 ≡[h, o, T] K2.ⓑ{I}V2 → ∃∃K1,V1. L1 = K1.ⓑ{I}V1. /2 width=5 by lfxs_fwd_dx/ qed-. -(* Basic_2A1: removed theorems 31: - lleq_ind lleq_inv_bind lleq_inv_flat lleq_fwd_length lleq_fwd_lref +(* Basic_2A1: removed theorems 10: + lleq_ind lleq_fwd_lref lleq_fwd_drop_sn lleq_fwd_drop_dx - lleq_fwd_bind_sn lleq_fwd_bind_dx lleq_fwd_flat_sn lleq_fwd_flat_dx - lleq_sort lleq_skip lleq_lref lleq_free lleq_gref lleq_bind lleq_flat - lleq_refl lleq_Y lleq_sym lleq_ge_up lleq_ge lleq_bind_O llpx_sn_lrefl - lleq_trans lleq_canc_sn lleq_canc_dx lleq_nlleq_trans nlleq_lleq_div - lleq_dec + lleq_skip lleq_lref lleq_free + lleq_Y lleq_ge_up lleq_ge + *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma index 529236417..b20b5a0bf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_fqup.ma @@ -19,6 +19,7 @@ include "basic_2/static/lfdeq.ma". (* Advanced properties ******************************************************) +(* Basic_2A1: uses: lleq_refl *) lemma lfdeq_refl: ∀h,o,T. reflexive … (lfdeq h o T). /2 width=1 by lfxs_refl/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma index d7c04b6ec..aafc79221 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_length.ma @@ -19,5 +19,6 @@ include "basic_2/static/lfdeq.ma". (* Forward lemmas with length for local environments ************************) +(* Basic_2A1: lleq_fwd_length *) lemma lfdeq_fwd_length: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → |L1| = |L2|. /2 width=3 by lfxs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma index 9f92ecd27..f3fbeda42 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfdeq.ma @@ -20,20 +20,24 @@ include "basic_2/static/lfdeq.ma". (* Advanced properties ******************************************************) +(* Basic_2A1: uses: lleq_dec *) lemma lfdeq_dec: ∀h,o,L1,L2. ∀T:term. Decidable (L1 ≡[h, o, T] L2). /3 width=1 by lfxs_dec, tdeq_dec/ qed-. (* Main properties **********************************************************) +(* Basic_2A1: uses: lleq_bind lleq_bind_O *) theorem lfdeq_bind: ∀h,o,p,I,L1,L2,V1,V2,T. L1 ≡[h, o, V1] L2 → L1.ⓑ{I}V1 ≡[h, o, T] L2.ⓑ{I}V2 → L1 ≡[h, o, ⓑ{p,I}V1.T] L2. /2 width=2 by lfxs_bind/ qed. +(* Basic_2A1: uses: lleq_flat *) theorem lfdeq_flat: ∀h,o,I,L1,L2,V,T. L1 ≡[h, o, V] L2 → L1 ≡[h, o, T] L2 → L1 ≡[h, o, ⓕ{I}V.T] L2. /2 width=1 by lfxs_flat/ qed. +(* Basic_2A1: uses: lleq_trans *) theorem lfdeq_trans: ∀h,o,T. Transitive … (lfdeq h o T). #h #o #T #L1 #L * #f1 #Hf1 #HL1 #L2 * #f2 #Hf2 #HL2 lapply (frees_tdeq_conf_lexs … Hf1 T … HL1) // #H0 @@ -41,9 +45,11 @@ lapply (frees_mono … Hf2 … H0) -Hf2 -H0 /4 width=7 by lexs_trans, lexs_eq_repl_back, tdeq_trans, ex2_intro/ qed-. +(* Basic_2A1: uses: lleq_canc_sn *) theorem lfdeq_canc_sn: ∀h,o,T. left_cancellable … (lfdeq h o T). /3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. +(* Basic_2A1: uses: lleq_canc_dx *) theorem lfdeq_canc_dx: ∀h,o,T. right_cancellable … (lfdeq h o T). /3 width=3 by lfdeq_trans, lfdeq_sym/ qed-. @@ -51,13 +57,31 @@ theorem lfdeq_repl: ∀h,o,L1,L2. ∀T:term. L1 ≡[h, o, T] L2 → ∀K1. L1 ≡[h, o, T] K1 → ∀K2. L2 ≡[h, o, T] K2 → K1 ≡[h, o, T] K2. /3 width=3 by lfdeq_canc_sn, lfdeq_trans/ qed-. -(* Advanced properies on negated lazy equivalence *****************************) +(* Negated properties *******************************************************) -(* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred ************) -lemma lfdeq_nlfdeq_trans: ∀h,o.∀T:term.∀L1,L. L1 ≡[h, o, T] L → +(* Note: auto works with /4 width=8/ so lfdeq_canc_sn is preferred **********) +(* Basic_2A1: uses: lleq_nlleq_trans *) +lemma lfdeq_lfdneq_trans: ∀h,o.∀T:term.∀L1,L. L1 ≡[h, o, T] L → ∀L2. (L ≡[h, o, T] L2 → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). /3 width=3 by lfdeq_canc_sn/ qed-. -lemma nlfdeq_lfdeq_div: ∀h,o.∀T:term.∀L2,L. L2 ≡[h, o, T] L → +(* Basic_2A1: uses: nlleq_lleq_div *) +lemma lfdneq_lfdeq_div: ∀h,o.∀T:term.∀L2,L. L2 ≡[h, o, T] L → ∀L1. (L1 ≡[h, o, T] L → ⊥) → (L1 ≡[h, o, T] L2 → ⊥). /3 width=3 by lfdeq_trans/ qed-. + +theorem lfdneq_lfdeq_canc_dx: ∀h,o,L1,L. ∀T:term. (L1 ≡[h, o, T] L → ⊥) → + ∀L2. L2 ≡[h, o, T] L → L1 ≡[h, o, T] L2 → ⊥. +/3 width=3 by lfdeq_trans/ qed-. + +(* Negated inversion lemmas *************************************************) + +(* Basic_2A1: uses: nlleq_inv_bind nlleq_inv_bind_O *) +lemma lfdneq_inv_bind: ∀h,o,p,I,L1,L2,V,T. (L1 ≡[h, o, ⓑ{p,I}V.T] L2 → ⊥) → + (L1 ≡[h, o, V] L2 → ⊥) ∨ (L1.ⓑ{I}V ≡[h, o, T] L2.ⓑ{I}V → ⊥). +/3 width=2 by lfnxs_inv_bind, tdeq_dec/ qed-. + +(* Basic_2A1: uses: nlleq_inv_flat *) +lemma lfdneq_inv_flat: ∀h,o,I,L1,L2,V,T. (L1 ≡[h, o, ⓕ{I}V.T] L2 → ⊥) → + (L1 ≡[h, o, V] L2 → ⊥) ∨ (L1 ≡[h, o, T] L2 → ⊥). +/3 width=2 by lfnxs_inv_flat, tdeq_dec/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma index d7dae247e..367b19d32 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs.ma @@ -49,6 +49,7 @@ lemma lfxs_atom: ∀R,I. ⋆ ⦻*[R, ⓪{I}] ⋆. /3 width=3 by lexs_atom, frees_atom, ex2_intro/ qed. +(* Basic_2A1: uses: llpx_sn_sort *) lemma lfxs_sort: ∀R,I,L1,L2,V1,V2,s. L1 ⦻*[R, ⋆s] L2 → L1.ⓑ{I}V1 ⦻*[R, ⋆s] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #s * /3 width=3 by lexs_push, frees_sort, ex2_intro/ @@ -64,6 +65,7 @@ lemma lfxs_lref: ∀R,I,L1,L2,V1,V2,i. #R #I #L1 #L2 #V1 #V2 #i * /3 width=3 by lexs_push, frees_lref, ex2_intro/ qed. +(* Basic_2A1: uses: llpx_sn_gref *) lemma lfxs_gref: ∀R,I,L1,L2,V1,V2,l. L1 ⦻*[R, §l] L2 → L1.ⓑ{I}V1 ⦻*[R, §l] L2.ⓑ{I}V2. #R #I #L1 #L2 #V1 #V2 #l * /3 width=3 by lexs_push, frees_gref, ex2_intro/ @@ -84,6 +86,7 @@ lemma lfxs_sym: ∀R. lexs_frees_confluent R cfull → /4 width=5 by sle_lexs_trans, lexs_sym, ex2_intro/ qed-. +(* Basic_2A1: uses: llpx_sn_co *) lemma lfxs_co: ∀R1,R2. (∀L,T1,T2. R1 L T1 T2 → R2 L T1 T2) → ∀L1,L2,T. L1 ⦻*[R1, T] L2 → L1 ⦻*[R2, T] L2. #R1 #R2 #HR #L1 #L2 #T * /4 width=7 by lexs_co, ex2_intro/ @@ -155,12 +158,14 @@ lemma lfxs_inv_gref: ∀R,Y1,Y2,l. Y1 ⦻*[R, §l] Y2 → ] qed-. +(* Basic_2A1: uses: llpx_sn_inv_bind llpx_sn_inv_bind_O *) lemma lfxs_inv_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → L1 ⦻*[R, V1] L2 ∧ L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. #R #p #I #L1 #L2 #V1 #V2 #T * #f #Hf #HL #HV elim (frees_inv_bind … Hf) -Hf /6 width=6 by sle_lexs_trans, lexs_inv_tl, sor_inv_sle_dx, sor_inv_sle_sn, ex2_intro, conj/ qed-. +(* Basic_2A1: uses: llpx_sn_inv_flat *) lemma lfxs_inv_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2 ∧ L1 ⦻*[R, T] L2. #R #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_flat … Hf) -Hf @@ -239,28 +244,24 @@ qed-. (* Basic forward lemmas *****************************************************) -lemma lfxs_fwd_bind_sn: ∀R,p,I,L1,L2,V,T. L1 ⦻*[R, ⓑ{p,I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #p #I #L1 #L2 #V #T * #f #Hf #HL elim (frees_inv_bind … Hf) -Hf +(* Basic_2A1: uses: llpx_sn_fwd_pair_sn llpx_sn_fwd_bind_sn llpx_sn_fwd_flat_sn *) +lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. +#R * [ #p ] #I #L1 #L2 #V #T * #f #Hf #HL +[ elim (frees_inv_bind … Hf) | elim (frees_inv_flat … Hf) ] -Hf /4 width=6 by sle_lexs_trans, sor_inv_sle_sn, ex2_intro/ qed-. +(* Basic_2A1: uses: llpx_sn_fwd_bind_dx llpx_sn_fwd_bind_O_dx *) lemma lfxs_fwd_bind_dx: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, ⓑ{p,I}V1.T] L2 → R L1 V1 V2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2. #R #p #I #L1 #L2 #V1 #V2 #T #H #HV elim (lfxs_inv_bind … H HV) -H -HV // qed-. -lemma lfxs_fwd_flat_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // -qed-. - +(* Basic_2A1: uses: llpx_sn_fwd_flat_dx *) lemma lfxs_fwd_flat_dx: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ⓕ{I}V.T] L2 → L1 ⦻*[R, T] L2. #R #I #L1 #L2 #V #T #H elim (lfxs_inv_flat … H) -H // qed-. -lemma lfxs_fwd_pair_sn: ∀R,I,L1,L2,V,T. L1 ⦻*[R, ②{I}V.T] L2 → L1 ⦻*[R, V] L2. -#R * /2 width=4 by lfxs_fwd_flat_sn, lfxs_fwd_bind_sn/ -qed-. - lemma lfxs_fwd_dx: ∀R,I,L1,K2,T,V2. L1 ⦻*[R, T] K2.ⓑ{I}V2 → ∃∃K1,V1. L1 = K1.ⓑ{I}V1. #R #I #L1 #K2 #T #V2 * #f elim (pn_split f) * #g #Hg #_ #Hf destruct @@ -268,13 +269,9 @@ lemma lfxs_fwd_dx: ∀R,I,L1,K2,T,V2. L1 ⦻*[R, T] K2.ⓑ{I}V2 → /2 width=3 by ex1_2_intro/ qed-. -(* Basic_2A1: removed theorems 25: - llpx_sn_sort llpx_sn_skip llpx_sn_lref llpx_sn_free llpx_sn_gref - llpx_sn_bind llpx_sn_flat - llpx_sn_inv_bind llpx_sn_inv_flat - llpx_sn_fwd_lref llpx_sn_fwd_pair_sn llpx_sn_fwd_length - llpx_sn_fwd_bind_sn llpx_sn_fwd_bind_dx llpx_sn_fwd_flat_sn llpx_sn_fwd_flat_dx - llpx_sn_refl llpx_sn_Y llpx_sn_bind_O llpx_sn_ge_up llpx_sn_ge llpx_sn_co - llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx - llpx_sn_dec +(* Basic_2A1: removed theorems 9: + llpx_sn_skip llpx_sn_lref llpx_sn_free + llpx_sn_fwd_lref + llpx_sn_Y llpx_sn_ge_up llpx_sn_ge + llpx_sn_fwd_drop_sn llpx_sn_fwd_drop_dx *) diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma index 50fb764fa..e0fc99355 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_fqup.ma @@ -19,6 +19,7 @@ include "basic_2/static/lfxs.ma". (* Advanced properties ******************************************************) +(* Basic_2A1: uses: llpx_sn_refl *) lemma lfxs_refl: ∀R. (∀L. reflexive … (R L)) → ∀L,T. L ⦻*[R, T] L. #R #HR #L #T elim (frees_total L T) /3 width=3 by lexs_refl, ex2_intro/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma index 01dd82cf4..386e2ba88 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_length.ma @@ -19,6 +19,7 @@ include "basic_2/static/lfxs.ma". (* Forward lemmas with length for local environments ************************) +(* Basic_2A1: uses: llpx_sn_fwd_length *) lemma lfxs_fwd_length: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → |L1| = |L2|. #R #L1 #L2 #T * /2 width=4 by lexs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma index 54fdb9e43..78b1c526b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lfxs.ma @@ -26,6 +26,7 @@ lemma lfxs_inv_frees: ∀R,L1,L2,T. L1 ⦻*[R, T] L2 → #R #L1 #L2 #T * /3 width=6 by frees_mono, lexs_eq_repl_back/ qed-. +(* Basic_2A1: uses: llpx_sn_dec *) lemma lfxs_dec: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → ∀L1,L2,T. Decidable (L1 ⦻*[R, T] L2). #R #HR #L1 #L2 #T @@ -71,6 +72,7 @@ qed-. (* Main properties **********************************************************) +(* Basic_2A1: uses: llpx_sn_bind llpx_sn_bind_O *) theorem lfxs_bind: ∀R,p,I,L1,L2,V1,V2,T. L1 ⦻*[R, V1] L2 → L1.ⓑ{I}V1 ⦻*[R, T] L2.ⓑ{I}V2 → L1 ⦻*[R, ⓑ{p,I}V1.T] L2. @@ -79,6 +81,7 @@ elim (lexs_fwd_pair … Hf2) -Hf2 #Hf2 #_ elim (sor_isfin_ex f1 (⫱f2)) /3 width=7 by frees_fwd_isfin, frees_bind, lexs_join, isfin_tl, ex2_intro/ qed. +(* Basic_2A1: llpx_sn_flat *) theorem lfxs_flat: ∀R,I,L1,L2,V,T. L1 ⦻*[R, V] L2 → L1 ⦻*[R, T] L2 → L1 ⦻*[R, ⓕ{I}V.T] L2. @@ -108,3 +111,21 @@ elim (lexs_conf … HL01 … HL02) /2 width=3 by ex2_intro/ [ | -HL01 -HL02 ] elim (HR12 … HV01 … HV02 K1 … K2) /2 width=3 by ex2_intro/ ] qed-. + +(* Negated inversion lemmas *************************************************) + +(* Basic_2A1: uses: nllpx_sn_inv_bind nllpx_sn_inv_bind_O *) +lemma lfnxs_inv_bind: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → + ∀p,I,L1,L2,V,T. (L1 ⦻*[R, ⓑ{p,I}V.T] L2 → ⊥) → + (L1 ⦻*[R, V] L2 → ⊥) ∨ (L1.ⓑ{I}V ⦻*[R, T] L2.ⓑ{I}V → ⊥). +#R #HR #p #I #L1 #L2 #V #T #H elim (lfxs_dec … HR L1 L2 V) +/4 width=2 by lfxs_bind, or_intror, or_introl/ +qed-. + +(* Basic_2A1: uses: nllpx_sn_inv_flat *) +lemma lfnxs_inv_flat: ∀R. (∀L,T1,T2. Decidable (R L T1 T2)) → + ∀I,L1,L2,V,T. (L1 ⦻*[R, ⓕ{I}V.T] L2 → ⊥) → + (L1 ⦻*[R, V] L2 → ⊥) ∨ (L1 ⦻*[R, T] L2 → ⊥). +#R #HR #I #L1 #L2 #V #T #H elim (lfxs_dec … HR L1 L2 V) +/4 width=1 by lfxs_flat, or_intror, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma index bdb48def6..51d09c534 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq_tdeq.ma @@ -45,6 +45,6 @@ theorem tdeq_tdneq_trans: ∀h,o,T1,T. T1 ≡[h, o] T → ∀T2. (T ≡[h, o] T2 T1 ≡[h, o] T2 → ⊥. /3 width=3 by tdeq_canc_sn/ qed-. -theorem tndeq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≡[h, o] T → ⊥) → ∀T2. T2 ≡[h, o] T → +theorem tdneq_tdeq_canc_dx: ∀h,o,T1,T. (T1 ≡[h, o] T → ⊥) → ∀T2. T2 ≡[h, o] T → T1 ≡[h, o] T2 → ⊥. /3 width=3 by tdeq_trans/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml index 9332d62da..f55e45f41 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2.ldw.xml @@ -84,7 +84,7 @@ (anniversary milestone). - Parametrized slicing of local environments + Parametrized slicing on local environments comprises both versions of this operation (one from basic_1, the other used in basic_2 till now). diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl index 0ac1d94d2..bf098d4a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl @@ -113,10 +113,10 @@ table { [ "lpxs ( ⦃?,?⦄ ⊢ ➡*[?,?] ? )" "lpxs_drop" + "lpxs_lleq" + "lpxs_aaa" + "lpxs_cpxs" + "lpxs_lpxs" * ] [ "cpxs_lreq" + "cpxs_lleq" + "cpxs_aaa" * ] *) - [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfsx" * ] + [ "lfsx ( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_fqup" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ "csx_vector ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] - [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_cpxs" * ] + [ "lfpxs ( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_cpxs" + "lfpxs_lfpxs" * ] [ "cpxs ( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" "cpxs_tdeq" + "cpxs_theq" + "cpxs_theq_vector" + "cpxs_drops" + "cpxs_lsubr" + "cpxs_aaa" + "cpxs_lfpx" + "cpxs_cnx" + "cpxs_cpxs" * ] } ] @@ -150,7 +150,7 @@ table { class "water" [ { "iterated static typing" * } { [ { "iterated extension on referred entries" * } { - [ "tc_lfxs ( ? ⦻**[?,?] ? )" * ] + [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" * ] } ] } -- 2.39.2