From 3c8da07d7a5d7cf0432a83732a6d103f527afaef Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 5 May 2018 01:20:47 +0200 Subject: [PATCH] update in ground_2 and basic_2 + updated notation for lists + updated structure for global environments --- .../lambdadelta/apps_2/functional/rtm.ma | 6 ++--- .../lambdadelta/apps_2/functional/rtm_step.ma | 4 +-- .../contribs/lambdadelta/basic_2/names.txt | 1 + .../basic_2/relocation/lifts_vector.ma | 10 +++---- .../lambdadelta/basic_2/static/gcp_aaa.ma | 12 ++++----- .../lambdadelta/basic_2/static/gcp_cr.ma | 8 +++--- .../lambdadelta/basic_2/syntax/genv.ma | 25 ++++++++++++----- .../syntax/genv_length.ma} | 25 +++++------------ .../lambdadelta/basic_2/syntax/term_vector.ma | 2 +- .../lambdadelta/basic_2/web/basic_2_src.tbl | 1 + .../contribs/lambdadelta/ground_2/lib/list.ma | 8 +++--- .../notation/constructors/circledE_1.ma | 27 +++++++++++++++++++ .../constructors/{nil_0.ma => diamond_0.ma} | 4 +-- .../{oplusright_5.ma => semicolon_3.ma} | 14 ++-------- .../lambdadelta/ground_2/relocation/mr2.ma | 14 ++++++++-- .../lambdadelta/ground_2/relocation/mr2_at.ma | 12 ++++----- .../ground_2/relocation/mr2_minus.ma | 18 ++++++------- .../ground_2/relocation/mr2_plus.ma | 8 +++--- .../lambdadelta/ground_2/web/ground_2_src.tbl | 4 +-- matita/matita/contribs/lambdadelta/replace.sh | 2 +- 20 files changed, 117 insertions(+), 88 deletions(-) rename matita/matita/contribs/lambdadelta/{ground_2/lib/list2.ma => basic_2/syntax/genv_length.ma} (60%) create mode 100644 matita/matita/contribs/lambdadelta/ground_2/notation/constructors/circledE_1.ma rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{nil_0.ma => diamond_0.ma} (94%) rename matita/matita/contribs/lambdadelta/ground_2/notation/constructors/{oplusright_5.ma => semicolon_3.ma} (68%) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma index 66b481290..e8ac12370 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm.ma @@ -44,18 +44,18 @@ record rtm: Type[0] ≝ (* initial state *) definition rtm_i: genv → term → rtm ≝ - λG,T. mk_rtm G 0 (⋆) (◊) T. + λG,T. mk_rtm G 0 (⋆) (Ⓔ) T. (* update code *) definition rtm_t: rtm → term → rtm ≝ λM,T. match M with - [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (◊) T + [ mk_rtm G u E _ _ ⇒ mk_rtm G u E (Ⓔ) T ]. (* update closure *) definition rtm_u: rtm → xenv → term → rtm ≝ λM,E,T. match M with - [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (◊) T + [ mk_rtm G u _ _ _ ⇒ mk_rtm G u E (Ⓔ) T ]. (* get global environment *) diff --git a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma index 8f5a61ee8..1b456b521 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/functional/rtm_step.ma @@ -46,8 +46,8 @@ inductive rtm_step: relation rtm ≝ rtm_step (mk_rtm G u E ({D, V} @ S) (+ⓛW. T)) (mk_rtm G u (E. ④{Abbr} {u, D, V}) S T) | rtm_push : ∀G,u,E,W,T. - rtm_step (mk_rtm G u E (◊) (+ⓛW. T)) - (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (◊) T) + rtm_step (mk_rtm G u E (Ⓔ) (+ⓛW. T)) + (mk_rtm G (u + 1) (E. ④{Abst} {u, E, W}) (Ⓔ) T) | rtm_theta : ∀G,u,E,S,V,T. rtm_step (mk_rtm G u E S (+ⓓV. T)) (mk_rtm G u (E. ④{Abbr} {u, E, V}) S T) diff --git a/matita/matita/contribs/lambdadelta/basic_2/names.txt b/matita/matita/contribs/lambdadelta/basic_2/names.txt index eba318b7e..c24186766 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/names.txt +++ b/matita/matita/contribs/lambdadelta/basic_2/names.txt @@ -39,6 +39,7 @@ NAMING CONVENTIONS FOR CONSTRUCTORS 2: binary A: application to vector +E: empty list F: boolean false T: boolean true diff --git a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma index dc7c7d309..8e234a5c1 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/relocation/lifts_vector.ma @@ -19,7 +19,7 @@ include "basic_2/relocation/lifts.ma". (* Basic_2A1: includes: liftv_nil liftv_cons *) inductive liftsv (f:rtmap): relation (list term) ≝ -| liftsv_nil : liftsv f (◊) (◊) +| liftsv_nil : liftsv f (Ⓔ) (Ⓔ) | liftsv_cons: ∀T1s,T2s,T1,T2. ⬆*[f] T1 ≘ T2 → liftsv f T1s T2s → liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s) @@ -33,13 +33,13 @@ interpretation "generic relocation (term vector)" (* Basic inversion lemmas ***************************************************) -fact liftsv_inv_nil1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → X = ◊ → Y = ◊. +fact liftsv_inv_nil1_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → X = Ⓔ → Y = Ⓔ. #f #X #Y * -X -Y // #T1s #T2s #T1 #T2 #_ #_ #H destruct qed-. (* Basic_2A1: includes: liftv_inv_nil1 *) -lemma liftsv_inv_nil1: ∀f,Y. ⬆*[f] ◊ ≘ Y → Y = ◊. +lemma liftsv_inv_nil1: ∀f,Y. ⬆*[f] Ⓔ ≘ Y → Y = Ⓔ. /2 width=5 by liftsv_inv_nil1_aux/ qed-. fact liftsv_inv_cons1_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y → @@ -58,12 +58,12 @@ lemma liftsv_inv_cons1: ∀f:rtmap. ∀T1,T1s,Y. ⬆*[f] T1 ⨮ T1s ≘ Y → Y = T2 ⨮ T2s. /2 width=3 by liftsv_inv_cons1_aux/ qed-. -fact liftsv_inv_nil2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → Y = ◊ → X = ◊. +fact liftsv_inv_nil2_aux: ∀f,X,Y. ⬆*[f] X ≘ Y → Y = Ⓔ → X = Ⓔ. #f #X #Y * -X -Y // #T1s #T2s #T1 #T2 #_ #_ #H destruct qed-. -lemma liftsv_inv_nil2: ∀f,X. ⬆*[f] X ≘ ◊ → X = ◊. +lemma liftsv_inv_nil2: ∀f,X. ⬆*[f] X ≘ Ⓔ → X = Ⓔ. /2 width=5 by liftsv_inv_nil2_aux/ qed-. fact liftsv_inv_cons2_aux: ∀f:rtmap. ∀X,Y. ⬆*[f] X ≘ Y → diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma index d8768fcf8..31bcb5aa5 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_aaa.ma @@ -31,7 +31,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_inv_sort … HA) -HA #H destruct >(lifts_inv_sort1 … H0) -H0 lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom - lapply (s4 … HAtom G L2 (◊)) /2 width=1 by/ + lapply (s4 … HAtom G L2 (Ⓔ)) /2 width=1 by/ | #i #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct elim (aaa_inv_lref_drops … HA) -HA #I #K1 #V1 #HLK1 #HKV1 elim (lifts_inv_lref1 … H0) -H0 #j #Hf #H destruct @@ -46,16 +46,16 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. elim (lsubc_inv_bind2 … H) -H * [ #K2 #HK20 #H destruct lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b - lapply (s5 … HA ? G ? ? (◊) … HV0 ?) -HA + lapply (s5 … HA ? G ? ? (Ⓔ) … HV0 ?) -HA /4 width=11 by acr_lifts, fqup_lref, drops_inv_gen/ | #K2 #V2 #W2 #B #HKV2 #HK2V0 #HKV0B #_ #H1 #H2 destruct -IH -HLK1 lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b lapply (aaa_lifts … HKV1 … HK01 … HV10) -HKV1 -HK01 -HV10 #HKV0A lapply (aaa_mono … HKV0B … HKV0A) #H destruct -HKV0B -HKV0A elim (lifts_total V2 (𝐔❴↑j❵)) #V3 #HV23 - lapply (s5 … HA … G … (◊) … (ⓝW2.V2) (ⓝV.V3) ????) + lapply (s5 … HA … G … (Ⓔ) … (ⓝW2.V2) (ⓝV.V3) ????) [3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2 - lapply (s7 … HA G L2 (◊)) -HA /3 width=7 by acr_lifts/ + lapply (s7 … HA G L2 (Ⓔ)) -HA /3 width=7 by acr_lifts/ ] | #l #HG #HL #HT #A #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct -IH elim (aaa_inv_gref … HA) @@ -65,7 +65,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (acr_gcr … H1RP H2RP A) #HA lapply (acr_gcr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - lapply (s6 … HA G L2 (◊) (◊)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/ + lapply (s6 … HA G L2 (Ⓔ) (Ⓔ)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/ | #W #T #HG #HL #HT #Z0 #HA #b #f #L0 #HL01 #X0 #H0 #L2 #HL20 destruct elim (aaa_inv_abst … HA) -HA #B #A #HW #HT #H destruct elim (lifts_inv_bind1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct @@ -85,7 +85,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. elim (aaa_inv_cast … HA) -HA #HW #HT elim (lifts_inv_flat1 … H0) -H0 #W0 #T0 #HW0 #HT0 #H destruct lapply (acr_gcr … H1RP H2RP A) #HA - lapply (s7 … HA G L2 (◊)) /3 width=10 by/ + lapply (s7 … HA G L2 (Ⓔ)) /3 width=10 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma index ae7140efe..f9b13438a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/static/gcp_cr.ma @@ -105,7 +105,7 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → #B #A #IHB #IHA @mk_gcr [ #G #L #T #H elim (cp1 … H1RP G L) #s #HK - lapply (s2 … IHB G L (◊) … HK) // #HB + lapply (s2 … IHB G L (Ⓔ) … HK) // #HB lapply (H (𝐈𝐝) L (⋆s) T ? ? ?) -H /3 width=6 by s1, cp3, drops_refl, lifts_refl/ | #G #L #Vs #HVs #T #H1T #H2T #f #L0 #V0 #X #HL0 #H #HB @@ -165,11 +165,11 @@ lapply (acr_gcr … H1RP H2RP A) #HCA lapply (acr_gcr … H1RP H2RP B) #HCB elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct lapply (acr_lifts … H1RP … HW … HL0 … HW0) -HW #HW0 -lapply (s3 … HCA … p G L0 (◊)) #H @H -H -lapply (s6 … HCA G L0 (◊) (◊) ?) // #H @H -H +lapply (s3 … HCA … p G L0 (Ⓔ)) #H @H -H +lapply (s6 … HCA G L0 (Ⓔ) (Ⓔ) ?) // #H @H -H [ @(HA … HL0) // | lapply (s1 … HCB) -HCB #HCB - lapply (s7 … H2RP G L0 (◊)) /3 width=1 by/ + lapply (s7 … H2RP G L0 (Ⓔ)) /3 width=1 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma index 8483917c4..085e35dac 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv.ma @@ -12,7 +12,6 @@ (* *) (**************************************************************************) -include "ground_2/lib/list2.ma". include "basic_2/notation/constructors/star_0.ma". include "basic_2/notation/constructors/dxbind2_3.ma". include "basic_2/notation/constructors/dxabbr_2.ma". @@ -22,20 +21,32 @@ include "basic_2/syntax/term.ma". (* GLOBAL ENVIRONMENTS ******************************************************) (* global environments *) -definition genv ≝ list2 bind2 term. +inductive genv: Type[0] ≝ +| GAtom: genv (* empty *) +| GBind: genv → bind2 → term → genv (* binding construction *) +. interpretation "sort (global environment)" - 'Star = (nil2 bind2 term). + 'Star = (GAtom). interpretation "global environment binding construction (binary)" - 'DxBind2 L I T = (cons2 bind2 term I T L). + 'DxBind2 G I T = (GBind G I T). interpretation "abbreviation (global environment)" - 'DxAbbr L T = (cons2 bind2 term Abbr T L). + 'DxAbbr G T = (GBind G Abbr T). interpretation "abstraction (global environment)" - 'DxAbst L T = (cons2 bind2 term Abst T L). + 'DxAbst G T = (GBind G Abst T). (* Basic properties *********************************************************) -axiom eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2). +lemma eq_genv_dec: ∀G1,G2:genv. Decidable (G1 = G2). +#G1 elim G1 -G1 [| #G1 #I1 #T1 #IHG1 ] * [2,4: #G2 #I2 #T2 ] +[3: /2 width=1 by or_introl/ +|2: elim (eq_bind2_dec I1 I2) #HI + [ elim (IHG1 G2) -IHG1 #HG + [ elim (eq_term_dec T1 T2) #HT /2 width=1 by or_introl/ ] + ] +] +@or_intror #H destruct /2 width=1 by/ +qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma similarity index 60% rename from matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma rename to matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma index f9d93b74e..15244609a 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list2.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/genv_length.ma @@ -12,25 +12,14 @@ (* *) (**************************************************************************) -include "ground_2/notation/constructors/nil_0.ma". -include "ground_2/notation/constructors/oplusright_5.ma". -include "ground_2/lib/arith.ma". +include "basic_2/syntax/genv.ma". -(* LISTS OF PAIRS ***********************************************************) +(* LENGTH OF A GLOBAL ENVIRONMENT *******************************************) -inductive list2 (A1,A2:Type[0]) : Type[0] := - | nil2 : list2 A1 A2 - | cons2: A1 → A2 → list2 A1 A2 → list2 A1 A2. - -interpretation "nil (list of pairs)" 'Nil = (nil2 ? ?). - -interpretation "cons (list of pairs)" - 'OPlusRight A1 A2 hd1 hd2 tl = (cons2 A1 A2 hd1 hd2 tl). - -rec definition length2 A1 A2 (l:list2 A1 A2) on l ≝ match l with -[ nil2 ⇒ 0 -| cons2 _ _ l ⇒ ↑(length2 A1 A2 l) +rec definition glength G on G ≝ match G with +[ GAtom ⇒ 0 +| GBind G _ _ ⇒ ↑(glength G) ]. -interpretation "length (list of pairs)" - 'card l = (length2 ? ? l). +interpretation "length (global environment)" + 'card G = (glength G). diff --git a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma index cbb43ebb2..df6e6e1cf 100644 --- a/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2/syntax/term_vector.ma @@ -29,7 +29,7 @@ interpretation "application to vector (term)" (* Basic properties *********************************************************) -lemma applv_nil: ∀T. Ⓐ◊.T = T. +lemma applv_nil: ∀T. ⒶⒺ.T = T. // qed. lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T. 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 51f54e6e3..46ccf13b9 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 @@ -250,6 +250,7 @@ table { } ] [ { "global environments" * } { + [ [ "" ] "genv_length" + "( |?| )" * ] [ [ "" ] "genv" * ] } ] diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma index ffce31286..0ea6ae285 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/lib/list.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground_2/notation/constructors/nil_0.ma". +include "ground_2/notation/constructors/circledE_1.ma". include "ground_2/notation/constructors/oplusright_3.ma". include "ground_2/lib/arith.ma". @@ -22,7 +22,7 @@ inductive list (A:Type[0]) : Type[0] := | nil : list A | cons: A → list A → list A. -interpretation "nil (list)" 'Nil = (nil ?). +interpretation "nil (list)" 'CircledE A = (nil A). interpretation "cons (list)" 'OPlusRight A hd tl = (cons A hd tl). @@ -50,11 +50,11 @@ lemma length_cons (A:Type[0]) (l:list A) (a:A): |a⨮l| = ↑|l|. (* Basic inversion lemmas on length *****************************************) -lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = ◊. +lemma length_inv_zero_dx (A:Type[0]) (l:list A): |l| = 0 → l = Ⓔ. #A * // #a #l >length_cons #H destruct qed-. -lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = ◊. +lemma length_inv_zero_sn (A:Type[0]) (l:list A): 0 = |l| → l = Ⓔ. /2 width=1 by length_inv_zero_dx/ qed-. lemma length_inv_succ_dx (A:Type[0]) (l:list A) (x): |l| = ↑x → diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/circledE_1.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/circledE_1.ma new file mode 100644 index 000000000..53cf85698 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/circledE_1.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) + +notation < "hvbox( Ⓔ )" + non associative with precedence 55 + for @{ 'CircledE $S }. + +notation > "hvbox( Ⓔ )" + non associative with precedence 55 + for @{ 'CircledE ? }. + +notation > "hvbox( Ⓔ{ term 46 C } )" + non associative with precedence 55 + for @{ 'CircledE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/diamond_0.ma similarity index 94% rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/diamond_0.ma index 6ea5151a9..4f218dd61 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/nil_0.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/diamond_0.ma @@ -15,5 +15,5 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) notation "◊" - non associative with precedence 46 - for @{ 'Nil }. + non associative with precedence 55 + for @{ 'Diamond }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/semicolon_3.ma similarity index 68% rename from matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma rename to matita/matita/contribs/lambdadelta/ground_2/notation/constructors/semicolon_3.ma index 8ea93cad8..44b7c17a5 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/oplusright_5.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/notation/constructors/semicolon_3.ma @@ -14,16 +14,6 @@ (* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************) -notation < "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )" +notation "hvbox( { term 46 hd1, break term 46 hd2 }; break term 46 tl )" non associative with precedence 47 - for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }. - -notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮ break term 46 tl )" - non associative with precedence 47 - for @{ 'OPlusRight ? ? $hd1 $hd2 $tl }. -(* -(**) fix pair notation -notation > "hvbox( { term 46 hd1, break term 46 hd2 }⨮{ break term 46 S1, break term 46 S2 } break term 46 tl )" - non associative with precedence 47 - for @{ 'OPlusRight $S1 $S2 $hd1 $hd2 $tl }. -*) + for @{ 'Semicolon $hd1 $hd2 $tl }. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma index 3bd8fa3f9..b6062f295 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2.ma @@ -12,8 +12,18 @@ (* *) (**************************************************************************) -include "ground_2/lib/list2.ma". +include "ground_2/notation/constructors/diamond_0.ma". +include "ground_2/notation/constructors/semicolon_3.ma". +include "ground_2/lib/arith.ma". (* MULTIPLE RELOCATION WITH PAIRS *******************************************) -definition mr2: Type[0] ≝ list2 nat nat. +inductive mr2: Type[0] := + | nil2 : mr2 + | cons2: nat → nat → mr2 → mr2. + +interpretation "nil (multiple relocation with pairs)" + 'Diamond = (nil2). + +interpretation "cons (multiple relocation with pairs)" + 'Semicolon hd1 hd2 tl = (cons2 hd1 hd2 tl). diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma index 2e148b71d..77aa3917c 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_at.ma @@ -20,9 +20,9 @@ include "ground_2/relocation/mr2.ma". inductive at: mr2 → relation nat ≝ | at_nil: ∀i. at (◊) i i | at_lt : ∀cs,l,m,i1,i2. i1 < l → - at cs i1 i2 → at ({l, m} ⨮ cs) i1 i2 + at cs i1 i2 → at ({l, m};cs) i1 i2 | at_ge : ∀cs,l,m,i1,i2. l ≤ i1 → - at cs (i1 + m) i2 → at ({l, m} ⨮ cs) i1 i2 + at cs (i1 + m) i2 → at ({l, m};cs) i1 i2 . interpretation "application (multiple relocation with pairs)" @@ -42,7 +42,7 @@ lemma at_inv_nil: ∀i1,i2. @⦃i1, ◊⦄ ≘ i2 → i1 = i2. /2 width=3 by at_inv_nil_aux/ qed-. fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≘ i2 → - ∀l,m,cs0. cs = {l, m} ⨮ cs0 → + ∀l,m,cs0. cs = {l, m};cs0 → i1 < l ∧ @⦃i1, cs0⦄ ≘ i2 ∨ l ≤ i1 ∧ @⦃i1 + m, cs0⦄ ≘ i2. #cs #i1 #i2 * -cs -i1 -i2 @@ -52,19 +52,19 @@ fact at_inv_cons_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≘ i2 → ] qed-. -lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 → +lemma at_inv_cons: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 → i1 < l ∧ @⦃i1, cs⦄ ≘ i2 ∨ l ≤ i1 ∧ @⦃i1 + m, cs⦄ ≘ i2. /2 width=3 by at_inv_cons_aux/ qed-. -lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 → +lemma at_inv_cons_lt: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 → i1 < l → @⦃i1, cs⦄ ≘ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hli1 #_ #Hi1l elim (lt_le_false … Hi1l Hli1) qed-. -lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m} ⨮ cs⦄ ≘ i2 → +lemma at_inv_cons_ge: ∀cs,l,m,i1,i2. @⦃i1, {l, m};cs⦄ ≘ i2 → l ≤ i1 → @⦃i1 + m, cs⦄ ≘ i2. #cs #l #m #i1 #m2 #H elim (at_inv_cons … H) -H * // #Hi1l #_ #Hli1 diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma index b721754b6..f118cf129 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_minus.ma @@ -20,9 +20,9 @@ include "ground_2/relocation/mr2.ma". inductive minuss: nat → relation mr2 ≝ | minuss_nil: ∀i. minuss i (◊) (◊) | minuss_lt : ∀cs1,cs2,l,m,i. i < l → minuss i cs1 cs2 → - minuss i ({l, m} ⨮ cs1) ({l - i, m} ⨮ cs2) + minuss i ({l, m};cs1) ({l - i, m};cs2) | minuss_ge : ∀cs1,cs2,l,m,i. l ≤ i → minuss (m + i) cs1 cs2 → - minuss i ({l, m} ⨮ cs1) cs2 + minuss i ({l, m};cs1) cs2 . interpretation "minus (multiple relocation with pairs)" @@ -42,10 +42,10 @@ lemma minuss_inv_nil1: ∀cs2,i. ◊ ▭ i ≘ cs2 → cs2 = ◊. /2 width=4 by minuss_inv_nil1_aux/ qed-. fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≘ cs2 → - ∀l,m,cs. cs1 = {l, m} ⨮ cs → + ∀l,m,cs. cs1 = {l, m};cs → l ≤ i ∧ cs ▭ m + i ≘ cs2 ∨ ∃∃cs0. i < l & cs ▭ i ≘ cs0 & - cs2 = {l - i, m} ⨮ cs0. + cs2 = {l - i, m};cs0. #cs1 #cs2 #i * -cs1 -cs2 -i [ #i #l #m #cs #H destruct | #cs1 #cs #l1 #m1 #i1 #Hil1 #Hcs #l2 #m2 #cs2 #H destruct /3 width=3 by ex3_intro, or_intror/ @@ -53,22 +53,22 @@ fact minuss_inv_cons1_aux: ∀cs1,cs2,i. cs1 ▭ i ≘ cs2 → ] qed-. -lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 → +lemma minuss_inv_cons1: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 → l ≤ i ∧ cs1 ▭ m + i ≘ cs2 ∨ ∃∃cs. i < l & cs1 ▭ i ≘ cs & - cs2 = {l - i, m} ⨮ cs. + cs2 = {l - i, m};cs. /2 width=3 by minuss_inv_cons1_aux/ qed-. -lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 → +lemma minuss_inv_cons1_ge: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 → l ≤ i → cs1 ▭ m + i ≘ cs2. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * // #cs #Hil #_ #_ #Hli elim (lt_le_false … Hil Hli) qed-. -lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m} ⨮ cs1 ▭ i ≘ cs2 → +lemma minuss_inv_cons1_lt: ∀cs1,cs2,l,m,i. {l, m};cs1 ▭ i ≘ cs2 → i < l → - ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m} ⨮ cs. + ∃∃cs. cs1 ▭ i ≘ cs & cs2 = {l - i, m};cs. #cs1 #cs2 #l #m #i #H elim (minuss_inv_cons1 … H) -H * /2 width=3 by ex2_intro/ #Hli #_ #Hil elim (lt_le_false … Hil Hli) qed-. diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma index 7d9e5e603..e1ef5d287 100644 --- a/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/mr2_plus.ma @@ -18,7 +18,7 @@ include "ground_2/relocation/mr2.ma". rec definition pluss (cs:mr2) (i:nat) on cs ≝ match cs with [ nil2 ⇒ ◊ -| cons2 l m cs ⇒ {l + i, m} ⨮ pluss cs i +| cons2 l m cs ⇒ {l + i, m};pluss cs i ]. interpretation "plus (multiple relocation with pairs)" @@ -26,7 +26,7 @@ interpretation "plus (multiple relocation with pairs)" (* Basic properties *********************************************************) -lemma pluss_SO2: ∀l,m,cs. ({l, m} ⨮ cs) + 1 = {↑l, m} ⨮ cs + 1. +lemma pluss_SO2: ∀l,m,cs. ({l, m};cs) + 1 = {↑l, m};cs + 1. normalize // qed. (* Basic inversion lemmas ***************************************************) @@ -36,8 +36,8 @@ lemma pluss_inv_nil2: ∀i,cs. cs + i = ◊ → cs = ◊. #l #m #cs #H destruct qed. -lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m} ⨮ cs2 → - ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m} ⨮ cs1. +lemma pluss_inv_cons2: ∀i,l,m,cs2,cs. cs + i = {l, m};cs2 → + ∃∃cs1. cs1 + i = cs2 & cs = {l - i, m};cs1. #i #l #m #cs2 * [ normalize #H destruct | #l1 #m1 #cs1 whd in ⊢ (??%?→?); #H destruct 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 1cd156ab1..4fc221673 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 @@ -33,7 +33,7 @@ table { [ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≘ ? )" "trace_after ( ? ⊚ ? ≘ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )" "trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≘ ? )" "trace_snot ( ∁ ? )" * ] *) - [ "mr2" "mr2_at ( @⦃?,?⦄ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ] + [ "mr2 ( ◊ ) ( {?,?};? )" "mr2_at ( @⦃?,?⦄ ≘ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≘ ? )" * ] } ] } @@ -53,7 +53,7 @@ table { [ { "extensions to the library" * } { [ { "" * } { [ "stream ( ? ⨮{?} ? )" "stream_eq ( ? ≗{?} ? )" "stream_hdtl ( ⫰{?}? )" "stream_tls ( ⫰*{?}[?]? )" * ] - [ "list ( ◊ ) ( ? ⨮{?} ? ) ( |?| )" "list2 ( ◊ ) ( {?,?} ⨮{?,?} ? ) ( |?| )" * ] + [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? ) ( |?| )" * ] [ "bool ( Ⓕ ) ( Ⓣ )" "arith ( ?^? ) ( ↑? ) ( ↓? ) ( ? ∨ ? ) ( ? ∧ ? )" * ] [ "logic ( ⊥ ) ( ⊤ )" "relations ( ? ⊆ ? )" "functions" "exteq ( ? ≐{?,?} ? )" "star" "ltc" * ] } diff --git a/matita/matita/contribs/lambdadelta/replace.sh b/matita/matita/contribs/lambdadelta/replace.sh index e121468e2..291dc454a 100644 --- a/matita/matita/contribs/lambdadelta/replace.sh +++ b/matita/matita/contribs/lambdadelta/replace.sh @@ -1,5 +1,5 @@ #!/bin/sh -for SRC in `find ground_2 basic_2 -name "*.ma" -or -name "*.tbl"`; do +for SRC in `find ground_2 basic_2 apps_2 -name "*.ma" -or -name "*.tbl"`; do sed "s!$1!$2!g" ${SRC} > ${SRC}.new if [ ! -s ${SRC}.new ] || diff ${SRC} ${SRC}.new > /dev/null; then rm -f ${SRC}.new; -- 2.39.2