From: Ferruccio Guidi Date: Mon, 14 Oct 2013 19:38:22 +0000 (+0000) Subject: strongly normalizing terms for big-tree reduction are now defined ... X-Git-Tag: make_still_working~1079 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f418a6f9fe878f17a2c7afa0d13a361cce140694;p=helm.git strongly normalizing terms for big-tree reduction are now defined ... --- diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma index f400f5c43..cc4ac8889 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma @@ -33,7 +33,7 @@ interpretation "'big tree' proper parallel computation (closure)" lemma fpbg_fwd_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G2 -L2 -T2 -/3 width=5 by fpbs_strap1, fpbc_fpb, fpb_lpx/ +/3 width=5 by fpbs_strap1, fpbc_fwd_fpb, fpb_lpx/ qed-. (* Basic properties *********************************************************) @@ -46,7 +46,7 @@ lemma fpbg_strap1: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ >[h, g] ⦃G ⦃G, L, T⦄ ≽[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄. #h #g #G1 #G #G2 #L1 #L #L2 #T1 #T #T2 #H1 #H2 lapply (fpbg_fwd_fpbs … H1) #H0 -elim (fpb_inv_fpbc … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] +elim (fpb_fpbc_or_refl … H2) -H2 [| * #HG2 #HL2 #HT2 destruct ] /2 width=5 by fpbg_inj, fpbg_step/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma new file mode 100644 index 000000000..0ad3212fc --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fsb.ma @@ -0,0 +1,43 @@ +(**************************************************************************) +(* ___ *) +(* ||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/btsn_5.ma". +include "basic_2/reduction/fpbc.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 + ) → fsb h g G1 L1 T1 +. + +interpretation + "'big tree' strong normalization (closure)" + 'BTSN h g G L T = (fsb h g G L T). + +(* Basic eliminators ********************************************************) + +theorem fsb_ind_alt: ∀h,g. ∀R: relation3 …. ( + ∀G1,L1,T1. ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄≽ [h, g] ⦃G2, L2, T2⦄ → + (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → ⦃G2, L2⦄ ⊢ ⦥[h,g] T2 + ) → ( + ∀G2,L2,T2. ⦃G1, L1, T1⦄≽ [h, g] ⦃G2, L2, T2⦄ → + (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → R G2 L2 T2 + ) → R G1 L1 T1 + ) → + ∀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-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.ma new file mode 100644 index 000000000..d6c4f4259 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsn_5.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 G, break term 46 L ⦄ ⊢ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )" + non associative with precedence 45 + for @{ 'BTSN $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.ma new file mode 100644 index 000000000..44976571b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btsnalt_5.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 G, break term 46 L ⦄ ⊢ ⦥ ⦥ break [ term 46 h , break term 46 g ] break term 46 T )" + non associative with precedence 45 + for @{ 'BTSNAlt $h $g $G $L $T }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma index cb391a6c9..ec64bd5a6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma @@ -29,21 +29,13 @@ interpretation (* Basic properties *********************************************************) -lemma fpbc_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄. -#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 -/3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/ -qed. - lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) → ⦃G, L, T1⦄ ≻[h, g] ⦃G, L, T2⦄. /3 width=1 by fpbc_cpx, cpr_cpx/ qed. -(* Inversion lemmas on "big tree" parallel reduction for closures ***********) - -lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → - ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ - ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. +lemma fpb_fpbc_or_refl: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ ∨ + ∧∧ G1 = G2 & ⦃G1, L1⦄ ⊢ ➡[h, g] L2 & T1 = T2. #h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /3 width=1 by and3_intro, or_intror/ [ #G2 #L2 #T2 #H elim (fquq_inv_gen … H) -H [| * ] @@ -52,3 +44,25 @@ lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/ ] qed-. + +lemma fpb_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄ → + (|G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥) → + ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H #H0 elim (fpb_fpbc_or_refl … H) -H // * +#HG #HL #HT destruct lapply (lpx_fwd_length … HL) -HL #HL +elim H0 -H0 // +qed. + +(* Basic forward lemmas *****************************************************) + +lemma fpbc_fwd_fpb: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2, L2, T2⦄. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 +/3 width=1 by fpb_fquq, fpb_cpx, fqu_fquq/ +qed-. + +lemma fpbc_fwd_gen: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, g] ⦃G2, L2, T2⦄ → + |G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥. +#h #g #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2 /2 width=1 by / +#G2 #L2 #T2 #H #HG #HL #HT @(fqu_fwd_gen … H) -H // (**) (* auto does not work *) +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma index 41c68deaf..1da166cf3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fqu.ma @@ -65,3 +65,16 @@ qed-. lemma fqu_fwd_length_lref1: ∀G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊃ ⦃G2, L2, T2⦄ → |L2| < |L1|. /2 width=7 by fqu_fwd_length_lref1_aux/ qed-. + +lemma fqu_fwd_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → + |G1| = |G2| → |L1| = |L2| → T1 = T2 → ⊥. +#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ #I #G #L #V #_ #H elim (plus_xSy_x_false … H) +| #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_x … H) +| #a #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_y … H) +| #I #G #L #V #T #_ #_ #H elim (discr_tpair_xy_y … H) +| #G #L #K #T #U #e #HLK #_ #_ #H + lapply (ldrop_fwd_length_lt4 … HLK ?) // >H -L #H + elim (lt_refl_false … H) +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/arith.ma index b854c3569..2c47b2873 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/arith.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/arith.ma @@ -80,6 +80,9 @@ qed-. lemma plus_xySz_x_false: ∀z,x,y. x + y + S z = x → ⊥. /2 width=4 by le_plus_xySz_x_false/ qed-. +lemma plus_xSy_x_false: ∀y,x. x + S y = x → ⊥. +/2 width=4 by plus_xySz_x_false/ qed-. + (* Iterators ****************************************************************) (* Note: see also: lib/arithemetcs/bigops.ma *)