From 291fe1d3b56faf91d07099f43f3ebde2988649e1 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 25 Dec 2021 16:40:06 +0100 Subject: [PATCH] update in ground, basic_2A and apps_2 + notation for lists: fixed and updated --- .../contribs/lambdadelta/apps_2/functional/mf.ma | 10 +++++----- .../lambdadelta/apps_2/functional/mf_cpr.ma | 2 +- .../lambdadelta/apps_2/functional/mf_exteq.ma | 4 ++-- .../lambdadelta/apps_2/functional/mf_lifts.ma | 2 +- .../contribs/lambdadelta/apps_2/models/tm.ma | 2 +- .../lambdadelta/apps_2/models/tm_props.ma | 4 ++-- .../{blackcircle_3.ma => black_square_3.ma} | 4 ++-- .../lambdadelta/apps_2/web/apps_2_src.tbl | 2 +- .../lambdadelta/basic_2A/computation/gcp_aaa.ma | 4 ++-- .../lambdadelta/basic_2A/grammar/lenv_append.ma | 14 +++++++------- .../lambdadelta/basic_2A/multiple/drops.ma | 6 +++--- .../lambdadelta/basic_2A/multiple/drops_drops.ma | 2 +- .../basic_2A/multiple/frees_append.ma | 6 +++--- .../lambdadelta/basic_2A/multiple/lifts.ma | 6 +++--- .../lambdadelta/basic_2A/multiple/lifts_lifts.ma | 2 +- .../basic_2A/substitution/drop_append.ma | 10 +++++----- .../lambdadelta/basic_2A/unfold/unfold.ma | 2 +- .../{double_semicolon_2.ma => black_circle_2.ma} | 6 +++--- ...semicolon_3.ma => black_halfcircleright_3.ma} | 6 +++--- .../notation/functions/circled_element_e_1.ma | 2 +- .../ground/notation/functions/oplus_3.ma | 8 ++++---- .../ground/notation/functions/oplusleft_3.ma | 8 ++++---- .../lambdadelta/ground/relocation/fr2_append.ma | 12 ++++++------ .../lambdadelta/ground/relocation/fr2_map.ma | 4 ++-- .../lambdadelta/ground/relocation/fr2_minus.ma | 16 ++++++++-------- .../lambdadelta/ground/relocation/fr2_nat.ma | 12 ++++++------ .../lambdadelta/ground/relocation/fr2_plus.ma | 8 ++++---- .../lambdadelta/ground/web/ground_src.tbl | 4 ++-- 28 files changed, 84 insertions(+), 84 deletions(-) rename matita/matita/contribs/lambdadelta/apps_2/notation/functional/{blackcircle_3.ma => black_square_3.ma} (91%) rename matita/matita/contribs/lambdadelta/ground/notation/functions/{double_semicolon_2.ma => black_circle_2.ma} (90%) rename matita/matita/contribs/lambdadelta/ground/notation/functions/{semicolon_3.ma => black_halfcircleright_3.ma} (86%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma index 4e88c1a78..3d5d22b64 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf.ma @@ -35,19 +35,19 @@ interpretation "term filling (multiple filling)" (* Basic Properties *********************************************************) -lemma mf_sort: ∀gv,lv,s. ●[gv,lv]⋆s = ⋆s. +lemma mf_sort: ∀gv,lv,s. ■[gv,lv]⋆s = ⋆s. // qed. -lemma mf_lref: ∀gv,lv,i. ●[gv,lv]#i = lv i. +lemma mf_lref: ∀gv,lv,i. ■[gv,lv]#i = lv i. // qed. -lemma mf_gref: ∀gv,lv,l. ●[gv,lv]§l = gv l. +lemma mf_gref: ∀gv,lv,l. ■[gv,lv]§l = gv l. // qed. lemma mf_bind (p) (I): ∀gv,lv,V,T. - ●[gv,lv]ⓑ[p,I]V.T = ⓑ[p,I]●[gv,lv]V.●[⇡[0]gv,⇡[0←#0]lv]T. + ■[gv,lv]ⓑ[p,I]V.T = ⓑ[p,I]■[gv,lv]V.■[⇡[0]gv,⇡[0←#0]lv]T. // qed. lemma mf_flat (I): ∀gv,lv,V,T. - ●[gv,lv]ⓕ[I]V.T = ⓕ[I]●[gv,lv]V.●[gv,lv]T. + ■[gv,lv]ⓕ[I]V.T = ⓕ[I]■[gv,lv]V.■[gv,lv]T. // qed. diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma index 70b98821c..26d43e20a 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_cpr.ma @@ -22,7 +22,7 @@ include "apps_2/functional/mf_exteq.ma". lemma mf_delta_drops (h) (G): ∀K,V1,V2. ❨G,K❩ ⊢ V1 ➡[h,0] V2 → ∀T,L,i. ⇩[i] L ≘ K.ⓓV1 → - ∀gv,lv. ❨G,L❩ ⊢ ●[gv,⇡[i←#i]lv]T ➡[h,0] ●[gv,⇡[i←↑[↑i]V2]lv]T. + ∀gv,lv. ❨G,L❩ ⊢ ■[gv,⇡[i←#i]lv]T ➡[h,0] ■[gv,⇡[i←↑[↑i]V2]lv]T. #h #G #K #V1 #V2 #HV #T elim T -T * // [ #i #L #j #HKL #gv #lv >mf_lref >mf_lref diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma index 0f6975a73..ab162c630 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/mf_exteq.ma @@ -20,7 +20,7 @@ include "apps_2/functional/mf.ma". (* Properties with extensional equivalence **********************************) -lemma mf_comp (T): compatible_3 … (λgv,lv.●[gv,lv]T) (exteq …) (exteq …) (eq …). +lemma mf_comp (T): compatible_3 … (λgv,lv.■[gv,lv]T) (exteq …) (exteq …) (eq …). #T elim T -T * [ // | #i #gv1 #gv2 #Hgv #lv1 #lv2 #Hlv @@ -36,7 +36,7 @@ qed-. (* Advanced properties ******************************************************) -lemma mf_id (T): ●[mf_gi,mf_li]T = T. +lemma mf_id (T): ■[mf_gi,mf_li]T = T. #T elim T -T * // [ #p #I #V #T #IHV #IHT mf_bind >mf_bind >flifts_basic_bind diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma index 96a98fc75..f56ff538b 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm.ma @@ -28,7 +28,7 @@ definition tm_co (p) (V) (T) ≝ ⓓ[p]V.(↑[1]T). definition tm_ap (V) (T) ≝ ⓐV.T. -definition tm_ti (gv) (lv) (T) ≝ ●[gv,lv]T. +definition tm_ti (gv) (lv) (T) ≝ ■[gv,lv]T. definition TM (h): model ≝ mk_model … . [ @tm_dd diff --git a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma index 1777a2d00..640de8c4f 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma @@ -24,7 +24,7 @@ include "apps_2/models/tm_vpush.ma". lemma cpcs_repl (h) (G) (L): replace_2 … (cpcs h G L) (cpcs h G L) (cpcs h G L). /3 width=5 by cpcs_trans, cpcs_sym/ qed-. (* -lemma pippo (h) (gv) (lv) (T): ●[gv,lv]T = ⟦T⟧{TM h}[gv,lv]. +lemma pippo (h) (gv) (lv) (T): ■[gv,lv]T = ⟦T⟧{TM h}[gv,lv]. // qed. lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T): @@ -38,7 +38,7 @@ lemma tm_mi (h) (gv1) (gv2) (lv1) (lv2) (p) (W) (T): (mf_comp … T) in ⊢ (????%?); -[2: ;;tm_vpush_vlift_join_O +[2: @tm_vpush_vlift_join_O "hvbox( ⓔ )" non associative with precedence 75 for @{ 'CircledElementE ? }. -notation > "hvbox( ⓔ{ term 46 C } )" +notation > "hvbox( ⓔ{ term 46 S } )" non associative with precedence 75 for @{ 'CircledElementE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma index d1860243f..db030f3b6 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplus_3.ma @@ -15,13 +15,13 @@ (* GROUND NOTATION **********************************************************) notation < "hvbox( hd ⨁ break tl )" - right associative with precedence 55 + right associative with precedence 47 for @{ 'OPlus $S $hd $tl }. notation > "hvbox( hd ⨁ break tl )" - right associative with precedence 55 + right associative with precedence 47 for @{ 'OPlus ? $hd $tl }. -notation > "hvbox( hd ⨁{ break term 46 S } break term 54 tl )" - non associative with precedence 55 +notation > "hvbox( hd ⨁{ break term 46 S } break term 46 tl )" + non associative with precedence 47 for @{ 'OPlus $S $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma index 2e4bbf673..6d71ba242 100644 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/oplusleft_3.ma @@ -15,13 +15,13 @@ (* GROUND NOTATION **********************************************************) notation < "hvbox( hd ⨭ break tl )" - left associative with precedence 50 + left associative with precedence 47 for @{ 'OPlusLeft $S $hd $tl }. notation > "hvbox( hd ⨭ break tl )" - left associative with precedence 50 + left associative with precedence 47 for @{ 'OPlusLeft ? $hd $tl }. -notation > "hvbox( hd ⨭{ break term 46 S } break term 50 tl )" - non associative with precedence 50 +notation > "hvbox( hd ⨭{ break term 46 S } break term 47 tl )" + non associative with precedence 47 for @{ 'OPlusLeft $S $hd $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma index b50a5cfa8..911c011b4 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma @@ -12,30 +12,30 @@ (* *) (**************************************************************************) -include "ground/notation/functions/double_semicolon_2.ma". +include "ground/notation/functions/black_circle_2.ma". include "ground/relocation/fr2_map.ma". (* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************) -(* Note: this is compose *) +(* Note: this is reverse compose *) (*** fr2_append *) rec definition fr2_append f1 f2 on f1 ≝ match f1 with [ fr2_empty ⇒ f2 -| fr2_lcons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2 +| fr2_lcons d h f1 ⇒ ❨d, h❩◗ fr2_append f1 f2 ]. interpretation "append (finite relocation maps with pairs)" - 'DoubleSemicolon f1 f2 = (fr2_append f1 f2). + 'BlackCircle f1 f2 = (fr2_append f1 f2). (* Basic constructions ******************************************************) (*** mr2_append_nil *) lemma fr2_append_empty (f2): - f2 = 𝐞 ;; f2. + f2 = 𝐞 ● f2. // qed. (*** mr2_append_cons *) lemma fr2_append_lcons (d) (h) (f1) (f2): - ❨d, h❩; (f1 ;; f2) = (❨d, h❩; f1) ;; f2. + ❨d, h❩◗ (f1 ● f2) = (❨d, h❩◗ f1) ● f2. // qed. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma index a1f2f4d4e..77a1c518a 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma @@ -13,7 +13,7 @@ (**************************************************************************) include "ground/notation/functions/element_e_0.ma". -include "ground/notation/functions/semicolon_3.ma". +include "ground/notation/functions/black_halfcircleright_3.ma". include "ground/arith/nat.ma". (* FINITE RELOCATION MAPS WITH PAIRS ****************************************) @@ -32,4 +32,4 @@ interpretation interpretation "left cons (finite relocation maps with pairs)" - 'Semicolon d h f = (fr2_lcons d h f). + 'BlackHalfCircleRight d h f = (fr2_lcons d h f). diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma index d083a5df8..1e54b3846 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma @@ -28,10 +28,10 @@ inductive fr2_minus: nat → relation fr2_map ≝ fr2_minus i (𝐞) (𝐞) (*** minuss_lt *) | fr2_minus_lt (f1) (f2) (d) (h) (i): - i < d → fr2_minus i f1 f2 → fr2_minus i (❨d,h❩;f1) (❨d-i,h❩;f2) + i < d → fr2_minus i f1 f2 → fr2_minus i (❨d,h❩◗f1) (❨d-i,h❩◗f2) (*** minuss_ge *) | fr2_minus_ge (f1) (f2) (d) (h) (i): - d ≤ i → fr2_minus (h+i) f1 f2 → fr2_minus i (❨d,h❩;f1) f2 + d ≤ i → fr2_minus (h+i) f1 f2 → fr2_minus i (❨d,h❩◗f1) f2 . interpretation @@ -53,10 +53,10 @@ qed-. (*** minuss_inv_cons1 *) lemma fr2_minus_inv_lcons_sn (f1) (f2) (d) (h) (i): - ❨d, h❩;f1 ▭ i ≘ f2 → + ❨d, h❩◗f1 ▭ i ≘ f2 → ∨∨ ∧∧ d ≤ i & f1 ▭ h+i ≘ f2 - | ∃∃f. i < d & f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f. -#g1 #f2 #d #h #i @(insert_eq_1 … (❨d,h❩;g1)) + | ∃∃f. i < d & f1 ▭ i ≘ f & f2 = ❨d-i,h❩◗f. +#g1 #f2 #d #h #i @(insert_eq_1 … (❨d,h❩◗g1)) #f1 * -f1 -f2 -i [ #i #H destruct | #f1 #f #d1 #h1 #i1 #Hid1 #Hf #H destruct /3 width=3 by ex3_intro, or_intror/ @@ -66,7 +66,7 @@ qed-. (*** minuss_inv_cons1_ge *) lemma fr2_minus_inv_lcons_sn_ge (f1) (f2) (d) (h) (i): - ❨d, h❩;f1 ▭ i ≘ f2 → d ≤ i → f1 ▭ h+i ≘ f2. + ❨d, h❩◗f1 ▭ i ≘ f2 → d ≤ i → f1 ▭ h+i ≘ f2. #f1 #f2 #d #h #i #H elim (fr2_minus_inv_lcons_sn … H) -H * // #f #Hid #_ #_ #Hdi elim (nlt_ge_false … Hid Hdi) @@ -74,8 +74,8 @@ qed-. (*** minuss_inv_cons1_lt *) lemma fr2_minus_inv_lcons_sn_lt (f1) (f2) (d) (h) (i): - ❨d, h❩;f1 ▭ i ≘ f2 → i < d → - ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f. + ❨d, h❩◗f1 ▭ i ≘ f2 → i < d → + ∃∃f. f1 ▭ i ≘ f & f2 = ❨d-i,h❩◗f. #f1 #f2 #d #h #i #H elim (fr2_minus_inv_lcons_sn … H) -H * [ #Hdi #_ #Hid elim (nlt_ge_false … Hid Hdi) | /2 width=3 by ex2_intro/ diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma index 6b3d84f8a..453315c77 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma @@ -26,10 +26,10 @@ inductive fr2_nat: fr2_map → relation nat ≝ fr2_nat (𝐞) l l (*** at_lt *) | fr2_nat_lt (f) (d) (h) (l1) (l2): - l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩;f) l1 l2 + l1 < d → fr2_nat f l1 l2 → fr2_nat (❨d,h❩◗f) l1 l2 (*** at_ge *) | fr2_nat_ge (f) (d) (h) (l1) (l2): - d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩;f) l1 l2 + d ≤ l1 → fr2_nat f (l1 + h) l2 → fr2_nat (❨d,h❩◗f) l1 l2 . interpretation @@ -51,10 +51,10 @@ qed-. (*** at_inv_cons *) lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2): - @❨l1, ❨d,h❩;f❩ ≘ l2 → + @❨l1, ❨d,h❩◗f❩ ≘ l2 → ∨∨ ∧∧ l1 < d & @❨l1, f❩ ≘ l2 | ∧∧ d ≤ l1 & @❨l1+h, f❩ ≘ l2. -#g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩;g)) +#g #d #h #l1 #l2 @(insert_eq_1 … (❨d, h❩◗g)) #f * -f -l1 -l2 [ #l #H destruct | #f1 #d1 #h1 #l1 #l2 #Hld1 #Hl12 #H destruct /3 width=1 by or_introl, conj/ @@ -64,7 +64,7 @@ qed-. (*** at_inv_cons *) lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2): - @❨l1, ❨d,h❩;f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2. + @❨l1, ❨d,h❩◗f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2. #f #d #h #l1 #h2 #H elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d elim (nlt_ge_false … Hl1d Hdl1) @@ -72,7 +72,7 @@ qed-. (*** at_inv_cons *) lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2): - @❨l1, ❨d,h❩;f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2. + @❨l1, ❨d,h❩◗f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2. #f #d #h #l1 #h2 #H elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1 elim (nlt_ge_false … Hl1d Hdl1) diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma index cc36d81b2..a5010b833 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma @@ -21,7 +21,7 @@ include "ground/relocation/fr2_map.ma". (*** pluss *) rec definition fr2_plus (f:fr2_map) (n:nat) on f ≝ match f with [ fr2_empty ⇒ 𝐞 -| fr2_lcons d h f ⇒ ❨d+n,h❩;fr2_plus f n +| fr2_lcons d h f ⇒ ❨d+n,h❩◗fr2_plus f n ]. interpretation @@ -32,7 +32,7 @@ interpretation (*** pluss_SO2 *) lemma fr2_plus_lcons_unit (d) (h) (f): - ((❨d,h❩;f)+𝟏) = ❨↑d,h❩;f+𝟏. + ((❨d,h❩◗f)+𝟏) = ❨↑d,h❩◗f+𝟏. normalize // qed. (* Basic inversions *********************************************************) @@ -46,8 +46,8 @@ qed. (*** pluss_inv_cons2 *) lemma fr2_plus_inv_lcons_dx (n) (d) (h) (f2) (f): - f + n = ❨d,h❩;f2 → - ∃∃f1. f1+n = f2 & f = ❨d-n,h❩;f1. + f + n = ❨d,h❩◗f2 → + ∃∃f1. f1+n = f2 & f = ❨d-n,h❩◗f1. #n #d #h #f2 * [ normalize #H destruct | #d1 #h1 #f1 whd in ⊢ (??%?→?); #H destruct diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index 6a4e3dcf9..2b655f20c 100644 --- a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl +++ b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl @@ -24,9 +24,9 @@ table { [ { "finite relocation with pairs" * } { [ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ] [ "fr2_minus ( ? ▭ ? ≘ ? )" * ] - [ "fr2_append ( ?;;? )" * ] + [ "fr2_append ( ?●? )" * ] [ "fr2_plus ( ?+? )" * ] - [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ] + [ "fr2_map ( 𝐞 ) ( ❨?,?❩◗? )" * ] } ] [ { "total relocation" * } { -- 2.39.2