From: Ferruccio Guidi Date: Sun, 16 Apr 2017 13:42:16 +0000 (+0000) Subject: - strong normalization for rt-comutation X-Git-Tag: make_still_working~458 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=fed8c1a61273b0eb4a719fda70e2b5dd31933c8a - strong normalization for rt-comutation - advances on lfpxs ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc deleted file mode 100644 index fb7dad498..000000000 --- a/matita/matita/contribs/lambdadelta/basic_2/etc/csx_aaa.etc +++ /dev/null @@ -1,60 +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/static/gcp_aaa.ma". -include "basic_2/rt_computation/cpxs_aaa.ma". -include "basic_2/rt_computation/csx_gcp.ma". -include "basic_2/rt_computation/csx_gcr.ma". - -(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) - -(* Main properties with atomic arity assignment *****************************) - -theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. -#h #o #G #L #T #A #H -@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H) -qed. - -(* Advanced eliminators *****************************************************) - -fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ -qed-. - -lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. -/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. - -fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. -#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ -qed-. - -(* Basic_2A1: was: aaa_ind_csx_alt *) -lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term. - (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → - (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 - ) → - ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. -/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma new file mode 100644 index 000000000..4fe37f452 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_tc_lfxs.ma @@ -0,0 +1,23 @@ +(**************************************************************************) +(* ___ *) +(* ||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.ma". + +(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***) + +(* Main properties **********************************************************) + +theorem tc_lfxs_trans: ∀R,T. Transitive … (tc_lfxs R T). +#R #T #L1 #L #HL1 #L2 #HL2 @(trans_TC … HL1 HL2) (**) (* auto fails *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.ma new file mode 100644 index 000000000..fb7dad498 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_aaa.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/static/gcp_aaa.ma". +include "basic_2/rt_computation/cpxs_aaa.ma". +include "basic_2/rt_computation/csx_gcp.ma". +include "basic_2/rt_computation/csx_gcr.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) + +(* Main properties with atomic arity assignment *****************************) + +theorem aaa_csx: ∀h,o,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄. +#h #o #G #L #T #A #H +@(gcr_aaa … (csx_gcp h o) (csx_gcr h o) … H) +qed. + +(* Advanced eliminators *****************************************************) + +fact aaa_ind_csx_aux: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. +#h #o #G #L #A #R #IH #T #H @(csx_ind … H) -T /4 width=5 by cpx_aaa_conf/ +qed-. + +lemma aaa_ind_csx: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. +/5 width=9 by aaa_ind_csx_aux, aaa_csx/ qed-. + +fact aaa_ind_csx_cpxs_aux: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ ⬈*[h, o] 𝐒⦃T⦄ → ⦃G, L⦄ ⊢ T ⁝ A → R T. +#h #o #G #L #A #R #IH #T #H @(csx_ind_cpxs … H) -T /4 width=5 by cpxs_aaa_conf/ +qed-. + +(* Basic_2A1: was: aaa_ind_csx_alt *) +lemma aaa_ind_csx_cpxs: ∀h,o,G,L,A. ∀R:predicate term. + (∀T1. ⦃G, L⦄ ⊢ T1 ⁝ A → + (∀T2. ⦃G, L⦄ ⊢ T1 ⬈*[h] T2 → (T1 ≡[h, o] T2 → ⊥) → R T2) → R T1 + ) → + ∀T. ⦃G, L⦄ ⊢ T ⁝ A → R T. +/5 width=9 by aaa_ind_csx_cpxs_aux, aaa_csx/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma index e2a5ee4d9..09d004b2c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lfpxs.ma @@ -12,6 +12,7 @@ (* *) (**************************************************************************) +include "basic_2/i_static/tc_lfxs_tc_lfxs.ma". include "basic_2/rt_computation/lfpxs.ma". (* UNCOUNTED PARALLEL RT-COMPUTATION FOR LOCAL ENV.S ON REFERRED ENTRIES ****) @@ -20,5 +21,4 @@ include "basic_2/rt_computation/lfpxs.ma". (* 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-. +/2 width=3 by tc_lfxs_trans/ 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 16ff258d1..876994e66 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_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.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_aaa.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_lfpxs.ma lfsx_lfsx.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 f55e45f41..a11a40126 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,11 @@ Stage "A2": "Extending the Applicability Condition" + + Strong rt-normalization + for simply typed terms + (anniversary milestone). + First behavioral component reconstructed: rt_transition. 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 bf098d4a9..db3bcf966 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 @@ -115,7 +115,7 @@ table { *) [ "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" * ] + [ "csx ( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_csx" * ] [ "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_length" + "tc_lfxs_fqup" * ] + [ "tc_lfxs ( ? ⦻**[?,?] ? )" "tc_lfxs_length" + "tc_lfxs_fqup" + "tc_lfxs_tc_lfxs" * ] } ] }