From 268e7f336d036f77ffc9663358e9afda92b97730 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Fri, 9 Mar 2018 18:21:37 +0100 Subject: [PATCH] update in basic_2 + web page + csx completed + notational change to lreq and lfeq to reduce overloading --- .../basic_2/i_static/tc_lfxs_drops.ma | 2 +- .../basic_2/i_static/tc_lfxs_lex.ma | 4 +- .../relations/{lazyeqsn_3.ma => doteqsn_3.ma} | 4 +- .../lambdadelta/basic_2/relocation/drops.ma | 2 +- .../basic_2/relocation/drops_lexs.ma | 4 +- .../basic_2/relocation/drops_lreq.ma | 12 ++-- .../lambdadelta/basic_2/relocation/lreq.ma | 40 ++++++------ .../basic_2/relocation/lreq_length.ma | 2 +- .../basic_2/relocation/lreq_lreq.ma | 8 +-- .../basic_2/rt_computation/csx_fqus.ma | 62 +++++++++++++------ .../basic_2/rt_computation/lfpxs_lpxs.ma | 4 +- .../basic_2/rt_computation/partial.txt | 2 +- .../basic_2/rt_transition/lfpx_lpx.ma | 2 +- .../lambdadelta/basic_2/static/lfdeq_lfeq.ma | 2 +- .../lambdadelta/basic_2/static/lfeq.ma | 34 +++++----- .../lambdadelta/basic_2/static/lfeq_fsle.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_drops.ma | 2 +- .../lambdadelta/basic_2/static/lfxs_lex.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- 19 files changed, 107 insertions(+), 85 deletions(-) rename matita/matita/contribs/lambdadelta/basic_2/notation/relations/{lazyeqsn_3.ma => doteqsn_3.ma} (91%) diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma index 13aec62e4..2122b0533 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_drops.ma @@ -21,7 +21,7 @@ include "basic_2/i_static/tc_lfxs.ma". definition tc_dedropable_sn: predicate (relation3 lenv term term) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2,T. K1 ⪤**[R, T] K2 → ∀U. ⬆*[f] T ≡ U → - ∃∃L2. L1 ⪤**[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + ∃∃L2. L1 ⪤**[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≐[f] L2. definition tc_dropable_sn: predicate (relation3 lenv term term) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma index e38f9f796..cb32e58b0 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/i_static/tc_lfxs_lex.ma @@ -28,7 +28,7 @@ lemma tc_lfxs_lex: ∀R. c_reflexive … R → qed. lemma tc_lfxs_lex_lfeq: ∀R. c_reflexive … R → - ∀L1,L. L1 ⪤[LTC … R] L → ∀L2,T. L ≡[T] L2 → + ∀L1,L. L1 ⪤[LTC … R] L → ∀L2,T. L ≐[T] L2 → L1 ⪤**[R, T] L2. /3 width=3 by tc_lfxs_lex, tc_lfxs_step_dx, lfeq_fwd_lfxs/ qed. @@ -40,7 +40,7 @@ lemma tc_lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → s_rs_transitive … R (λ_.lex R) → lfeq_transitive R → ∀L1,L2,T. L1 ⪤**[R, T] L2 → - ∃∃L. L1 ⪤[LTC … R] L & L ≡[T] L2. + ∃∃L. L1 ⪤[LTC … R] L & L ≐[T] L2. #R #H1R #H2R #H3R #H4R #L1 #L2 #T #H lapply (s_rs_transitive_lex_inv_isid … H3R) -H3R #H3R @(tc_lfxs_ind_sn … H1R … H) -H -L2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma similarity index 91% rename from matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma rename to matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma index 24b7250e5..96060d509 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/notation/relations/lazyeqsn_3.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/notation/relations/doteqsn_3.ma @@ -14,6 +14,6 @@ (* NOTATION FOR THE FORMAL SYSTEM λδ ****************************************) -notation "hvbox( L1 ≡ [ break term 46 f ] break term 46 L2 )" +notation "hvbox( L1 ≐ [ break term 46 f ] break term 46 L2 )" non associative with precedence 45 - for @{ 'LazyEqSn $f $L1 $L2 }. + for @{ 'DotEqSn $f $L1 $L2 }. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma index 5e8cfaeaa..57bf1bfe5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops.ma @@ -92,7 +92,7 @@ definition co_dropable_dx: predicate (rtmap → relation lenv) ≝ definition co_dedropable_sn: predicate (rtmap → relation lenv) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀f1,K2. R f1 K1 K2 → ∀f2. f ~⊚ f1 ≡ f2 → - ∃∃L2. R f2 L1 L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + ∃∃L2. R f2 L1 L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≐[f] L2. (* Basic properties *********************************************************) diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma index 7cfbf82c0..a3ff3cdac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lexs.ma @@ -163,7 +163,7 @@ lemma drops_lexs_trans_next: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 → ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 → ∀f2. f ~⊚ f1 ≡ ⫯f2 → - ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.ⓘ{I1} ≡[f] L2.ⓘ{I2}. + ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RN L1 I1 I2 & L1.ⓘ{I1} ≐[f] L2.ⓘ{I2}. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_next1 … HX) -HX @@ -175,7 +175,7 @@ lemma drops_lexs_trans_push: ∀RN,RP. (∀L. reflexive ? (RN L)) → (∀L. ref ∀f1,K1,K2. K1 ⪤*[RN, RP, f1] K2 → ∀b,f,I1,L1. ⬇*[b, f] L1.ⓘ{I1} ≡ K1 → ∀f2. f ~⊚ f1 ≡ ↑f2 → - ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.ⓘ{I1} ≡[f] L2.ⓘ{I2}. + ∃∃I2,L2. ⬇*[b, f] L2.ⓘ{I2} ≡ K2 & L1 ⪤*[RN, RP, f2] L2 & RP L1 I1 I2 & L1.ⓘ{I1} ≐[f] L2.ⓘ{I2}. #RN #RP #H1RN #H1RP #H2RN #H2RP #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (lexs_liftable_co_dedropable_sn … H1RN H1RP H2RN H2RP … HLK1 … HK12 … Hf2) -K1 -f1 -H1RN -H1RP -H2RN -H2RP #X #HX #HLK2 #H1L12 elim (lexs_inv_push1 … HX) -HX diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma index a1ca60e4c..bc32717b6 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lreq.ma @@ -29,10 +29,10 @@ lemma lreq_co_dropable_dx: co_dropable_dx lreq. @lexs_co_dropable_dx qed-. (* Basic_2A1: includes: lreq_drop_trans_be *) -lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≡[f2] L2 → +lemma lreq_drops_trans_next: ∀f2,L1,L2. L1 ≐[f2] L2 → ∀b,f,I,K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} → 𝐔⦃f⦄ → ∀f1. f ~⊚ ⫯f1 ≡ f2 → - ∃∃K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} & K1 ≡[f1] K2. + ∃∃K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} & K1 ≐[f1] K2. #f2 #L1 #L2 #HL12 #b #f #I2 #K2 #HLK2 #Hf #f1 #Hf2 elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf #I1 #K1 #HLK1 #HK12 #H <(ceq_ext_inv_eq … H) -I2 @@ -40,19 +40,19 @@ elim (lexs_drops_trans_next … HL12 … HLK2 Hf … Hf2) -f2 -L2 -Hf qed-. (* Basic_2A1: includes: lreq_drop_conf_be *) -lemma lreq_drops_conf_next: ∀f2,L1,L2. L1 ≡[f2] L2 → +lemma lreq_drops_conf_next: ∀f2,L1,L2. L1 ≐[f2] L2 → ∀b,f,I,K1. ⬇*[b, f] L1 ≡ K1.ⓘ{I} → 𝐔⦃f⦄ → ∀f1. f ~⊚ ⫯f1 ≡ f2 → - ∃∃K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} & K1 ≡[f1] K2. + ∃∃K2. ⬇*[b, f] L2 ≡ K2.ⓘ{I} & K1 ≐[f1] K2. #f2 #L1 #L2 #HL12 #b #f #I1 #K1 #HLK1 #Hf #f1 #Hf2 elim (lreq_drops_trans_next … (lreq_sym … HL12) … HLK1 … Hf2) // -f2 -L1 -Hf /3 width=3 by lreq_sym, ex2_intro/ qed-. -lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≡[f1] K2 → +lemma drops_lreq_trans_next: ∀f1,K1,K2. K1 ≐[f1] K2 → ∀b,f,I,L1. ⬇*[b, f] L1.ⓘ{I} ≡ K1 → ∀f2. f ~⊚ f1 ≡ ⫯f2 → - ∃∃L2. ⬇*[b, f] L2.ⓘ{I} ≡ K2 & L1 ≡[f2] L2 & L1.ⓘ{I} ≡[f] L2.ⓘ{I}. + ∃∃L2. ⬇*[b, f] L2.ⓘ{I} ≡ K2 & L1 ≐[f2] L2 & L1.ⓘ{I} ≐[f] L2.ⓘ{I}. #f1 #K1 #K2 #HK12 #b #f #I1 #L1 #HLK1 #f2 #Hf2 elim (drops_lexs_trans_next … HK12 … HLK1 … Hf2) -f1 -K1 /2 width=6 by cfull_lift_sn, ceq_lift_sn/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma index cc3e75b0a..1ec062b82 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeqsn_3.ma". +include "basic_2/notation/relations/doteqsn_3.ma". include "basic_2/syntax/ceq_ext.ma". include "basic_2/relocation/lexs.ma". @@ -23,18 +23,18 @@ definition lreq: relation3 rtmap lenv lenv ≝ lexs ceq_ext cfull. interpretation "ranged equivalence (local environment)" - 'LazyEqSn f L1 L2 = (lreq f L1 L2). + 'DotEqSn f L1 L2 = (lreq f L1 L2). (* Basic properties *********************************************************) -lemma lreq_eq_repl_back: ∀L1,L2. eq_repl_back … (λf. L1 ≡[f] L2). +lemma lreq_eq_repl_back: ∀L1,L2. eq_repl_back … (λf. L1 ≐[f] L2). /2 width=3 by lexs_eq_repl_back/ qed-. -lemma lreq_eq_repl_fwd: ∀L1,L2. eq_repl_fwd … (λf. L1 ≡[f] L2). +lemma lreq_eq_repl_fwd: ∀L1,L2. eq_repl_fwd … (λf. L1 ≐[f] L2). /2 width=3 by lexs_eq_repl_fwd/ qed-. -lemma sle_lreq_trans: ∀f2,L1,L2. L1 ≡[f2] L2 → - ∀f1. f1 ⊆ f2 → L1 ≡[f1] L2. +lemma sle_lreq_trans: ∀f2,L1,L2. L1 ≐[f2] L2 → + ∀f1. f1 ⊆ f2 → L1 ≐[f1] L2. /2 width=3 by sle_lexs_trans/ qed-. (* Basic_2A1: includes: lreq_refl *) @@ -48,54 +48,54 @@ lemma lreq_sym: ∀f. symmetric … (lreq f). (* Basic inversion lemmas ***************************************************) (* Basic_2A1: includes: lreq_inv_atom1 *) -lemma lreq_inv_atom1: ∀f,Y. ⋆ ≡[f] Y → Y = ⋆. +lemma lreq_inv_atom1: ∀f,Y. ⋆ ≐[f] Y → Y = ⋆. /2 width=4 by lexs_inv_atom1/ qed-. (* Basic_2A1: includes: lreq_inv_pair1 *) -lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≡[⫯g] Y → - ∃∃K2. K1 ≡[g] K2 & Y = K2.ⓘ{J}. +lemma lreq_inv_next1: ∀g,J,K1,Y. K1.ⓘ{J} ≐[⫯g] Y → + ∃∃K2. K1 ≐[g] K2 & Y = K2.ⓘ{J}. #g #J #K1 #Y #H elim (lexs_inv_next1 … H) -H #Z #K2 #HK12 #H1 #H2 destruct <(ceq_ext_inv_eq … H1) -Z /2 width=3 by ex2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_zero1 lreq_inv_succ1 *) -lemma lreq_inv_push1: ∀g,J1,K1,Y. K1.ⓘ{J1} ≡[↑g] Y → - ∃∃J2,K2. K1 ≡[g] K2 & Y = K2.ⓘ{J2}. +lemma lreq_inv_push1: ∀g,J1,K1,Y. K1.ⓘ{J1} ≐[↑g] Y → + ∃∃J2,K2. K1 ≐[g] K2 & Y = K2.ⓘ{J2}. #g #J1 #K1 #Y #H elim (lexs_inv_push1 … H) -H /2 width=4 by ex2_2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_atom2 *) -lemma lreq_inv_atom2: ∀f,X. X ≡[f] ⋆ → X = ⋆. +lemma lreq_inv_atom2: ∀f,X. X ≐[f] ⋆ → X = ⋆. /2 width=4 by lexs_inv_atom2/ qed-. (* Basic_2A1: includes: lreq_inv_pair2 *) -lemma lreq_inv_next2: ∀g,J,X,K2. X ≡[⫯g] K2.ⓘ{J} → - ∃∃K1. K1 ≡[g] K2 & X = K1.ⓘ{J}. +lemma lreq_inv_next2: ∀g,J,X,K2. X ≐[⫯g] K2.ⓘ{J} → + ∃∃K1. K1 ≐[g] K2 & X = K1.ⓘ{J}. #g #J #X #K2 #H elim (lexs_inv_next2 … H) -H #Z #K1 #HK12 #H1 #H2 destruct <(ceq_ext_inv_eq … H1) -J /2 width=3 by ex2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_zero2 lreq_inv_succ2 *) -lemma lreq_inv_push2: ∀g,J2,X,K2. X ≡[↑g] K2.ⓘ{J2} → - ∃∃J1,K1. K1 ≡[g] K2 & X = K1.ⓘ{J1}. +lemma lreq_inv_push2: ∀g,J2,X,K2. X ≐[↑g] K2.ⓘ{J2} → + ∃∃J1,K1. K1 ≐[g] K2 & X = K1.ⓘ{J1}. #g #J2 #X #K2 #H elim (lexs_inv_push2 … H) -H /2 width=4 by ex2_2_intro/ qed-. (* Basic_2A1: includes: lreq_inv_pair *) -lemma lreq_inv_next: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[⫯f] L2.ⓘ{I2} → - L1 ≡[f] L2 ∧ I1 = I2. +lemma lreq_inv_next: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≐[⫯f] L2.ⓘ{I2} → + L1 ≐[f] L2 ∧ I1 = I2. #f #I1 #I2 #L1 #L2 #H elim (lexs_inv_next … H) -H /3 width=3 by ceq_ext_inv_eq, conj/ qed-. (* Basic_2A1: includes: lreq_inv_succ *) -lemma lreq_inv_push: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≡[↑f] L2.ⓘ{I2} → L1 ≡[f] L2. +lemma lreq_inv_push: ∀f,I1,I2,L1,L2. L1.ⓘ{I1} ≐[↑f] L2.ⓘ{I2} → L1 ≐[f] L2. #f #I1 #I2 #L1 #L2 #H elim (lexs_inv_push … H) -H /2 width=1 by conj/ qed-. -lemma lreq_inv_tl: ∀f,I,L1,L2. L1 ≡[⫱f] L2 → L1.ⓘ{I} ≡[f] L2.ⓘ{I}. +lemma lreq_inv_tl: ∀f,I,L1,L2. L1 ≐[⫱f] L2 → L1.ⓘ{I} ≐[f] L2.ⓘ{I}. /2 width=1 by lexs_inv_tl/ qed-. (* Basic_2A1: removed theorems 5: diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma index fcb54e71a..69c4efa31 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_length.ma @@ -20,5 +20,5 @@ include "basic_2/relocation/lreq.ma". (* Forward lemmas with length for local environments ************************) (* Basic_2A1: includes: lreq_fwd_length *) -lemma lreq_fwd_length: ∀f,L1,L2. L1 ≡[f] L2 → |L1| = |L2|. +lemma lreq_fwd_length: ∀f,L1,L2. L1 ≐[f] L2 → |L1| = |L2|. /2 width=4 by lexs_fwd_length/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma index ec166cb7d..b2bf0385a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lreq_lreq.ma @@ -28,10 +28,10 @@ theorem lreq_canc_sn: ∀f. left_cancellable … (lreq f). theorem lreq_canc_dx: ∀f. right_cancellable … (lreq f). /3 width=3 by lexs_canc_dx, lreq_trans, lreq_sym/ qed-. -theorem lreq_join: ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 → - ∀f. f1 ⋓ f2 ≡ f → L1 ≡[f] L2. +theorem lreq_join: ∀f1,L1,L2. L1 ≐[f1] L2 → ∀f2. L1 ≐[f2] L2 → + ∀f. f1 ⋓ f2 ≡ f → L1 ≐[f] L2. /2 width=5 by lexs_join/ qed-. -theorem lreq_meet: ∀f1,L1,L2. L1 ≡[f1] L2 → ∀f2. L1 ≡[f2] L2 → - ∀f. f1 ⋒ f2 ≡ f → L1 ≡[f] L2. +theorem lreq_meet: ∀f1,L1,L2. L1 ≐[f1] L2 → ∀f2. L1 ≐[f2] L2 → + ∀f. f1 ⋒ f2 ≡ f → L1 ≐[f] L2. /2 width=5 by lexs_meet/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma index 4ea05ba43..9515e64b9 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/csx_fqus.ma @@ -1,28 +1,50 @@ -lemma csx_fqu_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 -/2 width=8 by csx_inv_lref_bind, csx_inv_lift, csx_fwd_flat_dx, csx_fwd_bind_dx, csx_fwd_pair_sn/ -qed-. +(**************************************************************************) +(* ___ *) +(* ||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/s_computation/fqus.ma". +include "basic_2/rt_computation/csx_lsubr.ma". + +(* STRONGLY NORMALIZING TERMS FOR UNCOUNTED PARALLEL RT-TRANSITION **********) -lemma csx_fquq_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fquq_inv_gen … H12) -H12 -[ /2 width=5 by csx_fqu_conf/ -| * #HG #HL #HT destruct // +(* Properties with extended supclosure **************************************) + +lemma csx_fqu_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐[b] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H elim H -G1 -G2 -L1 -L2 -T1 -T2 +[ /3 width=5 by csx_inv_lref_pair, drops_refl/ +| /2 width=3 by csx_fwd_pair_sn/ +| /2 width=2 by csx_fwd_bind_dx/ +| /2 width=4 by csx_fwd_bind_dx_unit/ +| /2 width=3 by csx_fwd_flat_dx/ +| /4 width=7 by csx_inv_lifts, drops_refl, drops_drop/ ] qed-. -lemma csx_fqup_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+ ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 -/3 width=5 by csx_fqu_conf/ +lemma csx_fquq_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐⸮[b] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 * /2 width=6 by csx_fqu_conf/ +* #HG #HL #HT destruct // qed-. -lemma csx_fqus_conf: ∀h,o,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐* ⦃G2, L2, T2⦄ → - ⦃G1, L1⦄ ⊢ ⬈*[h, o] T1 → ⦃G2, L2⦄ ⊢ ⬈*[h, o] T2. -#h #o #G1 #G2 #L1 #L2 #T1 #T2 #H12 #H elim (fqus_inv_gen … H12) -H12 -[ /2 width=5 by csx_fqup_conf/ -| * #HG #HL #HT destruct // -] +lemma csx_fqup_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐+[b] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqup_ind … H) -G2 -L2 -T2 +/3 width=6 by csx_fqu_conf/ qed-. +lemma csx_fqus_conf: ∀h,o,b,G1,G2,L1,L2,T1,T2. ⦃G1, L1, T1⦄ ⊐*[b] ⦃G2, L2, T2⦄ → + ⦃G1, L1⦄ ⊢ ⬈*[h, o] 𝐒⦃T1⦄ → ⦃G2, L2⦄ ⊢ ⬈*[h, o] 𝐒⦃T2⦄. +#h #o #b #G1 #G2 #L1 #L2 #T1 #T2 #H @(fqus_ind … H) -H +/3 width=6 by csx_fquq_conf/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma index 79b41f785..21beea53b 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/lfpxs_lpxs.ma @@ -26,11 +26,11 @@ lemma lfpxs_lpxs: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h] L2 → ⦃G, L1⦄ ⊢ /2 width=1 by tc_lfxs_lex/ qed. lemma lfpxs_lpxs_lfeq: ∀h,G,L1,L. ⦃G, L1⦄ ⊢ ⬈*[h] L → - ∀L2,T. L ≡[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. + ∀L2,T. L ≐[T] L2 → ⦃G, L1⦄ ⊢ ⬈*[h, T] L2. /2 width=3 by tc_lfxs_lex_lfeq/ qed. (* Inversion lemmas with uncounted parallel rt-computation for local envs ***) lemma lfpxs_inv_lpxs_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈*[h, T] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≡[T] L2. + ∃∃L. ⦃G, L1⦄ ⊢ ⬈*[h] L & L ≐[T] L2. /3 width=5 by lfpx_fsge_comp, lpx_cpxs_trans, lfeq_cpx_trans, tc_lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt index a5cc2eae9..85df12939 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/partial.txt @@ -2,7 +2,7 @@ cpxs.ma cpxs_tdeq.ma cpxs_theq.ma cpxs_theq_vector.ma cpxs_drops.ma cpxs_fqus.ma cpxs_ext.ma lpxs.ma lpxs_length.ma lpxs_lpx.ma lpxs_cpxs.ma lfpxs.ma lfpxs_length.ma lfpxs_drops.ma lfpxs_fqup.ma lfpxs_lfdeq.ma lfpxs_aaa.ma lfpxs_cpxs.ma lfpxs_lpxs.ma lfpxs_lfpxs.ma -csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma +csx.ma csx_simple.ma csx_simple_theq.ma csx_drops.ma csx_fqus.ma csx_lsubr.ma csx_lfdeq.ma csx_aaa.ma csx_gcp.ma csx_gcr.ma csx_lfpx.ma csx_cnx.ma csx_cpxs.ma csx_lfpxs.ma csx_csx.ma csx_vector.ma csx_cnx_vector.ma csx_csx_vector.ma lfsx.ma lfsx_drops.ma lfsx_fqup.ma lfsx_lpx.ma lfsx_lpxs.ma lfsx_lfpxs.ma lfsx_csx.ma lfsx_lfsx.ma lsubsx.ma lsubsx_lfsx.ma lsubsx_lsubsx.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma index 034ce9c7e..a61602733 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_transition/lfpx_lpx.ma @@ -26,5 +26,5 @@ lemma lfpx_lpx: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h] L2 → ⦃G, L1⦄ ⊢ (* Inversion lemmas with uncounted parallel rt-transition for local envs ****) lemma lfpx_inv_lpx_lfeq: ∀h,G,L1,L2,T. ⦃G, L1⦄ ⊢ ⬈[h, T] L2 → - ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≡[T] L2. + ∃∃L. ⦃G, L1⦄ ⊢ ⬈[h] L & L ≐[T] L2. /3 width=3 by lfpx_fsge_comp, lfxs_inv_lex_lfeq/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma index 41b2c033e..5682e7218 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfdeq_lfeq.ma @@ -19,5 +19,5 @@ include "basic_2/static/lfdeq.ma". (* Properties with syntactic equivalence on referred entries ****************) -lemma lfeq_lfdeq: ∀h,o,L1,L2,T. L1 ≡[T] L2 → L1 ≛[h, o, T] L2. +lemma lfeq_lfdeq: ∀h,o,L1,L2,T. L1 ≐[T] L2 → L1 ≛[h, o, T] L2. /2 width=3 by lfxs_co/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma index 684e57370..c248d2acb 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/notation/relations/lazyeqsn_3.ma". +include "basic_2/notation/relations/doteqsn_3.ma". include "basic_2/static/lfxs.ma". (* SYNTACTIC EQUIVALENCE FOR LOCAL ENVIRONMENTS ON REFERRED ENTRIES *********) @@ -23,45 +23,45 @@ definition lfeq: relation3 term lenv lenv ≝ interpretation "syntactic equivalence on referred entries (local environment)" - 'LazyEqSn T L1 L2 = (lfeq T L1 L2). + 'DotEqSn T L1 L2 = (lfeq T L1 L2). (* Note: "lfeq_transitive R" is equivalent to "lfxs_transitive ceq R R" *) (* Basic_2A1: uses: lleq_transitive *) definition lfeq_transitive: predicate (relation3 lenv term term) ≝ - λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≡[T1] L2 → R L1 T1 T2. + λR. ∀L2,T1,T2. R L2 T1 T2 → ∀L1. L1 ≐[T1] L2 → R L1 T1 T2. (* Basic inversion lemmas ***************************************************) -lemma lfeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≡[ⓑ{p,I}V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1.ⓑ{I}V ≡[T] L2.ⓑ{I}V. +lemma lfeq_inv_bind: ∀p,I,L1,L2,V,T. L1 ≐[ⓑ{p,I}V.T] L2 → + ∧∧ L1 ≐[V] L2 & L1.ⓑ{I}V ≐[T] L2.ⓑ{I}V. /2 width=2 by lfxs_inv_bind/ qed-. -lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≡[ⓕ{I}V.T] L2 → - ∧∧ L1 ≡[V] L2 & L1 ≡[T] L2. +lemma lfeq_inv_flat: ∀I,L1,L2,V,T. L1 ≐[ⓕ{I}V.T] L2 → + ∧∧ L1 ≐[V] L2 & L1 ≐[T] L2. /2 width=2 by lfxs_inv_flat/ qed-. (* Advanced inversion lemmas ************************************************) -lemma lfeq_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ{I}V ≡[#0] L2 → - ∃∃K2. K1 ≡[V] K2 & L2 = K2.ⓑ{I}V. +lemma lfeq_inv_zero_pair_sn: ∀I,L2,K1,V. K1.ⓑ{I}V ≐[#0] L2 → + ∃∃K2. K1 ≐[V] K2 & L2 = K2.ⓑ{I}V. #I #L2 #K1 #V #H elim (lfxs_inv_zero_pair_sn … H) -H #K2 #X #HK12 #HX #H destruct /2 width=3 by ex2_intro/ qed-. -lemma lfeq_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≡[#0] K2.ⓑ{I}V → - ∃∃K1. K1 ≡[V] K2 & L1 = K1.ⓑ{I}V. +lemma lfeq_inv_zero_pair_dx: ∀I,L1,K2,V. L1 ≐[#0] K2.ⓑ{I}V → + ∃∃K1. K1 ≐[V] K2 & L1 = K1.ⓑ{I}V. #I #L1 #K2 #V #H elim (lfxs_inv_zero_pair_dx … H) -H #K1 #X #HK12 #HX #H destruct /2 width=3 by ex2_intro/ qed-. -lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≡[#⫯i] L2 → - ∃∃I2,K2. K1 ≡[#i] K2 & L2 = K2.ⓘ{I2}. +lemma lfeq_inv_lref_bind_sn: ∀I1,K1,L2,i. K1.ⓘ{I1} ≐[#⫯i] L2 → + ∃∃I2,K2. K1 ≐[#i] K2 & L2 = K2.ⓘ{I2}. /2 width=2 by lfxs_inv_lref_bind_sn/ qed-. -lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} → - ∃∃I1,K1. K1 ≡[#i] K2 & L1 = K1.ⓘ{I1}. +lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≐[#⫯i] K2.ⓘ{I2} → + ∃∃I1,K1. K1 ≐[#i] K2 & L1 = K1.ⓘ{I1}. /2 width=2 by lfxs_inv_lref_bind_dx/ qed-. (* Basic forward lemmas *****************************************************) @@ -69,7 +69,7 @@ lemma lfeq_inv_lref_bind_dx: ∀I2,K2,L1,i. L1 ≡[#⫯i] K2.ⓘ{I2} → (* Basic_2A1: was: llpx_sn_lrefl *) (* Note: this should have been lleq_fwd_llpx_sn *) lemma lfeq_fwd_lfxs: ∀R. c_reflexive … R → - ∀L1,L2,T. L1 ≡[T] L2 → L1 ⪤*[R, T] L2. + ∀L1,L2,T. L1 ≐[T] L2 → L1 ⪤*[R, T] L2. #R #HR #L1 #L2 #T * #f #Hf #HL12 /4 width=7 by lexs_co, cext2_co, ex2_intro/ qed-. @@ -77,7 +77,7 @@ qed-. (* Basic_properties *********************************************************) lemma frees_lfeq_conf: ∀f,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f → - ∀L2. L1 ≡[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. + ∀L2. L1 ≐[T] L2 → L2 ⊢ 𝐅*⦃T⦄ ≡ f. #f #L1 #T #H elim H -f -L1 -T [ /2 width=3 by frees_sort/ | #f #i #Hf #L2 #H2 diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma index 0f80c9772..bb67cd325 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfeq_fsle.ma @@ -29,5 +29,5 @@ qed. (* Forward lemmas with free variables inclusion for restricted closures *****) lemma lfeq_lfxs_trans: ∀R. lfeq_transitive R → - ∀L1,L,T. L1 ≡[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. + ∀L1,L,T. L1 ≐[T] L → ∀L2. L ⪤*[R, T] L2 → L1 ⪤*[R, T] L2. /4 width=16 by lfeq_fsle_comp, lfxs_trans_fsle, lfxs_trans_next/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma index 03772d98c..9e334565f 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_drops.ma @@ -22,7 +22,7 @@ include "basic_2/static/lfxs.ma". definition dedropable_sn: predicate (relation3 lenv term term) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → ∀K2,T. K1 ⪤*[R, T] K2 → ∀U. ⬆*[f] T ≡ U → - ∃∃L2. L1 ⪤*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≡[f] L2. + ∃∃L2. L1 ⪤*[R, U] L2 & ⬇*[b, f] L2 ≡ K2 & L1 ≐[f] L2. definition dropable_sn: predicate (relation3 lenv term term) ≝ λR. ∀b,f,L1,K1. ⬇*[b, f] L1 ≡ K1 → 𝐔⦃f⦄ → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma index 01f578f4e..2957ac1c3 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/lfxs_lex.ma @@ -31,7 +31,7 @@ qed. lemma lfxs_inv_lex_lfeq: ∀R. c_reflexive … R → lfxs_fsge_compatible R → ∀L1,L2,T. L1 ⪤*[R, T] L2 → - ∃∃L. L1 ⪤[R] L & L ≡[T] L2. + ∃∃L. L1 ⪤[R] L & L ≐[T] L2. #R #H1R #H2R #L1 #L2 #T * #f1 #Hf1 #HL elim (lexs_sdj_split … ceq_ext … HL 𝐈𝐝 ?) -HL [ #L0 #HL10 #HL02 |*: /2 width=1 by ext2_refl, sdj_isid_dx/ ] -H1R 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 64c160295..40e94b86f 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 @@ -110,7 +110,7 @@ table { [ [ "refinement for lenvs" ] "lsubsx" + "( ? ⊢ ? ⊆ⓧ[?,?,?] ? )" "lsubsx_lfsx" + "lsubsx_lsubsx" * ] [ [ "strongly normalizing for lenvs on referred entries" ] "lfsx" + "( ? ⊢ ⬈*[?,?,?] 𝐒⦃?⦄ )" "lfsx_drops" + "lfsx_fqup" + "lfsx_cpx" + "lfsx_cpxs" + "lfsx_lfpxs" + "lfsx_lfsx" * ] [ [ "strongly normalizing for term vectors" ] "csx_vector" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_cnx_vector" + "csx_csx_vector" * ] - [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] + [ [ "strongly normalizing for terms" ] "csx" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] 𝐒⦃?⦄ )" "csx_simple" + "csx_simple_theq" + "csx_drops" + "csx_fqus" + "csx_lsubr" + "csx_lfdeq" + "csx_aaa" + "csx_gcp" + "csx_gcr" + "csx_lfpx" + "csx_cnx" + "csx_cpxs" + "csx_lfpxs" + "csx_csx" * ] [ [ "for lenvs on referred entries" ] "lfpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?,?] ? )" "lfpxs_length" + "lfpxs_drops" + "lfpxs_fqup" + "lfpxs_lfdeq" + "lfpxs_aaa" + "lfpxs_cpxs" + "lfpxs_lpxs" + "lfpxs_lfpxs" * ] [ [ "for lenvs on all entries" ] "lpxs" + "( ⦃?,?⦄ ⊢ ⬈*[?] ? )" "lpxs_length" + "lpxs_lpx" + "lpxs_cpxs" * ] [ [ "for binders" ] "cpxs_ext" + "( ⦃?,?⦄ ⊢ ? ⬈*[?] ? )" * ] -- 2.39.2