From: Ferruccio Guidi Date: Sat, 4 Dec 2021 16:43:16 +0000 (+0100) Subject: update in ground X-Git-Tag: make_still_working~128 X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=12dc655b7f5321b33b93a310d53e23e60e090caa update in ground + updated notation and terminology for lists --- 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 1f3c49413..1777a2d00 100644 --- a/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma +++ b/matita/matita/contribs/lambdadelta/apps_2/models/tm_props.ma @@ -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 (lifts_inv_sort1 … H) -H 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 #G #L1 #K1 #V1 #B #i #HLK1 #HKV1B #IHB #L0 #cs #HL01 #X #H #L2 #HL20 lapply (acr_gcr … H1RP H2RP B) #HB elim (lifts_inv_lref1 … H) -H #i1 #Hi1 #H destruct @@ -45,7 +45,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. [ #K2 #HK20 #H destruct elim (lift_total V0 0 (i0 +1)) #V #HV0 elim (lifts_lift_trans … Hi0 … Hcs0 … HV10 … HV0) -HV10 #V2 #HV12 #HV2 - lapply (s5 … HB ? G ? ? (Ⓔ) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) + lapply (s5 … HB ? G ? ? (ⓔ) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *) | -HLK1 -IHB -HL01 -HL20 -HK1b -Hi0 -Hcs0 #K2 #V2 #A2 #HKV2A #H1KV0A #H2KV0A #_ #H1 #H2 destruct lapply (drop_fwd_drop2 … HLK2) #HLK2b @@ -53,22 +53,22 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. lapply (aaa_mono … H2KV0A … HKV0B) #H destruct -H2KV0A -HKV0B elim (lift_total V0 0 (i0 +1)) #V3 #HV03 elim (lift_total V2 0 (i0 +1)) #V #HV2 - lapply (s5 … HB ? G ? ? (Ⓔ) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/ - lapply (s7 … HB G L2 (Ⓔ)) /3 width=7 by gcr_lift/ + lapply (s5 … HB ? G ? ? (ⓔ) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/ + lapply (s7 … HB G L2 (ⓔ)) /3 width=7 by gcr_lift/ ] | #a #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20 elim (lifts_inv_bind1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (acr_gcr … H1RP H2RP A) #HA lapply (acr_gcr … H1RP H2RP B) #HB lapply (s1 … HB) -HB #HB - lapply (s6 … HA G L2 (Ⓔ) (Ⓔ)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/ + lapply (s6 … HA G L2 (ⓔ) (ⓔ)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/ | #a #G #L #W #T #B #A #HLWB #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL02 elim (lifts_inv_bind1 … H) -H #W0 #T0 #HW0 #HT0 #H destruct @(acr_abst … H1RP H2RP) /2 width=5 by/ #L3 #V3 #W3 #T3 #cs3 #HL32 #HW03 #HT03 #H1B #H2B elim (drops_lsubc_trans … H1RP … HL32 … HL02) -L2 #L2 #HL32 #HL20 - lapply (aaa_lifts … L2 W3 … (cs @@ cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B - @(IHA (L2. ⓛW3) … (cs + 1 @@ cs3 + 1)) -IHA + lapply (aaa_lifts … L2 W3 … (cs ;; cs3) … HLWB) -HLWB /2 width=4 by drops_trans, lifts_trans/ #HLW2B + @(IHA (L2. ⓛW3) … (cs + 1 ;; cs3 + 1)) -IHA /3 width=5 by lsubc_beta, drops_trans, drops_skip, lifts_trans/ | #G #L #V #T #B #A #_ #_ #IHB #IHA #L0 #cs #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct @@ -76,7 +76,7 @@ theorem acr_aaa_csubc_lifts: ∀RR,RS,RP. | #G #L #V #T #A #_ #_ #IH1A #IH2A #L0 #cs #HL0 #X #H #L2 #HL20 elim (lifts_inv_flat1 … H) -H #V0 #T0 #HV0 #HT0 #H destruct lapply (acr_gcr … H1RP H2RP A) #HA - lapply (s7 … HA G L2 (Ⓔ)) /3 width=5 by/ + lapply (s7 … HA G L2 (ⓔ)) /3 width=5 by/ ] qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_cr.ma b/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_cr.ma index bb48bab78..836994f34 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/computation/gcp_cr.ma @@ -97,8 +97,8 @@ 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) #k #HK - lapply (H L (⋆k) T (◊) ? ? ?) -H // - [ lapply (s2 … IHB G L (Ⓔ) … HK) // + lapply (H L (⋆k) T (𝐞) ? ? ?) -H // + [ lapply (s2 … IHB G L (ⓔ) … HK) // | /3 width=6 by s1, cp3/ ] | #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #cs #HL0 #H #HB @@ -156,11 +156,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 (gcr_lifts … H1RP … HL0 … HW0 HW) -HW #HW0 -lapply (s3 … HCA … a G L0 (Ⓔ)) #H @H -H -lapply (s6 … HCA G L0 (Ⓔ) (Ⓔ) ?) // #H @H -H +lapply (s3 … HCA … a 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_2A/grammar/lenv_append.ma b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma index cd7a3d788..6ac04a83d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/grammar/lenv_append.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/append_2.ma". +include "ground/notation/functions/double_semicolon_2.ma". include "basic_2A/notation/functions/snbind2_3.ma". include "basic_2A/notation/functions/snabbr_2.ma". include "basic_2A/notation/functions/snabst_2.ma". @@ -25,23 +25,28 @@ let rec append L K on K ≝ match K with | LPair K I V ⇒ (append L K). ⓑ{I} V ]. -interpretation "append (local environment)" 'Append L1 L2 = (append L1 L2). +interpretation + "append (local environment)" + 'DoubleSemicolon L1 L2 = (append L1 L2). -interpretation "local environment tail binding construction (binary)" - 'SnBind2 I T L = (append (LPair LAtom I T) L). +interpretation + "local environment tail binding construction (binary)" + 'SnBind2 I T L = (append (LPair LAtom I T) L). -interpretation "tail abbreviation (local environment)" - 'SnAbbr T L = (append (LPair LAtom Abbr T) L). +interpretation + "tail abbreviation (local environment)" + 'SnAbbr T L = (append (LPair LAtom Abbr T) L). -interpretation "tail abstraction (local environment)" - 'SnAbst L T = (append (LPair LAtom Abst T) L). +interpretation + "tail abstraction (local environment)" + 'SnAbst L T = (append (LPair LAtom Abst T) L). definition d_appendable_sn: predicate (lenv→relation term) ≝ λR. - ∀K,T1,T2. R K T1 T2 → ∀L. R (L @@ K) T1 T2. + ∀K,T1,T2. R K T1 T2 → ∀L. R (L ;; K) T1 T2. (* Basic properties *********************************************************) -lemma append_atom_sn: ∀L. ⋆ @@ L = L. +lemma append_atom_sn: ∀L. ⋆ ;; L = L. #L elim L -L normalize // qed. @@ -49,7 +54,7 @@ lemma append_assoc: associative … append. #L1 #L2 #L3 elim L3 -L3 normalize // qed. -lemma append_length: ∀L1,L2. |L1 @@ L2| = |L1| + |L2|. +lemma append_length: ∀L1,L2. |L1 ;; L2| = |L1| + |L2|. #L1 #L2 elim L2 -L2 normalize // qed. @@ -66,7 +71,7 @@ qed-. (* Basic inversion lemmas ***************************************************) -lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → +lemma append_inj_sn: ∀K1,K2,L1,L2. L1 ;; K1 = L2 ;; K2 → |K1| = |K2| → L1 = L2 ∧ K1 = K2. #K1 elim K1 -K1 [ * normalize /2 width=1 by conj/ @@ -81,7 +86,7 @@ lemma append_inj_sn: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |K1| = |K2| → qed-. (* Note: lemma 750 *) -lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → +lemma append_inj_dx: ∀K1,K2,L1,L2. L1 ;; K1 = L2 ;; K2 → |L1| = |L2| → L1 = L2 ∧ K1 = K2. #K1 elim K1 -K1 [ * normalize /2 width=1 by conj/ @@ -99,11 +104,11 @@ lemma append_inj_dx: ∀K1,K2,L1,L2. L1 @@ K1 = L2 @@ K2 → |L1| = |L2| → ] qed-. -lemma append_inv_refl_dx: ∀L,K. L @@ K = L → K = ⋆. +lemma append_inv_refl_dx: ∀L,K. L ;; K = L → K = ⋆. #L #K #H elim (append_inj_dx … (⋆) … H) // qed-. -lemma append_inv_pair_dx: ∀I,L,K,V. L @@ K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. +lemma append_inv_pair_dx: ∀I,L,K,V. L ;; K = L.ⓑ{I}V → K = ⋆.ⓑ{I}V. #I #L #K #V #H elim (append_inj_dx … (⋆.ⓑ{I}V) … H) // qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma index 0320d8639..cd7fc2211 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops.ma @@ -22,7 +22,7 @@ include "basic_2A/multiple/lifts_vector.ma". (* ITERATED LOCAL ENVIRONMENT SLICING ***************************************) inductive drops (s:bool): mr2 → relation lenv ≝ -| drops_nil : ∀L. drops s (◊) L L +| drops_nil : ∀L. drops s (𝐞) L L | drops_cons: ∀L1,L,L2,cs,l,m. drops s cs L1 L → ⬇[s, l, m] L ≡ L2 → drops s (❨l, m❩; cs) L1 L2 . @@ -49,12 +49,12 @@ definition d_liftables1_all: relation2 lenv term → predicate bool ≝ (* Basic inversion lemmas ***************************************************) -fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = ◊ → L1 = L2. +fact drops_inv_nil_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → cs = 𝐞 → L1 = L2. #L1 #L2 #s #cs * -L1 -L2 -cs // #L1 #L #L2 #l #m #cs #_ #_ #H destruct qed-. -lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, ◊] L1 ≡ L2 → L1 = L2. +lemma drops_inv_nil: ∀L1,L2,s. ⬇*[s, 𝐞] L1 ≡ L2 → L1 = L2. /2 width=4 by drops_inv_nil_aux/ qed-. fact drops_inv_cons_aux: ∀L1,L2,s,cs. ⬇*[s, cs] L1 ≡ L2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma index dbe215329..36f7cc9ab 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/drops_drops.ma @@ -20,6 +20,6 @@ include "basic_2A/multiple/drops_drop.ma". (* Main properties **********************************************************) theorem drops_trans: ∀L,L2,s,cs2. ⬇*[s, cs2] L ≡ L2 → ∀L1,cs1. ⬇*[s, cs1] L1 ≡ L → - ⬇*[s, cs2 @@ cs1] L1 ≡ L2. + ⬇*[s, cs2 ;; cs1] L1 ≡ L2. #L #L2 #s #cs2 #H elim H -L -L2 -cs2 /3 width=3 by drops_cons/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/frees_append.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/frees_append.ma index 4b0ffce66..4154f4898 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/frees_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/frees_append.ma @@ -20,7 +20,7 @@ include "basic_2A/multiple/frees.ma". (* Properties on append for local environments ******************************) lemma frees_append: ∀L2,U,l,i. L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| → - ∀L1. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. + ∀L1. L1 ;; L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. #L2 #U #l #i #H elim H -L2 -U -l -i /3 width=2 by frees_eq/ #I #L2 #K2 #U #W #l #i #j #Hlj #Hji #HnU #HLK2 #_ #IHW #Hi #L1 lapply (drop_fwd_length_minus2 … HLK2) normalize #H0 @@ -33,7 +33,7 @@ qed. (* Inversion lemmas on append for local environments ************************) -fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 @@ L2 → +fact frees_inv_append_aux: ∀L,U,l,i. L ⊢ i ϵ 𝐅*[l]⦃U⦄ → ∀L1,L2. L = L1 ;; L2 → i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. #L #U #l #i #H elim H -L -U -l -i /3 width=2 by frees_eq/ #Z #L #Y #U #X #l #i #j #Hlj #Hji #HnU #HLY #_ #IHW #L1 #L2 #H #Hi destruct @@ -47,6 +47,6 @@ lapply (drop_O1_inv_append1_le … HLY … HLK2) -HLY ] qed-. -lemma frees_inv_append: ∀L1,L2,U,l,i. L1 @@ L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → +lemma frees_inv_append: ∀L1,L2,U,l,i. L1 ;; L2 ⊢ i ϵ 𝐅*[l]⦃U⦄ → i ≤ |L2| → L2 ⊢ i ϵ 𝐅*[l]⦃U⦄. /2 width=4 by frees_inv_append_aux/ qed-. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma index f83cbdf88..d49e1608d 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts.ma @@ -20,7 +20,7 @@ include "basic_2A/substitution/lift.ma". (* GENERIC TERM RELOCATION **************************************************) inductive lifts: mr2 → relation term ≝ -| lifts_nil : ∀T. lifts (◊) T T +| lifts_nil : ∀T. lifts (𝐞) T T | lifts_cons: ∀T1,T,T2,cs,l,m. ⬆[l,m] T1 ≡ T → lifts cs T T2 → lifts (❨l, m❩; cs) T1 T2 . @@ -30,12 +30,12 @@ interpretation "generic relocation (term)" (* Basic inversion lemmas ***************************************************) -fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = ◊ → T1 = T2. +fact lifts_inv_nil_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → cs = 𝐞 → T1 = T2. #T1 #T2 #cs * -T1 -T2 -cs // #T1 #T #T2 #l #m #cs #_ #_ #H destruct qed-. -lemma lifts_inv_nil: ∀T1,T2. ⬆*[◊] T1 ≡ T2 → T1 = T2. +lemma lifts_inv_nil: ∀T1,T2. ⬆*[𝐞] T1 ≡ T2 → T1 = T2. /2 width=3 by lifts_inv_nil_aux/ qed-. fact lifts_inv_cons_aux: ∀T1,T2,cs. ⬆*[cs] T1 ≡ T2 → diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_lifts.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_lifts.ma index a486fff72..fe447ef32 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_lifts.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_lifts.ma @@ -20,6 +20,6 @@ include "basic_2A/multiple/lifts_lift.ma". (* Main properties **********************************************************) theorem lifts_trans: ∀T1,T,cs1. ⬆*[cs1] T1 ≡ T → ∀T2:term. ∀cs2. ⬆*[cs2] T ≡ T2 → - ⬆*[cs1 @@ cs2] T1 ≡ T2. + ⬆*[cs1 ;; cs2] T1 ≡ T2. #T1 #T #cs1 #H elim H -T1 -T -cs1 /3 width=3 by lifts_cons/ qed. diff --git a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_vector.ma b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_vector.ma index 6c57aba3b..8c432fa05 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/multiple/lifts_vector.ma @@ -18,7 +18,7 @@ include "basic_2A/multiple/lifts.ma". (* GENERIC TERM VECTOR RELOCATION *******************************************) inductive liftsv (cs:mr2) : relation (list term) ≝ -| liftsv_nil : liftsv cs (Ⓔ) (Ⓔ) +| liftsv_nil : liftsv cs (ⓔ) (ⓔ) | liftsv_cons: ∀T1s,T2s,T1,T2. ⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s → liftsv cs (T1 ⨮ T1s) (T2 ⨮ T2s) diff --git a/matita/matita/contribs/lambdadelta/basic_2A/substitution/drop_append.ma b/matita/matita/contribs/lambdadelta/basic_2A/substitution/drop_append.ma index 16fb627ad..3bed5ca5a 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/substitution/drop_append.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/substitution/drop_append.ma @@ -22,19 +22,19 @@ include "basic_2A/substitution/drop.ma". fact drop_O1_append_sn_le_aux: ∀L1,L2,s,l,m. ⬇[s, l, m] L1 ≡ L2 → l = 0 → m ≤ |L1| → - ∀L. ⬇[s, 0, m] L @@ L1 ≡ L @@ L2. + ∀L. ⬇[s, 0, m] L ;; L1 ≡ L ;; L2. #L1 #L2 #s #l #m #H elim H -L1 -L2 -l -m normalize [2,3,4: /4 width=1 by drop_skip_lt, drop_drop, arith_b1, lt_minus_to_plus_r, monotonic_pred/ ] #l #m #_ #_ #H <(le_n_O_to_eq … H) -H // qed-. lemma drop_O1_append_sn_le: ∀L1,L2,s,m. ⬇[s, 0, m] L1 ≡ L2 → m ≤ |L1| → - ∀L. ⬇[s, 0, m] L @@ L1 ≡ L @@ L2. + ∀L. ⬇[s, 0, m] L ;; L1 ≡ L ;; L2. /2 width=3 by drop_O1_append_sn_le_aux/ qed. (* Inversion lemmas on append for local environments ************************) -lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 @@ L2 ≡ K → +lemma drop_O1_inv_append1_ge: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ;; L2 ≡ K → |L2| ≤ m → ⬇[s, 0, m - |L2|] L1 ≡ K. #K #L1 #L2 elim L2 -L2 normalize // #L2 #I #V #IHL2 #s #m #H #H1m @@ -45,8 +45,8 @@ elim (drop_inv_O1_pair1 … H) -H * #H2m #HL12 destruct ] qed-. -lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 @@ L2 ≡ K → m ≤ |L2| → - ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 @@ K2. +lemma drop_O1_inv_append1_le: ∀K,L1,L2,s,m. ⬇[s, 0, m] L1 ;; L2 ≡ K → m ≤ |L2| → + ∀K2. ⬇[s, 0, m] L2 ≡ K2 → K = L1 ;; K2. #K #L1 #L2 elim L2 -L2 normalize [ #s #m #H1 #H2 #K2 #H3 lapply (le_n_O_to_eq … H2) -H2 #H2 elim (drop_inv_atom1 … H3) -H3 #H3 #_ destruct diff --git a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_vector.ma b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_vector.ma index d62669746..dabf85505 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_vector.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/substitution/lift_vector.ma @@ -18,7 +18,7 @@ include "basic_2A/substitution/lift.ma". (* BASIC TERM VECTOR RELOCATION *********************************************) inductive liftv (l,m:nat) : relation (list term) ≝ -| liftv_nil : liftv l m (Ⓔ) (Ⓔ) +| liftv_nil : liftv l m (ⓔ) (ⓔ) | liftv_cons: ∀T1s,T2s,T1,T2. ⬆[l, m] T1 ≡ T2 → liftv l m T1s T2s → liftv l m (T1 ⨮ T1s) (T2 ⨮ T2s) @@ -28,12 +28,12 @@ interpretation "relocation (vector)" 'RLift l m T1s T2s = (liftv l m T1s T2s). (* Basic inversion lemmas ***************************************************) -fact liftv_inv_nil1_aux: ∀T1s,T2s,l,m. ⬆[l, m] T1s ≡ T2s → T1s = Ⓔ → T2s = Ⓔ. +fact liftv_inv_nil1_aux: ∀T1s,T2s,l,m. ⬆[l, m] T1s ≡ T2s → T1s = ⓔ → T2s = ⓔ. #T1s #T2s #l #m * -T1s -T2s // #T1s #T2s #T1 #T2 #_ #_ #H destruct qed-. -lemma liftv_inv_nil1: ∀T2s,l,m. ⬆[l, m] Ⓔ ≡ T2s → T2s = Ⓔ. +lemma liftv_inv_nil1: ∀T2s,l,m. ⬆[l, m] ⓔ ≡ T2s → T2s = ⓔ. /2 width=5 by liftv_inv_nil1_aux/ qed-. fact liftv_inv_cons1_aux: ∀T1s,T2s,l,m. ⬆[l, m] T1s ≡ T2s → diff --git a/matita/matita/contribs/lambdadelta/basic_2A/unfold/unfold.ma b/matita/matita/contribs/lambdadelta/basic_2A/unfold/unfold.ma index 063d9c7bb..f949f5e39 100644 --- a/matita/matita/contribs/lambdadelta/basic_2A/unfold/unfold.ma +++ b/matita/matita/contribs/lambdadelta/basic_2A/unfold/unfold.ma @@ -24,7 +24,7 @@ inductive unfold: relation4 genv lenv term lenv ≝ | unfold_sort: ∀G,L,k. unfold G L (⋆k) L | unfold_lref: ∀I,G,L1,L2,K1,K2,V,i. ⬇[i] L1 ≡ K1. ⓑ{I}V → unfold G K1 V K2 → ⬇[Ⓣ, |L2|, i] L2 ≡ K2 → - unfold G L1 (#i) (L1@@L2) + unfold G L1 (#i) (L1;;L2) | unfold_bind: ∀a,I,G,L1,L2,V,T. unfold G (L1.ⓑ{I}V) T L2 → unfold G L1 (ⓑ{a,I}V.T) L2 | unfold_flat: ∀I,G,L1,L2,V,T. diff --git a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.ma b/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.ma deleted file mode 100644 index 09651c16c..000000000 --- a/matita/matita/contribs/lambdadelta/delayed_updating/notation/functions/element_e_0.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation "hvbox( 𝐞 )" - non associative with precedence 75 - for @{ 'ElementE }. diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list.ma b/matita/matita/contribs/lambdadelta/ground/lib/list.ma index 21a0f7560..6dc752d65 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/circledE_1.ma". +include "ground/notation/functions/circled_element_e_1.ma". include "ground/notation/functions/oplusright_3.ma". include "ground/lib/relations.ma". @@ -25,7 +25,7 @@ inductive list (A:Type[0]): Type[0] := interpretation "empty (lists)" - 'CircledE A = (list_empty A). + 'CircledElementE A = (list_empty A). interpretation "left cons (lists)" diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma index 2dcf8e576..13c68a33c 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_append.ma @@ -29,7 +29,7 @@ interpretation (* Basic constructions ******************************************************) lemma list_append_empty_sn (A): - ∀l2. l2 = Ⓔ ⨁{A} l2. + ∀l2. l2 = ⓔ ⨁{A} l2. // qed. lemma list_append_lcons_sn (A): @@ -39,7 +39,7 @@ lemma list_append_lcons_sn (A): (* Advanced constructions ***************************************************) lemma list_append_empty_dx (A): - ∀l1. l1 = l1 ⨁{A} Ⓔ. + ∀l1. l1 = l1 ⨁{A} ⓔ. #A #l1 elim l1 -l1 [ list_length_lcons #H elim (eq_inv_nsucc_zero … H) qed-. lemma list_length_inv_zero_sn (A:Type[0]) (l:list A): - (𝟎) = |l| → l = Ⓔ. + (𝟎) = |l| → l = ⓔ. /2 width=1 by list_length_inv_zero_dx/ qed-. lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x): diff --git a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma index 429a766fd..2cf2e23bf 100644 --- a/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma +++ b/matita/matita/contribs/lambdadelta/ground/lib/list_rcons.ma @@ -24,7 +24,7 @@ interpretation (* Basic constructions ******************************************************) lemma list_cons_comm (A): - ∀a. a ⨮ Ⓔ = Ⓔ ⨭{A} a. + ∀a. a ⨮ ⓔ = ⓔ ⨭{A} a. // qed. lemma list_cons_shift (A): diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma deleted file mode 100644 index 1d14afad7..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/append_2.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation "hvbox( l1 @@ break l2 )" - right associative with precedence 55 - for @{ 'Append $l1 $l2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma deleted file mode 100644 index 274a8c105..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/circledE_1.ma +++ /dev/null @@ -1,27 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation < "hvbox( Ⓔ )" - non associative with precedence 75 - for @{ 'CircledE $S }. - -notation > "hvbox( Ⓔ )" - non associative with precedence 75 - for @{ 'CircledE ? }. - -notation > "hvbox( Ⓔ{ term 46 C } )" - non associative with precedence 75 - for @{ 'CircledE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_1.ma new file mode 100644 index 000000000..92e92543b --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/circled_element_e_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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation < "hvbox( ⓔ )" + non associative with precedence 75 + for @{ 'CircledElementE $S }. + +notation > "hvbox( ⓔ )" + non associative with precedence 75 + for @{ 'CircledElementE ? }. + +notation > "hvbox( ⓔ{ term 46 C } )" + non associative with precedence 75 + for @{ 'CircledElementE $S }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma deleted file mode 100644 index 6c25a97c8..000000000 --- a/matita/matita/contribs/lambdadelta/ground/notation/functions/diamond_0.ma +++ /dev/null @@ -1,19 +0,0 @@ -(**************************************************************************) -(* ___ *) -(* ||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 *) -(* *) -(**************************************************************************) - -(* GROUND NOTATION **********************************************************) - -notation "◊" - non associative with precedence 75 - for @{ 'Diamond }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/double_semicolon_2.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/double_semicolon_2.ma new file mode 100644 index 000000000..92f5e0bf1 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/double_semicolon_2.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation "hvbox( l1 ;; break l2 )" + right associative with precedence 55 + for @{ 'DoubleSemicolon $l1 $l2 }. diff --git a/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma new file mode 100644 index 000000000..d890760a2 --- /dev/null +++ b/matita/matita/contribs/lambdadelta/ground/notation/functions/element_e_0.ma @@ -0,0 +1,19 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +(* GROUND NOTATION **********************************************************) + +notation "𝐞" + non associative with precedence 75 + for @{ 'ElementE }. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma index c2d7b9ed7..b50a5cfa8 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_append.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/append_2.ma". +include "ground/notation/functions/double_semicolon_2.ma". include "ground/relocation/fr2_map.ma". (* CONCATENATION FOR FINITE RELOCATION MAPS WITH PAIRS **********************) @@ -20,22 +20,22 @@ include "ground/relocation/fr2_map.ma". (* Note: this is compose *) (*** fr2_append *) rec definition fr2_append f1 f2 on f1 ≝ match f1 with -[ fr2_nil ⇒ f2 -| fr2_cons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2 +[ fr2_empty ⇒ f2 +| fr2_lcons d h f1 ⇒ ❨d, h❩; fr2_append f1 f2 ]. interpretation "append (finite relocation maps with pairs)" - 'Append f1 f2 = (fr2_append f1 f2). + 'DoubleSemicolon f1 f2 = (fr2_append f1 f2). (* Basic constructions ******************************************************) (*** mr2_append_nil *) -lemma fr2_append_nil (f2): - f2 = ◊ @@ f2. +lemma fr2_append_empty (f2): + f2 = 𝐞 ;; f2. // qed. (*** mr2_append_cons *) -lemma fr2_append_cons (d) (h) (f1) (f2): - ❨d, h❩; (f1 @@ f2) = (❨d, h❩; f1) @@ f2. +lemma fr2_append_lcons (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 3de9abeb3..a1f2f4d4e 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_map.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -include "ground/notation/functions/diamond_0.ma". +include "ground/notation/functions/element_e_0.ma". include "ground/notation/functions/semicolon_3.ma". include "ground/arith/nat.ma". @@ -21,14 +21,15 @@ include "ground/arith/nat.ma". (*** mr2 *) inductive fr2_map: Type[0] := (*** nil2 *) - | fr2_nil : fr2_map +| fr2_empty: fr2_map (*** cons2 *) - | fr2_cons: nat → nat → fr2_map → fr2_map. +| fr2_lcons: nat → nat → fr2_map → fr2_map +. interpretation - "nil (finite relocation maps with pairs)" - 'Diamond = (fr2_nil). + "empty (finite relocation maps with pairs)" + 'ElementE = (fr2_empty). interpretation - "cons (finite relocation maps with pairs)" - 'Semicolon d h f = (fr2_cons d h f). + "left cons (finite relocation maps with pairs)" + 'Semicolon 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 edc241fc0..d083a5df8 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_minus.ma @@ -24,8 +24,8 @@ include "ground/relocation/fr2_map.ma". (*** minuss *) inductive fr2_minus: nat → relation fr2_map ≝ (*** minuss_nil *) -| fr2_minus_nil (i): - fr2_minus i (◊) (◊) +| fr2_minus_empty (i): + 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) @@ -41,9 +41,9 @@ interpretation (* Basic inversions *********************************************************) (*** minuss_inv_nil1 *) -lemma fr2_minus_inv_nil_sn (f2) (i): - ◊ ▭ i ≘ f2 → f2 = ◊. -#f2 #i @(insert_eq_1 … (◊)) +lemma fr2_minus_inv_empty_sn (f2) (i): + 𝐞 ▭ i ≘ f2 → f2 = 𝐞. +#f2 #i @(insert_eq_1 … (𝐞)) #f1 * -f1 -f2 -i [ // | #f1 #f2 #d #h #i #_ #_ #H destruct @@ -52,7 +52,7 @@ lemma fr2_minus_inv_nil_sn (f2) (i): qed-. (*** minuss_inv_cons1 *) -lemma fr2_minus_inv_cons_sn (f1) (f2) (d) (h) (i): +lemma fr2_minus_inv_lcons_sn (f1) (f2) (d) (h) (i): ❨d, h❩;f1 ▭ i ≘ f2 → ∨∨ ∧∧ d ≤ i & f1 ▭ h+i ≘ f2 | ∃∃f. i < d & f1 ▭ i ≘ f & f2 = ❨d-i,h❩;f. @@ -65,18 +65,18 @@ lemma fr2_minus_inv_cons_sn (f1) (f2) (d) (h) (i): qed-. (*** minuss_inv_cons1_ge *) -lemma fr2_minus_inv_cons_sn_ge (f1) (f2) (d) (h) (i): +lemma fr2_minus_inv_lcons_sn_ge (f1) (f2) (d) (h) (i): ❨d, h❩;f1 ▭ i ≘ f2 → d ≤ i → f1 ▭ h+i ≘ f2. #f1 #f2 #d #h #i #H -elim (fr2_minus_inv_cons_sn … H) -H * // #f #Hid #_ #_ #Hdi +elim (fr2_minus_inv_lcons_sn … H) -H * // #f #Hid #_ #_ #Hdi elim (nlt_ge_false … Hid Hdi) qed-. (*** minuss_inv_cons1_lt *) -lemma fr2_minus_inv_cons_sn_lt (f1) (f2) (d) (h) (i): +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. -#f1 #f2 #d #h #i #H elim (fr2_minus_inv_cons_sn … H) -H * +#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 59dec1229..6b3d84f8a 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat.ma @@ -22,8 +22,8 @@ include "ground/relocation/fr2_map.ma". (*** at *) inductive fr2_nat: fr2_map → relation nat ≝ (*** at_nil *) -| fr2_nat_nil (l): - fr2_nat (◊) l l +| fr2_nat_empty (l): + 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 @@ -39,9 +39,9 @@ interpretation (* Basic inversions *********************************************************) (*** at_inv_nil *) -lemma fr2_nat_inv_nil (l1) (l2): - @❨l1, ◊❩ ≘ l2 → l1 = l2. -#l1 #l2 @(insert_eq_1 … (◊)) +lemma fr2_nat_inv_empty (l1) (l2): + @❨l1, 𝐞❩ ≘ l2 → l1 = l2. +#l1 #l2 @(insert_eq_1 … (𝐞)) #f * -f -l1 -l2 [ // | #f #d #h #l1 #l2 #_ #_ #H destruct @@ -50,7 +50,7 @@ lemma fr2_nat_inv_nil (l1) (l2): qed-. (*** at_inv_cons *) -lemma fr2_nat_inv_cons (f) (d) (h) (l1) (l2): +lemma fr2_nat_inv_lcons (f) (d) (h) (l1) (l2): @❨l1, ❨d,h❩;f❩ ≘ l2 → ∨∨ ∧∧ l1 < d & @❨l1, f❩ ≘ l2 | ∧∧ d ≤ l1 & @❨l1+h, f❩ ≘ l2. @@ -63,17 +63,17 @@ lemma fr2_nat_inv_cons (f) (d) (h) (l1) (l2): qed-. (*** at_inv_cons *) -lemma fr2_nat_inv_cons_lt (f) (d) (h) (l1) (l2): +lemma fr2_nat_inv_lcons_lt (f) (d) (h) (l1) (l2): @❨l1, ❨d,h❩;f❩ ≘ l2 → l1 < d → @❨l1, f❩ ≘ l2. #f #d #h #l1 #h2 #H -elim (fr2_nat_inv_cons … H) -H * // #Hdl1 #_ #Hl1d +elim (fr2_nat_inv_lcons … H) -H * // #Hdl1 #_ #Hl1d elim (nlt_ge_false … Hl1d Hdl1) qed-. (*** at_inv_cons *) -lemma fr2_nat_inv_cons_ge (f) (d) (h) (l1) (l2): +lemma fr2_nat_inv_lcons_ge (f) (d) (h) (l1) (l2): @❨l1, ❨d,h❩;f❩ ≘ l2 → d ≤ l1 → @❨l1+h, f❩ ≘ l2. #f #d #h #l1 #h2 #H -elim (fr2_nat_inv_cons … H) -H * // #Hl1d #_ #Hdl1 +elim (fr2_nat_inv_lcons … H) -H * // #Hl1d #_ #Hdl1 elim (nlt_ge_false … Hl1d Hdl1) qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma index 744becdad..b4033e80c 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_nat_nat.ma @@ -22,10 +22,10 @@ include "ground/relocation/fr2_nat.ma". theorem fr2_nat_mono (f) (l): ∀l1. @❨l, f❩ ≘ l1 → ∀l2. @❨l, f❩ ≘ l2 → l1 = l2. #f #l #l1 #H elim H -f -l -l1 -[ #l #x #H <(fr2_nat_inv_nil … H) -x // +[ #l #x #H <(fr2_nat_inv_empty … H) -x // | #f #d #h #l #l1 #Hld #_ #IH #x #H - lapply (fr2_nat_inv_cons_lt … H Hld) -H -Hld /2 width=1 by/ + lapply (fr2_nat_inv_lcons_lt … H Hld) -H -Hld /2 width=1 by/ | #f #d #h #l #l1 #Hdl #_ #IH #x #H - lapply (fr2_nat_inv_cons_ge … H Hdl) -H -Hdl /2 width=1 by/ + lapply (fr2_nat_inv_lcons_ge … H Hdl) -H -Hdl /2 width=1 by/ ] qed-. diff --git a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma index 459560035..cc36d81b2 100644 --- a/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma +++ b/matita/matita/contribs/lambdadelta/ground/relocation/fr2_plus.ma @@ -20,8 +20,8 @@ include "ground/relocation/fr2_map.ma". (* Note: this is pushs *) (*** pluss *) rec definition fr2_plus (f:fr2_map) (n:nat) on f ≝ match f with -[ fr2_nil ⇒ ◊ -| fr2_cons d h f ⇒ ❨d+n,h❩;fr2_plus f n +[ fr2_empty ⇒ 𝐞 +| fr2_lcons d h f ⇒ ❨d+n,h❩;fr2_plus f n ]. interpretation @@ -31,21 +31,21 @@ interpretation (* Basic constructions ******************************************************) (*** pluss_SO2 *) -lemma fr2_plus_cons_unit (d) (h) (f): +lemma fr2_plus_lcons_unit (d) (h) (f): ((❨d,h❩;f)+𝟏) = ❨↑d,h❩;f+𝟏. normalize // qed. (* Basic inversions *********************************************************) (*** pluss_inv_nil2 *) -lemma fr2_plus_inv_nil_dx (n) (f): - f+n = ◊ → f = ◊. +lemma fr2_plus_inv_empty_dx (n) (f): + f+n = 𝐞 → f = 𝐞. #n * // normalize #d #h #f #H destruct qed. (*** pluss_inv_cons2 *) -lemma fr2_plus_inv_cons_dx (n) (d) (h) (f2) (f): +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. #n #d #h #f2 * diff --git a/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl b/matita/matita/contribs/lambdadelta/ground/web/ground_src.tbl index be1cfadbb..edc2157eb 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" * } { @@ -133,7 +133,7 @@ table { [ { "lists" * } { [ "list_append ( ?⨁{?}? )" "list_rcons ( ?⨭{?}? )" * ] [ "list_length ( |?| )" * ] - [ "list ( Ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" * ] + [ "list ( ⓔ{?} ) ( ? ⨮{?} ? )" "list_eq" * ] } ] [ { "" * } { diff --git a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma index d0cd506bc..23d54010d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma +++ b/matita/matita/contribs/lambdadelta/static_2/relocation/lifts_vector.ma @@ -19,7 +19,7 @@ include "static_2/relocation/lifts.ma". (* Basic_2A1: includes: liftv_nil liftv_cons *) inductive liftsv (f): relation … ≝ -| 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) @@ -34,14 +34,14 @@ interpretation "uniform relocation (term vector)" (* Basic inversion lemmas ***************************************************) fact liftsv_inv_nil1_aux (f): - ∀X,Y. ⇧*[f] X ≘ Y → X = Ⓔ → Y = Ⓔ. + ∀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 = Ⓔ. + ∀Y. ⇧*[f] ⓔ ≘ Y → Y = ⓔ. /2 width=5 by liftsv_inv_nil1_aux/ qed-. fact liftsv_inv_cons1_aux (f): @@ -60,13 +60,13 @@ lemma liftsv_inv_cons1 (f): /2 width=3 by liftsv_inv_cons1_aux/ qed-. fact liftsv_inv_nil2_aux (f): - ∀X,Y. ⇧*[f] X ≘ Y → Y = Ⓔ → X = Ⓔ. + ∀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 = Ⓔ. + ∀X. ⇧*[f] X ≘ ⓔ → X = ⓔ. /2 width=5 by liftsv_inv_nil2_aux/ qed-. fact liftsv_inv_cons2_aux (f): diff --git a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma index 046343a06..f32e5c528 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_aaa.ma @@ -31,7 +31,7 @@ theorem acr_aaa_lsubc_lifts (RR) (RS) (RP): lapply (aaa_inv_sort … HA) -HA #H destruct >(lifts_inv_sort1 … H0) -H0 lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom - lapply (s2 … HAtom G L2 (Ⓔ)) /3 width=7 by cp1, simple_atom/ + lapply (s2 … HAtom G L2 (ⓔ)) /3 width=7 by cp1, simple_atom/ | #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_lsubc_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_lsubc_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_lsubc_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/static_2/static/gcp_cr.ma b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma index 52952ea3a..a1315531c 100644 --- a/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma +++ b/matita/matita/contribs/lambdadelta/static_2/static/gcp_cr.ma @@ -103,7 +103,7 @@ lemma acr_gcr: ∀RR,RS,RP. gcp RR RS RP → gcr RR RS RP RP → [ #G #L #T #H letin s ≝ 0 (* one sort must exist *) lapply (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 @@ -158,11 +158,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/static_2/syntax/term_vector.ma b/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma index 8be2b3ae7..16ca60c7d 100644 --- a/matita/matita/contribs/lambdadelta/static_2/syntax/term_vector.ma +++ b/matita/matita/contribs/lambdadelta/static_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.