From 12023ae1e3d075130b31d2d8559c85847ef06dee Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 19 Oct 2013 14:49:35 +0000 Subject: [PATCH] more results towards the "big-tree" theorem ... --- .../basic_2/computation/csx_aaa.ma | 2 +- .../lambdadelta/basic_2/computation/fsb.ma | 9 +++- .../lambdadelta/basic_2/grammar/bteq.ma | 46 +++++++++++++++++++ .../lambdadelta/basic_2/grammar/bteq_bteq.ma | 23 ++++++++++ .../basic_2/notation/relations/bteq_6.ma | 19 ++++++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + matita/matita/predefined_virtuals.ml | 2 +- 7 files changed, 99 insertions(+), 3 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma create mode 100644 matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma index d951e4154..43e4d3ad5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/csx_aaa.ma @@ -17,7 +17,7 @@ include "basic_2/computation/csx_tstc_vector.ma". (* CONTEXT-SENSITIVE EXTENDED STRONGLY NORMALIZING TERMS ********************) -(* Main properties concerning atomic arity assignment ***********************) +(* Main properties on atomic arity assignment *******************************) theorem aaa_csx: ∀h,g,G,L,T,A. ⦃G, L⦄ ⊢ T ⁝ A → ⦃G, L⦄ ⊢ ⬊*[h, g] T. #h #g #G #L #T #A #H diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma index 0ad3212fc..f8996e4a9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -14,12 +14,13 @@ include "basic_2/notation/relations/btsn_5.ma". include "basic_2/reduction/fpbc.ma". +include "basic_2/computation/csx.ma". (* "BIG TREE" STRONGLY NORMALIZING TERMS ************************************) inductive fsb (h) (g): relation3 genv lenv term ≝ | fsb_intro: ∀G1,L1,T1. ( - ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2 + ∀G2,L2,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → fsb h g G2 L2 T2 ) → fsb h g G1 L1 T1 . @@ -41,3 +42,9 @@ theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. ( ∀G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → R G L T. #h #g #R #IH #G #L #T #H elim H -G -L -T /5 width=1 by fpb_fpbc/ qed-. + +(* Basic inversion lemmas ***************************************************) + +lemma fsb_inv_csx: ∀h,g,G,L,T. ⦃G, L⦄ ⊢ ⦥[h, g] T → ⦃G, L⦄ ⊢ ⬊*[h, g] T. +#h #g #G #L #T #H elim H -G -L -T /5 width=1 by csx_intro, fpbc_cpx/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma new file mode 100644 index 000000000..73e04e3d5 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq.ma @@ -0,0 +1,46 @@ +(**************************************************************************) +(* ___ *) +(* ||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/bteq_6.ma". +include "basic_2/grammar/lenv_length.ma". +include "basic_2/grammar/genv.ma". + +(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) + +definition bteq: tri_relation genv lenv term ≝ + λG1,L1,T1,G2,L2,T2. + ∧∧ G1 = G2 & |L1| = |L2| & T1 = T2. + +interpretation + "equivalent 'big tree' normal forms (closure)" + 'BTEq G1 L1 T1 G2 L2 T2 = (bteq G1 L1 T1 G2 L2 T2). + +(* Basic_properties *********************************************************) + +lemma bteq_refl: tri_reflexive … bteq. +/2 width=1 by and3_intro/ qed. + +lemma bteq_sym: tri_symmetric … bteq. +#G1 #G2 #L1 #L2 #T1 #T2 * // +qed-. + +lemma bteq_dec: ∀G1,G2,L1,L2,T1,T2. Decidable (⦃G1, L1, T1⦄ ⪴ ⦃G2, L2, T2⦄). +#G1 #G2 #L1 #L2 #T1 #T2 elim (genv_eq_dec G1 G2) +#H1G [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] +elim (eq_nat_dec (|L1|) (|L2|)) +#H1L [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] +elim (term_eq_dec T1 T2) +#H1T [2: @or_intror * #H2G #H2L #H2T destruct /2 width=1 by/ ] +/3 width=1 by and3_intro, or_introl/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.ma new file mode 100644 index 000000000..4dad596fd --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/grammar/bteq_bteq.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/grammar/bteq.ma". + +(* EQUIVALENT "BIG TREE" NORMAL FORMS ***************************************) + +(* Main properties **********************************************************) + +theorem bteq_trans: tri_transitive … bteq. +#G1 #G #L1 #L #T1 #T * // +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma new file mode 100644 index 000000000..a417d0ac7 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/bteq_6.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) + +notation "hvbox( ⦃ term 46 G1, break term 46 L1, break term 46 T1 ⦄ ⪴ break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )" + non associative with precedence 45 + for @{ 'BTEq $G1 $L1 $T1 $G2 $L2 $T2 }. 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 c43385009..e7a665c66 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 @@ -254,6 +254,7 @@ table { } ] [ { "closures" * } { + [ "bteq ( ⦃?,?,?⦄ ⪴ ⦃?,?,?⦄ )" "bteq_bteq" * ] [ "cl_shift ( ? @@ ? )" "cl_weight ( ♯{?,?,?} )" * ] } ] diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml index 6cf8ab99f..32e750973 100644 --- a/matita/matita/predefined_virtuals.ml +++ b/matita/matita/predefined_virtuals.ml @@ -1528,7 +1528,7 @@ let predefined_classes = [ ["□"; "◽"; "▪"; "◾"; ]; ["◊"; "♢"; "⧫"; "♦"; "⟐"; "⟠"; ] ; [">"; "⭃"; "⧁"; "〉"; "»"; "❭"; "❯"; "❱"; "▸"; "►"; "▶"; ] ; - ["≥"; "⪀"; "≽"; "⥸"; ]; + ["≥"; "⪀"; "≽"; "⪴"; "⥸"; ]; ["a"; "α"; "𝕒"; "𝐚"; "𝛂"; "ⓐ"; ] ; ["A"; "ℵ"; "𝔸"; "𝐀"; "Ⓐ"; ] ; ["b"; "β"; "ß"; "𝕓"; "𝐛"; "𝛃"; "ⓑ"; ] ; -- 2.39.2