bug fix in big-tree reduction

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
index 98a890ffe34f7014f187dc748bab4d09fe167a4c..5a7e77736f3eaa4bf6b87171d745cf5a32ebefdc 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbg.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstarproper_8.ma".
+include "basic_2/substitution/fsupp.ma".
 include "basic_2/reduction/fpbc.ma".
 include "basic_2/computation/fpbs.ma".
 
@@ -69,7 +70,7 @@ qed-.
 
 lemma fsupp_fpbg: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ >[h, g] ⦃G2, L2, T2⦄.
 #h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/3 width=5 by fsupp_fpbs, fpbc_fsup, fpbc_fpbg, fpbg_inj/
+/4 width=5 by fpbg_strap1, fpbc_fpbg, fpbc_fsup, fpb_fsupq, fsup_fsupq/
 qed.
 
 lemma cpxs_fpbg: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → (T1 = T2 → ⊥) →

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
index dc8e8f1853676a60d62fd42ae4a835bacc7cb649..ebebb4577274f4aac0baa2f10d32aba296b20d2e 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs.ma
@@ -13,7 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredstar_8.ma".
-include "basic_2/substitution/fsupp.ma".
+include "basic_2/substitution/fsups.ma".
 include "basic_2/reduction/fpb.ma".
 include "basic_2/computation/cpxs.ma".
 include "basic_2/computation/lpxs.ma".
@@ -55,11 +55,10 @@ lemma fpbs_strap2: ∀h,g,G1,G,G2,L1,L,L2,T1,T,T2. ⦃G1, L1, T1⦄ ≽[h, g] 
                    ⦃G, L, T⦄ ≥[h, g] ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
 /2 width=5 by tri_TC_strap/ qed-.
 
-(* Note: this is a general property of bi_TC *)
-lemma fsupp_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃+ ⦃G2, L2, T2⦄ →
+lemma fsups_fpbs: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L2, T2⦄ →
                   ⦃G1, L1, T1⦄ ≥[h, g] ⦃G2, L2, T2⦄.
-#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsupp_ind … L2 T2 H) -G2 -L2 -T2
-/3 width=5 by fpb_fsup, tri_step, fpb_fpbs/
+#h #g #G1 #G2 #L1 #L2 #T1 #T2 #H @(fsups_ind … L2 T2 H) -G2 -L2 -T2 
+/3 width=5 by fpb_fsupq, tri_step/
 qed.
 
 lemma cpxs_fpbs: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡*[h, g] T2 → ⦃G, L, T1⦄ ≥[h, g] ⦃G, L, T2⦄.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
