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 f400f5c437482ae97c2d5b3cf3105679024899b6..cc4ac888986a1e2039f67013ee067802fe5b7457 100644 (file)
--- 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 (file)
index 0000000..0ad3212
--- /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 (file)
index 0000000..d6c4f42
--- /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 (file)
index 0000000..4497657
--- /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 cb391a6c932c96dc276ab03eacff43390a182698..ec64bd5a6642ae4fd5bab4b6a122c0fc0af842e1 100644 (file)
--- 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 41c68deaf7e1b1f680e7ec4b5e188a92574015eb..1da166cf3009bd39b07d5b703ff120be9e33169c 100644 (file)
--- 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 b854c356909aef97473e8bc883bc0965517da022..2c47b2873c9ac03f0fcb26b6c5e8192279fe210a 100644 (file)
--- 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 *)