From 54c4e854515cbcb1376881e9aedad006bf6545f2 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 25 Apr 2018 13:25:19 +0200 Subject: [PATCH] update in ground_2 and basic_2 + old and unused definition llstar replaced with new definition ltc to appear in cpms --- .../basic_2/etc/drops/drops_lstar.etc | 22 ++++++ .../{drops_lstar.ma => drops_ctc.ma} | 30 +------ .../basic_2/rt_computation/cpxs_drops.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 2 +- .../ground_2/lib/{lstar.ma => functions.ma} | 9 ++- .../{xoa/xoa_props.ma => lib/logic.ma} | 2 +- .../contribs/lambdadelta/ground_2/lib/ltc.ma | 78 +++++++++++++++++++ .../lambdadelta/ground_2/lib/relations.ma | 5 +- .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +- 9 files changed, 118 insertions(+), 36 deletions(-) create mode 100644 matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc rename matita/matita/contribs/lambdadelta/basic_2/relocation/{drops_lstar.ma => drops_ctc.ma} (70%) rename matita/matita/contribs/lambdadelta/ground_2/lib/{lstar.ma => functions.ma} (79%) rename matita/matita/contribs/lambdadelta/ground_2/{xoa/xoa_props.ma => lib/logic.ma} (98%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma diff --git a/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc new file mode 100644 index 000000000..47da596ad --- /dev/null +++ b/matita/matita/contribs/lambdadelta/basic_2/etc/drops/drops_lstar.etc @@ -0,0 +1,22 @@ +include "ground_2/lib/lstar.ma". + +(* Basic_2A1: was: d_liftable_llstar *) +lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d). +#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2 +[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/ +| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1 + elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1 + elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/ +] +qed-. + +(* Basic_2A1: was: d_deliftable_sn_llstar *) +lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R → + ∀d. d_deliftable2_sn C S (llstar … R d). +#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2 +[ /2 width=3 by lstar_O, ex2_intro/ +| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1 + elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 + elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/ +] +qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma similarity index 70% rename from matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma rename to matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma index dadccae4f..cc485711c 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_lstar.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/drops_ctc.ma @@ -13,12 +13,11 @@ (**************************************************************************) include "ground_2/lib/star.ma". -include "ground_2/lib/lstar.ma". include "basic_2/relocation/lreq_lreq.ma". (* GENERIC SLICING FOR LOCAL ENVIRONMENTS ***********************************) -(* Properties with reflexive and transitive closure *************************) +(* Properties with contextual transitive closure ****************************) (* Basic_2A1: was: d_liftable_LTC *) lemma d2_liftable_sn_CTC: ∀C,S,R. d_liftable2_sn C S R → d_liftable2_sn C S (CTC … R). @@ -42,7 +41,7 @@ lemma d2_deliftable_sn_CTC: ∀C,S,R. d_deliftable2_sn C S R → d_deliftable2_s ] qed-. -lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R). +lemma co_dropable_sn_CTC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R). #R #HR #b #f #L1 #K1 #HLK1 #Hf #f2 #L2 #H elim H -L2 [ #L2 #HL12 #f1 #H elim (HR … HLK1 … Hf … HL12 … H) -HR -Hf -f2 -L1 /3 width=3 by inj, ex2_intro/ @@ -52,28 +51,7 @@ lemma co_dropable_sn_TC: ∀R. co_dropable_sn R → co_dropable_sn (CTC … R). ] qed-. -(* Basic_2A1: was: d_liftable_llstar *) -lemma d2_liftable_sn_llstar: ∀C,S,R. d_liftable2_sn C S R → ∀d. d_liftable2_sn C S (llstar … R d). -#C #S #R #HR #d #K #T1 #T2 #H @(lstar_ind_r … d T2 H) -d -T2 -[ #b #f #L #_ #U1 #HTU1 -HR -b -K /2 width=3 by ex2_intro/ -| #l #T #T2 #_ #HT2 #IHT1 #b #f #L #HLK #U1 #HTU1 - elim (IHT1 … HLK … HTU1) -T1 #U #HTU #HU1 - elim (HR … HT2 … HLK … HTU) -T /3 width=5 by lstar_dx, ex2_intro/ -] -qed-. - -(* Basic_2A1: was: d_deliftable_sn_llstar *) -lemma d2_deliftable_sn_llstar: ∀C,S,R. d_deliftable2_sn C S R → - ∀d. d_deliftable2_sn C S (llstar … R d). -#C #S #R #HR #l #L #U1 #U2 #H @(lstar_ind_r … l U2 H) -l -U2 -[ /2 width=3 by lstar_O, ex2_intro/ -| #l #U #U2 #_ #HU2 #IHU1 #b #f #K #HLK #T1 #HTU1 - elim (IHU1 … HLK … HTU1) -IHU1 -U1 #T #HTU #HT1 - elim (HR … HU2 … HLK … HTU) -HR -L -U /3 width=5 by lstar_dx, ex2_intro/ -] -qed-. - -lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R). +lemma co_dropable_dx_CTC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R). #R #HR #f2 #L1 #L2 #H elim H -L2 [ #L2 #HL12 #b #f #K2 #HLK2 #Hf #f1 #Hf2 elim (HR … HL12 … HLK2 … Hf … Hf2) -HR -Hf -f2 -L2 /3 width=3 by inj, ex2_intro/ @@ -83,7 +61,7 @@ lemma co_dropable_dx_TC: ∀R. co_dropable_dx R → co_dropable_dx (CTC … R). ] qed-. -lemma co_dedropable_sn_TC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R). +lemma co_dedropable_sn_CTC: ∀R. co_dedropable_sn R → co_dedropable_sn (CTC … R). #R #HR #b #f #L1 #K1 #HLK1 #f1 #K2 #H elim H -K2 [ #K2 #HK12 #f2 #Hf elim (HR … HLK1 … HK12 … Hf) -HR -f1 -K1 /3 width=4 by inj, ex3_intro/ diff --git a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma index 87ff4a980..04a376981 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/rt_computation/cpxs_drops.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "basic_2/relocation/drops_lstar.ma". +include "basic_2/relocation/drops_ctc.ma". include "basic_2/rt_transition/cpx_drops.ma". include "basic_2/rt_computation/cpxs.ma". 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 11112816b..f6b46722c 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 @@ -201,7 +201,7 @@ table { class "orange" [ { "relocation" * } { [ { "generic slicing" * } { - [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_lstar" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] + [ [ "for lenvs" ] "drops" + "( ⬇*[?,?] ? ≘ ? )" + "( ⬇*[?] ? ≘ ? )" "drops_ctc" + "drops_weight" + "drops_length" + "drops_cext2" + "drops_lexs" + "drops_lreq" + "drops_drops" + "drops_vector" * ] } ] [ { "generic relocation" * } { diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma similarity index 79% rename from matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma index ae707f2b9..64fbae2e1 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/lstar.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/functions.ma @@ -12,9 +12,10 @@ (* *) (**************************************************************************) -include "arithmetics/lstar.ma". +include "ground_2/lib/relations.ma". -(* PROPERTIES OF NAT-LABELED REFLEXIVE AND TRANSITIVE CLOSURE ***************) +(* FUNCTIONS ****************************************************************) -definition llstar: ∀A:Type[0]. ∀B. (A→relation B) → nat → (A→relation B) ≝ - λA,B,R,l,a. lstar … (R a) l. +definition left_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f i a. + +definition right_identity (A:Type[0]) (f): predicate A ≝ λi. ∀a:A. a = f a i. diff --git a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma similarity index 98% rename from matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma rename to matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma index 530c0e2b3..852e4e9ce 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/xoa/xoa_props.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/logic.ma @@ -23,7 +23,7 @@ interpretation "logical false" 'false = False. interpretation "logical true" 'true = True. -(* Logical properties missing in the basic library **************************) +(* Logical properties missing in the basic library **************************) lemma commutative_and: ∀A,B. A ∧ B → B ∧ A. #A #B * /2 width=1 by conj/ diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma new file mode 100644 index 000000000..27ef34de4 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/ltc.ma @@ -0,0 +1,78 @@ +(**************************************************************************) +(* ___ *) +(* ||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 "ground_2/lib/functions.ma". + +(* LABELLED TRANSITIVE CLOSURE **********************************************) + +inductive ltc (A:Type[0]) (f) (B) (R:relation3 A B B): relation3 A B B ≝ +| ltc_rc : ∀a,b1,b2. R a b1 b2 → ltc … a b1 b2 +| ltc_trans: ∀a1,a2,b1,b,b2. ltc … a1 b1 b → ltc … a2 b b2 → ltc … (f a1 a2) b1 b2 +. + +(* Basic properties *********************************************************) + +lemma ltc_sn (A) (f) (B) (R): ∀a1,b1,b. R a1 b1 b → + ∀a2,b2. ltc A f B R a2 b b2 → ltc … f … R (f a1 a2) b1 b2. +/3 width=3 by ltc_rc, ltc_trans/ qed. + +lemma ltc_dx (A) (f) (B) (R): ∀a1,b1,b. ltc A f B R a1 b1 b → + ∀a2,b2. R a2 b b2 → ltc … f … R (f a1 a2) b1 b2. +/3 width=3 by ltc_rc, ltc_trans/ qed. + +(* Basic eliminators ********************************************************) + +lemma ltc_ind_sn (A) (f) (B) (R) (Q:relation2 A B) (b2): associative … f → + (∀a,b1. R a b1 b2 → Q a b1) → + (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) → + ∀a,b1. ltc … f … R a b1 b2 → Q a b1. +#A #f #B #R #Q #b2 #Hf #IH1 #IH2 #a #b1 @(insert_eq … b2) +#b0 #H elim H -a -b1 -b0 /2 width=2 by/ +#a1 #a2 #b1 #b #b0 #H #Hb2 #_ +generalize in match Hb2; generalize in match a2; -Hb2 -a2 +elim H -a1 -b1 -b /4 width=4 by ltc_trans/ +qed-. + +lemma ltc_ind_dx (A) (f) (B) (R) (Q:A→predicate B) (b1): associative … f → + (∀a,b2. R a b1 b2 → Q a b2) → + (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) → + ∀a,b2. ltc … f … R a b1 b2 → Q a b2. +#A #f #B #R #Q #b1 #Hf #IH1 #IH2 #a #b2 @(insert_eq … b1) +#b0 #H elim H -a -b0 -b2 /2 width=2 by/ +#a1 #a2 #b0 #b #b2 #Hb0 #H #IHb0 #_ +generalize in match IHb0; generalize in match Hb0; generalize in match a1; -IHb0 -Hb0 -a1 +elim H -a2 -b -b2 /4 width=4 by ltc_trans/ +qed-. + +(* Advanced elimiators with reflexivity *************************************) + +lemma ltc_ind_sn_refl (A) (i) (f) (B) (R) (Q:relation2 A B) (b2): + associative … f → right_identity … f i → reflexive B (R i) → + Q i b2 → + (∀a1,a2,b1,b. R a1 b1 b → ltc … f … R a2 b b2 → Q a2 b → Q (f a1 a2) b1) → + ∀a,b1. ltc … f … R a b1 b2 → Q a b1. +#A #i #f #B #R #Q #b2 #H1f #H2f #HR #IH1 #IH2 #a #b1 #H +@(ltc_ind_sn … R … H1f … IH2 … H) -a -b1 -H1f #a #b1 #Hb12 +>(H2f a) -H2f /3 width=4 by ltc_rc/ +qed-. + +lemma ltc_ind_dx_refl (A) (i) (f) (B) (R) (Q:A→predicate B) (b1): + associative … f → left_identity … f i → reflexive B (R i) → + Q i b1 → + (∀a1,a2,b,b2. ltc … f … R a1 b1 b → Q a1 b → R a2 b b2 → Q (f a1 a2) b2) → + ∀a,b2. ltc … f … R a b1 b2 → Q a b2. +#A #i #f #B #R #Q #b1 #H1f #H2f #HR #IH1 #IH2 #a #b2 #H +@(ltc_ind_dx … R … H1f … IH2 … H) -a -b2 -H1f #a #b2 #Hb12 +>(H2f a) -H2f /3 width=4 by ltc_rc/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma index 86be38640..af10dbb89 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/relations.ma @@ -13,10 +13,13 @@ (**************************************************************************) include "basics/relations.ma". -include "ground_2/xoa/xoa_props.ma". +include "ground_2/lib/logic.ma". (* GENERIC RELATIONS ********************************************************) +lemma insert_eq: ∀A,a. ∀Q1,Q2:predicate A. (∀a0. Q1 a0 → a = a0 → Q2 a0) → Q1 a → Q2 a. +/2 width=1 by/ qed-. + (* Inclusion ****************************************************************) definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝ diff --git a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl index 090a67164..a7da5c2d0 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground_2/web/ground_2_src.tbl @@ -55,7 +55,7 @@ table { [ "stream ( ? @ ? )" "stream_eq ( ? ≗ ? )" "stream_hdtl ( ⫰? )" "stream_tls ( ⫰*[?]? )" * ] [ "list ( ◊ ) ( ? @ ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} @ ? ) ( ? @@ ? ) ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] - [ "relations ( ? ⊆ ? )" "star" "lstar" * ] + [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "star" "ltc" * ] } ] } @@ -63,7 +63,7 @@ table { class "orange" [ { "generated logical decomposables" * } { [ { "" * } { - [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" "xoa_props ( ⊥ ) ( ⊤ )" * ] + [ "xoa ( ∃∃ ) ( ∨∨ ) ( ∧∧ )" * ] } ] } -- 2.39.2