From 4738096e93f997fb36d35dd723b87682a2f6de90 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 13 Mar 2018 17:58:12 +0100 Subject: [PATCH] update in basic_2 + advances on fpb completed --- matita/matita/contribs/lambdadelta/Makefile | 7 +++- .../basic_2/rt_transition/fpb_ffdeq.ma | 10 ++---- .../basic_2/s_transition/fqu_length.ma | 15 -------- .../basic_2/s_transition/fqu_tdeq.ma | 36 +++++++++++++++++++ .../lambdadelta/basic_2/syntax/tdeq.ma | 7 ++++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 6 files changed, 53 insertions(+), 24 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/s_transition/fqu_tdeq.ma diff --git a/matita/matita/contribs/lambdadelta/Makefile b/matita/matita/contribs/lambdadelta/Makefile index e5a76486a..ff89218d2 100644 --- 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 1d0d211d5..5052736d8 100644 --- 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 712777ec4..467283ff1 100644 --- 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 index 000000000..2c7d03371 --- /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 516c42904..d431b7677 100644 --- 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 e8cb49308..37b94745b 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 @@ -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" * ] } ] } -- 2.39.2