update in basic_2

+ advances on fpb completed

diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile
index e5a76486a2d72b066c2d84f9f8732324b5ebdcf7..ff89218d28f0967256f588ef11c30af77296cb02 100644 (file)
--- a/matita/matita/contribs/lambdadelta/Makefile
+++ b/matita/matita/contribs/lambdadelta/Makefile
@@ -28,7 +28,7 @@ ORIGS        := basic_2/basic_1.orig
 
 CONTRIB      := lambdadelta_2
 
-TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib
+TAGS := all xoa xoa2 orig elim deps top leaf stats tbls trim contrib clean
 
 PACKAGES  := ground_2 basic_2 apps_2 alpha_1
 XPACKAGES := ground_2 basic_2
@@ -254,6 +254,11 @@ contrib:
        @echo "  TAR -czf $(CONTRIB).tar.gz root $(XPACKAGES)"
        $(H)tar -czf $(CONTRIB).tar.gz root $(XMAS)
 
+# clean ######################################################################
+
+clean:
+       @$(RM) `find -name "*~" -type f -print`
+
 ##############################################################################
 
 .PHONY: $(TAGS)

diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma
index 1d0d211d5701fa8882d4100e6375ae134ee3e400..5052736d8947daf6449fbd91e754e8209b732cab 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/fpb_ffdeq.ma
@@ -12,6 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
+include "basic_2/s_transition/fqu_tdeq.ma".
 include "basic_2/static/ffdeq.ma".
 include "basic_2/rt_transition/fpb_lfdeq.ma".
 
@@ -32,19 +33,14 @@ elim (lfdeq_fpb_trans … HK12 … H) -K2 #L0 #U0 #H #HUT0 #HLK0
 qed-.
 
 (* Inversion lemmas with degree-based equivalence for closures **************)
-(*
+
 (* Basic_2A1: uses: fpb_inv_fleq *)
 lemma fpb_inv_ffdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ≻[h, o] ⦃G2, L2, T2⦄ →
                      ⦃G1, L1, T1⦄ ≛[h, o] ⦃G2, L2, T2⦄ → ⊥.
 #h #o #G1 #G2 #L1 #L2 #T1 #T2 * -G2 -L2 -T2
 [ #G2 #L2 #T2 #H12 #H elim (ffdeq_inv_gen_sn … H) -H
-  #_ #H1 #H2
-(*
-
-  /3 width=8 by lfdeq_fwd_length, fqu_inv_eq/
-*)  
+  /3 width=11 by lfdeq_fwd_length, fqu_inv_tdeq/
 | #T2 #_ #HnT #H elim (ffdeq_inv_gen_sn … H) -H /2 width=1 by/
 | #L2 #_ #HnL #H elim (ffdeq_inv_gen_sn … H) -H /2 width=1 by/
 ]
 qed-.
-*)
\ No newline at end of file

diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma
index 712777ec45c7a54126c3d53ec8b2db7c2beb1fa2..467283ff1f6975a9fd6f0ec26db748b22aac0b88 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_length.ma
@@ -29,18 +29,3 @@ lemma fqu_fwd_length_lref1: ∀b,G1,G2,L1,L2,T2,i. ⦃G1, L1, #i⦄ ⊐[b] ⦃G2
                             |L2| < |L1|.
 /2 width=8 by fqu_fwd_length_lref1_aux/
 qed-.
