From b5ded5b0c305b30349339b24760820154f7de390 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Thu, 26 Jan 2017 21:13:39 +0000 Subject: [PATCH] - some commutations between the rt-steps and the s-steps proved - some bugs fixed --- matita/components/binaries/Makefile | 2 +- matita/components/binaries/Makefile.common | 2 +- .../lambdadelta/basic_2/relocation/lifts.ma | 7 ++ .../basic_2/relocation/lifts_tdeq.ma | 60 ++++++++++++++++ .../basic_2/rt_transition/cpx_fqus.ma | 71 ++++++++++--------- .../lambdadelta/basic_2/rt_transition/hls.ml | 5 +- .../basic_2/rt_transition/partial.txt | 2 +- .../lambdadelta/basic_2/syntax/tdeq.ma | 6 ++ .../lambdadelta/basic_2/web/basic_2_src.tbl | 6 +- 9 files changed, 120 insertions(+), 41 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma diff --git a/matita/components/binaries/Makefile b/matita/components/binaries/Makefile index 15ff284f3..2f2faf326 100644 --- a/matita/components/binaries/Makefile +++ b/matita/components/binaries/Makefile @@ -4,7 +4,7 @@ H=@ #CSC: by Andrea #BINARIES=extractor table_creator utilities saturate transcript #FG: my binaries -BINARIES=mac matex matitadep probe xoa +BINARIES=matex matitadep probe xoa all: $(BINARIES:%=rec@all@%) opt: $(BINARIES:%=rec@opt@%) diff --git a/matita/components/binaries/Makefile.common b/matita/components/binaries/Makefile.common index 8f8033dbb..78733ed39 100644 --- a/matita/components/binaries/Makefile.common +++ b/matita/components/binaries/Makefile.common @@ -9,7 +9,7 @@ OCAMLOPTIONS = -linkpkg -thread -rectypes -package \"$(REQUIRES)\" OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLOPTIONS) OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) -all: +opt: @echo " OCAMLBUILD $(EXEC).native" $(H)ocamlbuild -ocamlc "$(OCAMLC)" -ocamlopt "$(OCAMLOPT)" $(EXEC).native diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma index 73f3be9e7..afb3e127a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts.ma @@ -41,6 +41,13 @@ interpretation "uniform relocation (term)" interpretation "generic relocation (term)" 'RLiftStar f T1 T2 = (lifts f T1 T2). +definition liftable2: predicate (relation term) ≝ + λR. ∀T1,T2. R T1 T2 → ∀f,U1. ⬆*[f] T1 ≡ U1 → + ∃∃U2. ⬆*[f] T2 ≡ U2 & R U1 U2. + +definition deliftable2_sn: predicate (relation term) ≝ + λR. ∀U1,U2. R U1 U2 → ∀f,T1. ⬆*[f] T1 ≡ U1 → + ∃∃T2. ⬆*[f] T2 ≡ U2 & R T1 T2. (* Basic inversion lemmas ***************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma new file mode 100644 index 000000000..205514ce6 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_tdeq.ma @@ -0,0 +1,60 @@ +(**************************************************************************) +(* ___ *) +(* ||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/relocation/lifts.ma". + +(* GENERIC RELOCATION FOR TERMS *********************************************) + +(* Properties with degree-based equivalence for terms ***********************) + +lemma tdeq_lifts: ∀h,o. liftable2 (tdeq h o). +#h #o #T1 #T2 #H elim H -T1 -T2 [||| * ] +[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort1 … H) -H + /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/ +| #i #f #X #H elim (lifts_inv_lref1 … H) -H + /3 width=3 by lifts_lref, tdeq_lref, ex2_intro/ +| #l #f #X #H >(lifts_inv_gref1 … H) -H + /2 width=3 by lifts_gref, tdeq_gref, ex2_intro/ +| #p #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_bind1 … H) -H + #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1 + /3 width=5 by lifts_bind, tdeq_pair, ex2_intro/ +| #I #V1 #V2 #T1 #T2 #_ #_ #IHV #IHT #f #X #H elim (lifts_inv_flat1 … H) -H + #W1 #U1 #HVW1 #HTU1 #H destruct + elim (IHV … HVW1) -V1 elim (IHT … HTU1) -T1 + /3 width=5 by lifts_flat, tdeq_pair, ex2_intro/ +] +qed-. + +(* Inversion lemmas with degree-based equivalence for terms *****************) + +lemma tdeq_inv_lifts: ∀h,o. deliftable2_sn (tdeq h o). +#h #o #U1 #U2 #H elim H -U1 -U2 [||| * ] +[ #s1 #s2 #d #Hs1 #Hs2 #f #X #H >(lifts_inv_sort2 … H) -H + /3 width=5 by lifts_sort, tdeq_sort, ex2_intro/ +| #i #f #X #H elim (lifts_inv_lref2 … H) -H + /3 width=3 by lifts_lref, tdeq_lref, ex2_intro/ +| #l #f #X #H >(lifts_inv_gref2 … H) -H + /2 width=3 by lifts_gref, tdeq_gref, ex2_intro/ +| #p #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_bind2 … H) -H + #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1 + /3 width=5 by lifts_bind, tdeq_pair, ex2_intro/ +| #I #W1 #W2 #U1 #U2 #_ #_ #IHW #IHU #f #X #H elim (lifts_inv_flat2 … H) -H + #V1 #T1 #HVW1 #HTU1 #H destruct + elim (IHW … HVW1) -W1 elim (IHU … HTU1) -U1 + /3 width=5 by lifts_flat, tdeq_pair, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma index c8aaacf06..8bc29f301 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/cpx_fqus.ma @@ -14,6 +14,7 @@ (* UNCOUNTED CONTEXT-SENSITIVE PARALLEL RT-TRANSITION FOR TERMS *************) +include "basic_2/relocation/lifts_tdeq.ma". include "basic_2/s_computation/fqus_fqup.ma". include "basic_2/rt_transition/cpx_drops.ma". @@ -62,65 +63,67 @@ lemma fqus_cpx_trans: ∀h,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T | * #H1 #H2 #H3 destruct /2 width=3 by ex2_intro/ ] qed-. -(* -lemma fqu_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. + +lemma fqu_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐ ⦃G2, L2, U2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -[ #I #G #L #V1 #V2 #HV12 #_ elim (lift_total V2 0 1) +[ #I #G #L #V1 #V2 #HV12 #_ elim (lifts_total V2 𝐔❴1❵) #U2 #HVU2 @(ex3_intro … U2) - [1,3: /3 width=7 by fqu_drop, cpx_delta, drop_pair, drop_drop/ - | #H destruct - lapply (lift_inv_lref2_be … HVU2 ? ?) -HVU2 // + [1,3: /3 width=7 by cpx_delta, fqu_drop/ + | #H lapply (tdeq_inv_lref1 … H) -H + #H destruct /2 width=5 by lifts_inv_lref2_uni_lt/ ] -| #I #G #L #V1 #T #V2 #HV12 #H @(ex3_intro … (②{I}V2.T)) +| #I #G #L #V1 #T #V2 #HV12 #H0 @(ex3_intro … (②{I}V2.T)) [1,3: /2 width=4 by fqu_pair_sn, cpx_pair_sn/ - | #H0 destruct /2 width=1 by/ + | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] -| #a #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓑ{a,I}V.T2)) +| #p #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓑ{p,I}V.T2)) [1,3: /2 width=4 by fqu_bind_dx, cpx_bind/ - | #H0 destruct /2 width=1 by/ + | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ ] -| #I #G #L #V #T1 #T2 #HT12 #H @(ex3_intro … (ⓕ{I}V.T2)) +| #I #G #L #V #T1 #T2 #HT12 #H0 @(ex3_intro … (ⓕ{I}V.T2)) [1,3: /2 width=4 by fqu_flat_dx, cpx_flat/ - | #H0 destruct /2 width=1 by/ + | #H elim (tdeq_inv_pair … H) -H /2 width=1 by/ + ] +| #I #G #L #V #T1 #U1 #HTU1 #T2 #HT12 #H0 + elim (cpx_lifts … HT12 (Ⓣ) … (L.ⓑ{I}V) … HTU1) -HT12 /3 width=1 by drops_refl, drops_drop/ + #U2 #HTU2 #HU12 @(ex3_intro … U2) + [1,3: /3 width=1 by fqu_drop/ + | #H elim (tdeq_inv_lifts … H … HTU1) -U1 + #X2 #H <(lifts_inj … HTU2 … H) -U2 /2 width=1 by/ ] -| #G #L #K #T1 #U1 #k #HLK #HTU1 #T2 #HT12 #H elim (lift_total T2 0 (k+1)) - #U2 #HTU2 @(ex3_intro … U2) - [1,3: /2 width=10 by cpx_lift, fqu_drop/ - | #H0 destruct /3 width=5 by lift_inj/ ] qed-. -lemma fquq_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fquq_inv_gen … H12) -H12 -[ #H12 elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 +lemma fquq_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐⸮ ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 elim H12 -H12 +[ #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fquq, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. -lemma fqup_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. +lemma fqup_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐+ ⦃G2, L2, U2⦄. #h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind_dx … H) -G1 -L1 -T1 -[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_neq … H12 … HTU2 H) -T2 +[ #G1 #L1 #T1 #H12 #U2 #HTU2 #H elim (fqu_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqu_fqup, ex3_intro/ | #G #G1 #L #L1 #T #T1 #H1 #_ #IH12 #U2 #HTU2 #H elim (IH12 … HTU2 H) -T2 - #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_neq … H1 … HTU1 H) -T1 + #U1 #HTU1 #H #H12 elim (fqu_cpx_trans_ntdeq … H1 … HTU1 H) -T1 /3 width=8 by fqup_strap2, ex3_intro/ ] qed-. -lemma fqus_cpx_trans_neq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h, o] U2 → (T2 = U2 → ⊥) → - ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h, o] U1 & T1 = U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_gen … H12) -H12 -[ #H12 elim (fqup_cpx_trans_neq … H12 … HTU2 H) -T2 +lemma fqus_cpx_trans_ntdeq: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → + ∀U2. ⦃G2, L2⦄ ⊢ T2 ⬈[h] U2 → (T2 ≡[h, o] U2 → ⊥) → + ∃∃U1. ⦃G1, L1⦄ ⊢ T1 ⬈[h] U1 & T1 ≡[h, o] U1 → ⊥ & ⦃G1, L1, U1⦄ ⊐* ⦃G2, L2, U2⦄. +#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #U2 #HTU2 #H elim (fqus_inv_fqup … H12) -H12 +[ #H12 elim (fqup_cpx_trans_ntdeq … H12 … HTU2 H) -T2 /3 width=4 by fqup_fqus, ex3_intro/ | * #HG #HL #HT destruct /3 width=4 by ex3_intro/ ] qed-. -*) \ No newline at end of file diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml index 01f59045d..d796a4a66 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/hls.ml @@ -1,4 +1,6 @@ -let cols = int_of_string (Sys.getenv "COLUMNS") +let cols = + try int_of_string (Sys.getenv "COLUMNS") + with Not_found -> failwith "environment variable COLUMNS not visible" let hl = ref [] @@ -52,3 +54,4 @@ let main = Array.fast_sort compare files; let c = Array.fold_left (write l) 0 files in if 0 < c && c < cols then print_newline (); + diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt index 716b8611f..f2ca8d42a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/partial.txt @@ -1,5 +1,5 @@ cpg.ma cpg_simple.ma cpg_drops.ma cpg_lsubr.ma -cpx.ma cpx_simple.ma cpx_drops.ma cpx_lsubr.ma +cpx.ma cpx_simple.ma cpx_drops.ma cpx_fqus.ma cpx_lsubr.ma lfpx.ma lfpx_length.ma lfpx_drops.ma lfpx_fqup.ma lfpx_frees.ma lfpx_aaa.ma cpm.ma cpm_simple.ma cpm_drops.ma cpm_lsubr.ma cpm_cpx.ma cpr.ma cpr_drops.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma index b1658534c..21d140e51 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/tdeq.ma @@ -103,6 +103,12 @@ lemma tdeq_inv_sort1_deg: ∀h,o,Y,s1. ⋆s1 ≡[h, o] Y → ∀d. deg h o s1 d #s2 #x #Hx <(deg_mono h o … Hx … Hs1) -s1 -d /2 width=3 by ex2_intro/ qed-. +lemma tdeq_inv_pair: ∀h,o,I,V1,V2,T1,T2. ②{I}V1.T1 ≡[h, o] ②{I}V2.T2 → + V1 ≡[h, o] V2 ∧ T1 ≡[h, o] T2. +#h #o #I #V1 #V2 #T1 #T2 #H elim (tdeq_inv_pair1 … H) -H +#V0 #T0 #HV #HT #H destruct /2 width=1 by conj/ +qed-. + (* Basic forward lemmas *****************************************************) lemma tdeq_fwd_atom1: ∀h,o,I,Y. ⓪{I} ≡[h, o] Y → ∃J. Y = ⓪{J}. 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 a0f7ae830..d98e42c5c 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 @@ -139,7 +139,7 @@ table { ] [ { "context-sensitive rt-reduction" * } { [ "lpx_lleq" * ] - [ "cpx_lreq" + "cpx_fqus" + "cpx_llpx_sn" + "cpx_lleq" * ] + [ "cpx_lreq" + "cpx_llpx_sn" + "cpx_lleq" * ] } ] *) @@ -151,7 +151,7 @@ table { ] [ { "uncounted context-sensitive rt-transition" * } { [ "lfpx ( ⦃?,?⦄ ⊢ ⬈[?,?] ? )" "lfpx_length" + "lfpx_drops" + "lfpx_fqup" + "lfpx_frees" + "lfpx_aaa" * ] - [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_lsubr" * ] + [ "cpx ( ⦃?,?⦄ ⊢ ? ⬈[?] ? )" "cpx_simple" + "cpx_drops" + "cpx_fqus" + "cpx_lsubr" * ] } ] [ { "counted context-sensitive rt-transition" * } { @@ -223,7 +223,7 @@ table { ] [ { "generic relocation for terms" * } { [ "lifts_vector ( ⬆*[?] ? ≡ ? )" "lifts_lifts_vector" * ] - [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_lifts" * ] + [ "lifts ( ⬆*[?] ? ≡ ? )" "lifts_simple" + "lifts_weight" + "lifts_tdeq" + "lifts_lifts" * ] } ] [ { "ranged equivalence for local environments" * } { -- 2.39.2