From b8e20d61b2e76f7a36f05b8803e60cc3388c0882 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 16 Mar 2017 19:59:05 +0000 Subject: [PATCH] component rt_transition completed! --- .../fpb_fleq.ma => etc/fpb/fpb_fleq.etc} | 0 .../basic_2/etc/lfpr/lfpr_fquq.etc | 33 ++++++++++ .../lambdadelta/basic_2/rt_transition/lfpr.ma | 3 +- .../basic_2/rt_transition/lfpr_fquq.ma | 60 ++++++++++++++++++ .../basic_2/rt_transition/lpr_fquq.ma | 62 ------------------- .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/web/basic_2.ldw.xml | 8 ++- .../lambdadelta/basic_2/web/basic_2_src.tbl | 4 +- .../matita/contribs/lambdadelta/partial.txt | 1 + .../contribs/lambdadelta/partial_compile.sh | 4 +- 10 files changed, 106 insertions(+), 71 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/{rt_transition/fpb_fleq.ma => etc/fpb/fpb_fleq.etc} (100%) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/lfpr/lfpr_fquq.etc create mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma delete mode 100644 matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fquq.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fleq.ma b/matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_fleq.etc similarity index 100% rename from matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_fleq.ma rename to matita/matita/contribs/lambdadelta/basic_2/etc/fpb/fpb_fleq.etc diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr/lfpr_fquq.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr/lfpr_fquq.etc new file mode 100644 index 000000000..f7a794c81 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/lfpr/lfpr_fquq.etc @@ -0,0 +1,33 @@ +(* These do not hold: lfpr_fqu_trans and lfpr_fquq_trans should *) + +lemma fqu_lfpr_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡[h, T2] K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡[h, T1] K1 & ⦃G1, L1⦄ ⊢ T1 ➡[h] T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄. +#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by lfpr_zero, fqu_lref_O, ex3_2_intro/ +[ #I #G2 #L2 #V2 #T2 #K2 #HLK2 + + + + +lfpr_zero, fqu_lref_O, ex3_2_intro/ + +fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lfpr_pair, ex3_2_intro/ +[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lfpr_inv_pair1 … H) -H + #K2 #W2 #HLK2 #HVW2 #H destruct + /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/ +| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12 + elim (drop_lfpr_trans … HLK1 … HK12) -HK12 + /3 width=7 by fqu_drop, ex3_2_intro/ +] +qed-. + +(* Basic_2A1: was: fquq_lpr_trans *) +lemma fquq_lfpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 → + ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄. +#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H +[ #HT12 elim (fqu_lfpr_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. 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 381233f04..61fc781b2 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr.ma @@ -151,12 +151,13 @@ 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 14: +(* 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 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_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma new file mode 100644 index 000000000..4fdd21f9e --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpr_fquq.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/s_transition/fquq.ma". +include "basic_2/rt_transition/cpm_drops.ma". +include "basic_2/rt_transition/cpr.ma". +include "basic_2/rt_transition/lfpr_fqup.ma". + +(* PARALLEL R-TRANSITION FOR LOCAL ENV.S ON REFERRED ENTRIES ****************) + +(* Properties with supclosure ***********************************************) + +lemma fqu_cpr_trans_dx: ∀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, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. +#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ +#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U +/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +qed-. + +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⦄. +#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +/3 width=5 by lfpr_pair, cpr_pair_sn, cpr_flat, cpm_bind, fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, ex3_2_intro/ +#I #G #L #V #U #T #HUT #U2 #HU2 elim (cpm_lifts … HU2 (Ⓣ) … HUT) -U +/3 width=9 by fqu_drop, drops_refl, drops_drop, ex3_2_intro/ +qed-. + +(* Properties with optional supclosure **************************************) + +lemma fquq_cpr_trans_dx: ∀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, L⦄ ⊢ T1 ➡[h] U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H +[ #HT12 #U2 #HTU2 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. + +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⦄. +#h #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H +[ #HT12 #U2 #HTU2 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ +| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fquq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fquq.ma deleted file mode 100644 index 4c0a26e56..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lpr_fquq.ma +++ /dev/null @@ -1,62 +0,0 @@ -(* Properties on context-sensitive parallel reduction for terms *************) - -lemma fqu_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ -#G #L #K #U #T #k #HLK #HUT #U2 #HU2 -elim (lift_total U2 0 (k+1)) #T2 #HUT2 -lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ -qed-. - -lemma fquq_cpr_trans_dx: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpr_trans_dx … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma fqu_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_bind_dx, fqu_flat_dx, lpr_pair, cpr_pair_sn, cpr_atom, cpr_bind, cpr_flat, ex3_2_intro/ -#G #L #K #U #T #k #HLK #HUT #U2 #HU2 -elim (lift_total U2 0 (k+1)) #T2 #HUT2 -lapply (cpr_lift … HU2 … HLK … HUT … HUT2) -HU2 -HUT /3 width=9 by fqu_drop, ex3_2_intro/ -qed-. - -lemma fquq_cpr_trans_sn: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ➡ U2 → - ∃∃L,U1. ⦃G1, L1⦄ ⊢ ➡ L & ⦃G1, L1⦄ ⊢ T1 ➡ U1 & ⦃G1, L, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #U2 #HTU2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_cpr_trans_sn … HT12 … HTU2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. - -lemma fqu_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/3 width=5 by fqu_lref_O, fqu_pair_sn, fqu_flat_dx, lpr_pair, ex3_2_intro/ -[ #a #I #G2 #L2 #V2 #T2 #X #H elim (lpr_inv_pair1 … H) -H - #K2 #W2 #HLK2 #HVW2 #H destruct - /3 width=5 by fqu_fquq, cpr_pair_sn, fqu_bind_dx, ex3_2_intro/ -| #G #L1 #K1 #T1 #U1 #k #HLK1 #HTU1 #K2 #HK12 - elim (drop_lpr_trans … HLK1 … HK12) -HK12 - /3 width=7 by fqu_drop, ex3_2_intro/ -] -qed-. - -lemma fquq_lpr_trans: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀K2. ⦃G2, L2⦄ ⊢ ➡ K2 → - ∃∃K1,T. ⦃G1, L1⦄ ⊢ ➡ K1 & ⦃G1, L1⦄ ⊢ T1 ➡ T & ⦃G1, K1, T⦄ ⊐⸮ ⦃G2, K2, T2⦄. -#G1 #G2 #L1 #L2 #T1 #T2 #H #K2 #HLK2 elim (fquq_inv_gen … H) -H -[ #HT12 elim (fqu_lpr_trans … HT12 … HLK2) /3 width=5 by fqu_fquq, ex3_2_intro/ -| * #H1 #H2 #H3 destruct /2 width=5 by ex3_2_intro/ -] -qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 6105414f3..18ddd3c3d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -4,6 +4,6 @@ lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_lfdeq.ma lf cnx.ma cnx_simple.ma cnx_drops.ma cnx_cnx.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_lfxs.ma cpm_cpx.ma cpr.ma cpr_drops.ma -lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma +lfpr.ma lfpr_length.ma lfpr_drops.ma lfpr_fquq.ma lfpr_fqup.ma lfpr_frees.ma lfpr_aaa.ma lfpr_lfpx.ma lfpr_lfpr.ma fpb.ma fpb_lfdeq.ma fpbq.ma fpbq_aaa.ma 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 b8c48ab9b..9332d62da 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 @@ -34,6 +34,10 @@ Stage "A2": "Extending the Applicability Condition" + + First behavioral component reconstructed: + rt_transition. + Generic candidates of reducibility. @@ -44,8 +48,8 @@ Confluence for context-sensitive parallel r-transition on terms. - Grammatical component reconstructed: - grammar, relocation, s_transition, s_computation, static + Syntactic component reconstructed: + syntax, relocation, s_transition, s_computation, static (anniversary milestone). 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 9471aeaff..7df4abf0a 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 @@ -125,11 +125,11 @@ table { [ { "rt-transition" * } { [ { "parallel rst-transition" * } { [ "fpbq ( ⦃?,?,?⦄ ≽[?] ⦃?,?,?⦄ )" "fpbq_aaa" * ] - [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" (* + "fpb_fleq" *) * ] + [ "fpb ( ⦃?,?,?⦄ ≻[?,?] ⦃?,?,?⦄ )" "fpb_lfdeq" * ] } ] [ { "t-bound context-sensitive rt-transition" * } { - [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] + [ "lfpr ( ⦃?,?⦄ ⊢ ➡[?,?] ? )" "lfpr_length" + "lfpr_drops" + "lfpr_fquq" + "lfpr_fqup" + "lfpr_frees" + "lfpr_aaa" + "lfpr_lfpx" + "lfpr_lfpr" * ] [ "cpr ( ⦃?,?⦄ ⊢ ? ➡[?] ? )" "cpr_drops" * ] [ "cpm ( ⦃?,?⦄ ⊢ ? ➡[?,?] ? )" "cpm_simple" + "cpm_drops" + "cpm_lsubr" + "cpm_lfxs" + "cpm_cpx" * ] } diff --git a/matita/matita/contribs/lambdadelta/partial.txt b/matita/matita/contribs/lambdadelta/partial.txt index 48819214f..4f87c5f77 100644 --- a/matita/matita/contribs/lambdadelta/partial.txt +++ b/matita/matita/contribs/lambdadelta/partial.txt @@ -5,4 +5,5 @@ basic_2/s_transition basic_2/s_computation basic_2/static basic_2/i_static +basic_2/rt_transition apps_2/examples/ex_cpr_omega.ma diff --git a/matita/matita/contribs/lambdadelta/partial_compile.sh b/matita/matita/contribs/lambdadelta/partial_compile.sh index 61fb60662..a6e1f77ce 100644 --- a/matita/matita/contribs/lambdadelta/partial_compile.sh +++ b/matita/matita/contribs/lambdadelta/partial_compile.sh @@ -1,6 +1,4 @@ ../../matitac.opt `cat partial.txt` -cd basic_2/rt_transition/ -../../../../matitac.opt `cat partial.txt` -cd ../rt_computation/ +cd basic_2/rt_computation/ ../../../../matitac.opt `cat partial.txt` cd ../../ -- 2.39.2