-
-(* Inversion lemmas with length for local environments **********************)
-
-fact fqu_inv_eq_aux: ∀b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
-                     G1 = G2 → |L1| = |L2| → T1 = T2 → ⊥.
-#b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
-[1: #I #G #L #V #_ #H elim (succ_inv_refl_sn … H)
-|6: #I #G #L #T #U #_ #_ #H elim (succ_inv_refl_sn … H)
-]
-/2 width=4 by discr_tpair_xy_y, discr_tpair_xy_x/
-qed-.
-
-lemma fqu_inv_eq: ∀b,G,L1,L2,T. ⦃G, L1, T⦄ ⊐[b] ⦃G, L2, T⦄ → |L1| = |L2| → ⊥.
-#b #G #L1 #L2 #T #H #H0 @(fqu_inv_eq_aux … H … H0) // (**) (* full auto fails *)
-qed-. 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_tdeq.ma
new file mode 100644 (file)
index 0000000..2c7d033
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_tdeq.ma
@@ -0,0 +1,36 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/syntax/tdeq.ma".
+include "basic_2/s_transition/fqu_length.ma".
+
+(* SUPCLOSURE ***************************************************************)
+
+(* Inversion lemmas with context-free degree-based equivalence for terms ****)
+
+fact fqu_inv_tdeq_aux: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ →
+                       G1 = G2 → |L1| = |L2| → T1 ≛[h, o] T2 → ⊥.
+#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 * -G1 -G2 -L1 -L2 -T1 -T2
+[1: #I #G #L #V #_ #H elim (succ_inv_refl_sn … H)
+|6: #I #G #L #T #U #_ #_ #H elim (succ_inv_refl_sn … H)
+]
+/2 width=6 by tdeq_inv_pair_xy_y, tdeq_inv_pair_xy_x/
+qed-.
+
+(* Basic_2A1: uses: fqu_inv_eq *)
+lemma fqu_inv_tdeq: ∀h,o,b,G,L1,L2,T1,T2. ⦃G, L1, T1⦄ ⊐[b] ⦃G, L2, T2⦄ →
+                    |L1| = |L2| → T1 ≛[h, o] T2 → ⊥.
+#h #o #b #G #L1 #L2 #T1 #T2 #H
+@(fqu_inv_tdeq_aux … H) // (**) (* full auto fails *)
+qed-. 

diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
index 516c42904f65a58c53842bcc24c72fcac8ad8790..d431b7677a55bd28dc55f1e47578c4c7d06cbcd9 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma
@@ -101,6 +101,13 @@ lemma tdeq_inv_pair: ∀h,o,I1,I2,V1,V2,T1,T2. ②{I1}V1.T1 ≛[h, o] ②{I2}V2.
 #V0 #T0 #HV #HT #H destruct /2 width=1 by and3_intro/
 qed-.
 
+lemma tdeq_inv_pair_xy_x: ∀h,o,I,V,T. ②{I}V.T ≛[h, o] V → ⊥.
+#h #o #I #V elim V -V
+[ #J #T #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct
+| #J #X #Y #IHX #_ #T #H elim (tdeq_inv_pair … H) -H #H #HY #_ destruct /2 width=2 by/
+]
+qed-.
+
 lemma tdeq_inv_pair_xy_y: ∀h,o,I,T,V. ②{I}V.T ≛[h, o] T → ⊥.
 #h #o #I #T elim T -T
 [ #J #V #H elim (tdeq_inv_pair1 … H) -H #X #Y #_ #_ #H destruct

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 e8cb493089dd86e5808d19d23909256d6681c3a6..37b94745b881505d25253cbd36d9b3c197fd5e3a 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
@@ -209,7 +209,7 @@ table {
    [ { "s-transition" * } {
         [ { "structural successor" * } {
              [ [ "for closures" ] "fquq" + "( ⦃?,?,?⦄ ⊐⸮[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐⸮ ⦃?,?,?⦄ )" "fquq_length" + "fquq_weight" * ]
-             [ [ "proper for closures" ] "fqu" + "( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" * ]
+             [ [ "proper for closures" ] "fqu" + "( ⦃?,?,?⦄ ⊐[?] ⦃?,?,?⦄ )" + "( ⦃?,?,?⦄ ⊐ ⦃?,?,?⦄ )" "fqu_length" + "fqu_weight" + "fqu_tdeq" * ]
           }
         ]
      }