new file mode 100644 (file)
index 0000000..f04f358
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/computation/fpbs_alt.ma
@@ -0,0 +1,34 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/btpredstaralt_8.ma".
+include "basic_2/computation/fpbs_fpbs.ma".
+
+(* "BIG TREE" PARALLEL COMPUTATION FOR CLOSURES *****************************)
+
+(* Note: alternative definition of fpbs *)
+definition fpbsa: ∀h. sd h → tri_relation genv lenv term ≝
+                  λh,g,G1,L1,T1,G2,L2,T2.
+                  ∃∃L,T. ⦃G1, L1, T1⦄ ⊃* ⦃G2, L, T⦄ & ⦃G2, L⦄ ⊢ T ➡*[h, g] T2 & ⦃G2, L⦄ ⊢ ➡*[h, g] L2.
+
+interpretation "'big tree' parallel computation (closure) alternative"
+   'BTPRedStarAlt h g G1 L1 T1 G2 L2 T2 = (fpbsa h g G1 L1 T1 G2 L2 T2).
+
+(* Main inversion lemmas ****************************************************)
+
+theorem fpbsa_inv_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 * 
+/4 width=5 by fpbs_trans, fsups_fpbs, cpxs_fpbs, lpxs_fpbs/
+qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.ma
new file mode 100644 (file)
index 0000000..227a666
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/btpredstaralt_8.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 h, break term 46 g ] break ⦃ term 46 G2, break term 46 L2 , break term 46 T2 ⦄ )"
+   non associative with precedence 45
+   for @{ 'BTPRedStarAlt $h $g $G1 $L1 $T1 $G2 $L2 $T2 }.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
index 947c4eda31bbf298095a30fde527d7325a861ff8..734e7b5976a371a759958ce0c3b85e016938aaed 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpb.ma
@@ -13,15 +13,15 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpred_8.ma".
-include "basic_2/relocation/fsup.ma".
+include "basic_2/relocation/fsupq.ma".
 include "basic_2/reduction/lpx.ma".
 
 (* "BIG TREE" PARALLEL REDUCTION FOR CLOSURES *******************************)
 
 inductive fpb (h) (g) (G1) (L1) (T1): relation3 genv lenv term ≝
-| fpb_fsup: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
-| fpb_cpx : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
-| fpb_lpx : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
+| fpb_fsupq: ∀G2,L2,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → fpb h g G1 L1 T1 G2 L2 T2
+| fpb_cpx  : ∀T2. ⦃G1, L1⦄ ⊢ T1 ➡[h, g] T2 → fpb h g G1 L1 T1 G1 L1 T2
+| fpb_lpx  : ∀L2. ⦃G1, L1⦄ ⊢ ➡[h, g] L2 → fpb h g G1 L1 T1 G1 L2 T1
 .
 
 interpretation

diff --git a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
index a485258adacfc317d6389fae1e9ab36b88285780..a2b62d2a12eb464a58b747d3e1a3c1dc3cf2f508 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/reduction/fpbc.ma
@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 include "basic_2/notation/relations/btpredproper_8.ma".
+include "basic_2/relocation/fsupq_alt.ma".
 include "basic_2/reduction/fpb.ma".
 
 (* "BIG TREE" PROPER PARALLEL REDUCTION FOR CLOSURES ************************)
@@ -31,7 +32,7 @@ interpretation
 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
-/2 width=1 by fpb_fsup, fpb_cpx/
+/3 width=1 by fpb_fsupq, fpb_cpx, fsup_fsupq/
 qed.
 
 lemma cpr_fpbc: ∀h,g,G,L,T1,T2. ⦃G, L⦄ ⊢ T1 ➡ T2 → (T1 = T2 → ⊥) →
@@ -44,7 +45,10 @@ lemma fpb_inv_fpbc: ∀h,g,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≽[h, g] ⦃G2,
                    ⦃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_introl, or_intror, fpbc_fsup/
-#T2 #HT12 elim (term_eq_dec T1 T2) #H destruct
-/4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/
+/3 width=1 by and3_intro, or_intror/
+[ #G2 #L2 #T2 #H elim (fsupq_inv_gen … H) -H [| * ]
+  /3 width=1 by fpbc_fsup, and3_intro, or_introl, or_intror/
+| #T2 #HT12 elim (term_eq_dec T1 T2) #H destruct
+  /4 width=1 by and3_intro, or_introl, or_intror, fpbc_cpx/
+]
 qed-.

diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
index e9bc6c533e310956ea03ae853de6cc3fbc13db9a..54e161f7f4dc165115880e2f81f613ea493ae739 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/fsupq_alt.ma
@@ -33,19 +33,29 @@ lemma fsupqa_ldrop: ∀G1,G2,K1,K2,T1,T2. ⦃G1, K1, T1⦄ ⊃⊃⸮ ⦃G2, K2,
                     ∀L1,d,e. ⇩[d, e] L1 ≡ K1 →
                     ∀U1. ⇧[d, e] T1 ≡ U1 → ⦃G1, L1, U1⦄ ⊃⊃⸮ ⦃G2, K2, T2⦄.
 #G1 #G2 #K1 #K2 #T1 #T2 * [ /3 width=7/ ] * #H1 #H2 #H3 destruct
-#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e) [2: /3 width=5/ ] #H destruct
+#L1 #d #e #HLK #U1 #HTU elim (eq_or_gt e)
+/3 width=5 by fsup_ldrop_lt, or_introl/ #H destruct
 >(ldrop_inv_O2 … HLK) -L1 >(lift_inv_O2 … HTU) -T2 -d //
 qed.
 
 (* Main properties **********************************************************)
 
 theorem fsupq_fsupqa: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 // /2 width=1/ /2 width=7/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2
+/2 width=7 by fsupqa_ldrop, fsup_lref_O, fsup_pair_sn, fsup_bind_dx, fsup_flat_dx, or_introl/
 qed.
 
 (* Main inversion properties ************************************************)
 
 theorem fsupqa_inv_fsupq: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⊃⸮ ⦃G2, L2, T2⦄ → ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄.
-#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1/
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim H -H /2 width=1 by fsup_fsupq/
 * #H1 #H2 #H3 destruct //
 qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma fsupq_inv_gen: ∀G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊃⸮ ⦃G2, L2, T2⦄ →
+⦃G1, L1, T1⦄ ⊃ ⦃G2, L2, T2⦄ ∨ (∧∧ G1 = G2 & L1 = L2 & T1 = T2).
+#G1 #G2 #L1 #L2 #T1 #T2 #H elim (fsupq_fsupqa … H) -H [| * ]
+/2 width=1 by or_introl/
+qed-.

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 a7ffa62aa1d0d96ea3c66d83477a616ad7ac20a7..c5f04455d1d290176b116c802e66a345ee34a132 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -86,7 +86,7 @@ table {
         ]
         [ { "\"big tree\" parallel computation" * } {
              [ "fpbg ( ⦃?,?,?⦄ >[?,?] ⦃?,?,?⦄ )" "fpbg_lift" + "fpbg_fpbg" * ]
-             [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
+             [ "fpbs ( ⦃?,?,?⦄ ≥[?,?] ⦃?,?,?⦄ )" "fpbs_alt ( ⦃?,?,?⦄ ≥≥[?,?] ⦃?,?,?⦄ )" "fpbs_lift" + "fpbs_fpbs" * ]
           }
         ]
         [ { "decomposed extended computation" * } {