<pippo in ⊢ (????%?); >(mf_comp … T) in ⊢ (????%?);
-[2: @@tm_vpush_vlift_join_O
+[2: ;;tm_vpush_vlift_join_O
<pippo in ⊢ (????%?);
[ #G #L #k #L0 #cs #HL0 #X #H #L2 #HL20
>(lifts_inv_sort1 … H) -H
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
- lapply (s4 â\80¦ HAtom G L2 (â\92º)) /2 width=1 by/
+ lapply (s4 â\80¦ HAtom G L2 (â\93\94)) /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
[ #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 â\80¦ HB ? G ? ? (â\92º) … HV0 HLK2) /3 width=7 by drops_cons, lifts_cons/ (* Note: uses IHB HL20 V2 HV0 *)
+ lapply (s5 â\80¦ HB ? G ? ? (â\93\94) … 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
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 â\80¦ HB ? G ? ? (â\92º) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
- lapply (s7 â\80¦ HB G L2 (â\92º)) /3 width=7 by gcr_lift/
+ lapply (s5 â\80¦ HB ? G ? ? (â\93\94) … (ⓝV3.V) … HLK2) /2 width=1 by lift_flat/
+ lapply (s7 â\80¦ HB G L2 (â\93\94)) /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 â\80¦ HA G L2 (â\92º) (â\92º)) /4 width=5 by lsubc_pair, drops_skip, liftv_nil/
+ lapply (s6 â\80¦ HA G L2 (â\93\94) (â\93\94)) /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
| #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 â\80¦ HA G L2 (â\92º)) /3 width=5 by/
+ lapply (s7 â\80¦ HA G L2 (â\93\94)) /3 width=5 by/
]
qed.
#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 â\80¦ IHB G L (â\92º) … HK) //
+ lapply (H L (⋆k) T (𝐞) ? ? ?) -H //
+ [ lapply (s2 â\80¦ IHB G L (â\93\94) … HK) //
| /3 width=6 by s1, cp3/
]
| #G #L #Vs #HVs #T #H1T #H2T #L0 #V0 #X #cs #HL0 #H #HB
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 â\80¦ HCA â\80¦ a G L0 (â\92º)) #H @H -H
-lapply (s6 â\80¦ HCA G L0 (â\92º) (â\92º) ?) // #H @H -H
+lapply (s3 â\80¦ HCA â\80¦ a G L0 (â\93\94)) #H @H -H
+lapply (s6 â\80¦ HCA G L0 (â\93\94) (â\93\94) ?) // #H @H -H
[ @(HA … HL0) //
| lapply (s1 … HCB) -HCB #HCB
- lapply (s7 â\80¦ H2RP G L0 (â\92º)) /3 width=1 by/
+ lapply (s7 â\80¦ H2RP G L0 (â\93\94)) /3 width=1 by/
]
qed.
(* *)
(**************************************************************************)
-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".
| 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.
#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.
(* 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/
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/
]
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-.
(* 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
.
(* 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 →
(* 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-.
(* 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
(* 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
]
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-.
(* 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
.
(* 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 →
(* 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.
(* GENERIC TERM VECTOR RELOCATION *******************************************)
inductive liftsv (cs:mr2) : relation (list term) ≝
-| liftsv_nil : liftsv cs (â\92º) (â\92º)
+| liftsv_nil : liftsv cs (â\93\94) (â\93\94)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⬆*[cs] T1 ≡ T2 → liftsv cs T1s T2s →
liftsv cs (T1 ⨮ T1s) (T2 ⨮ T2s)
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
]
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
(* BASIC TERM VECTOR RELOCATION *********************************************)
inductive liftv (l,m:nat) : relation (list term) ≝
-| liftv_nil : liftv l m (â\92º) (â\92º)
+| liftv_nil : liftv l m (â\93\94) (â\93\94)
| liftv_cons: ∀T1s,T2s,T1,T2.
⬆[l, m] T1 ≡ T2 → liftv l m T1s T2s →
liftv l m (T1 ⨮ T1s) (T2 ⨮ T2s)
(* Basic inversion lemmas ***************************************************)
-fact liftv_inv_nil1_aux: â\88\80T1s,T2s,l,m. â¬\86[l, m] T1s â\89¡ T2s â\86\92 T1s = â\92º â\86\92 T2s = â\92º.
+fact liftv_inv_nil1_aux: â\88\80T1s,T2s,l,m. â¬\86[l, m] T1s â\89¡ T2s â\86\92 T1s = â\93\94 â\86\92 T2s = â\93\94.
#T1s #T2s #l #m * -T1s -T2s //
#T1s #T2s #T1 #T2 #_ #_ #H destruct
qed-.
-lemma liftv_inv_nil1: â\88\80T2s,l,m. â¬\86[l, m] â\92º â\89¡ T2s â\86\92 T2s = â\92º.
+lemma liftv_inv_nil1: â\88\80T2s,l,m. â¬\86[l, m] â\93\94 â\89¡ T2s â\86\92 T2s = â\93\94.
/2 width=5 by liftv_inv_nil1_aux/ qed-.
fact liftv_inv_cons1_aux: ∀T1s,T2s,l,m. ⬆[l, m] T1s ≡ T2s →
| 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.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
(* *)
(**************************************************************************)
-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".
interpretation
"empty (lists)"
- 'CircledE A = (list_empty A).
+ 'CircledElementE A = (list_empty A).
interpretation
"left cons (lists)"
(* Basic constructions ******************************************************)
lemma list_append_empty_sn (A):
- â\88\80l2. l2 = â\92º ⨁{A} l2.
+ â\88\80l2. l2 = â\93\94 ⨁{A} l2.
// qed.
lemma list_append_lcons_sn (A):
(* Advanced constructions ***************************************************)
lemma list_append_empty_dx (A):
- â\88\80l1. l1 = l1 â¨\81{A} â\92º.
+ â\88\80l1. l1 = l1 â¨\81{A} â\93\94.
#A #l1 elim l1 -l1
[ <list_append_empty_sn //
| #hd #tl #IH <list_append_lcons_sn <IH //
(* Basic inversions *********************************************************)
lemma list_length_inv_zero_dx (A:Type[0]) (l:list A):
- |l| = ð\9d\9f\8e â\86\92 l = â\92º.
+ |l| = ð\9d\9f\8e â\86\92 l = â\93\94.
#A * // #a #l >list_length_lcons #H
elim (eq_inv_nsucc_zero … H)
qed-.
lemma list_length_inv_zero_sn (A:Type[0]) (l:list A):
- (ð\9d\9f\8e) = |l| â\86\92 l = â\92º.
+ (ð\9d\9f\8e) = |l| â\86\92 l = â\93\94.
/2 width=1 by list_length_inv_zero_dx/ qed-.
lemma list_length_inv_succ_dx (A:Type[0]) (l:list A) (x):
(* Basic constructions ******************************************************)
lemma list_cons_comm (A):
- â\88\80a. a ⨮ â\92º = â\92º ⨭{A} a.
+ â\88\80a. a ⨮ â\93\94 = â\93\94 ⨭{A} a.
// qed.
lemma list_cons_shift (A):
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||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 }.
(* *)
(**************************************************************************)
-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 **********************)
(* 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.
(* *)
(**************************************************************************)
-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".
(*** 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).
(*** 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)
(* 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
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.
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/
]
(*** 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
(* 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
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.
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-.
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-.
(* 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
(* 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 *
[ { "finite relocation with pairs" * } {
[ "fr2_nat ( @❨?,?❩ ≘ ? )" "fr2_nat_nat" * ]
[ "fr2_minus ( ? ▭ ? ≘ ? )" * ]
- [ "fr2_append ( ?@@? )" * ]
+ [ "fr2_append ( ?;;? )" * ]
[ "fr2_plus ( ?+? )" * ]
- [ "fr2_map ( ◊ ) ( ❨?,?❩;? )" * ]
+ [ "fr2_map ( 𝐞 ) ( ❨?,?❩;? )" * ]
}
]
[ { "total relocation" * } {
[ { "lists" * } {
[ "list_append ( ?⨁{?}? )" "list_rcons ( ?⨭{?}? )" * ]
[ "list_length ( |?| )" * ]
- [ "list ( â\92º{?} ) ( ? ⨮{?} ? )" "list_eq" * ]
+ [ "list ( â\93\94{?} ) ( ? ⨮{?} ? )" "list_eq" * ]
}
]
[ { "" * } {
(* Basic_2A1: includes: liftv_nil liftv_cons *)
inductive liftsv (f): relation … ≝
-| liftsv_nil : liftsv f (â\92º) (â\92º)
+| liftsv_nil : liftsv f (â\93\94) (â\93\94)
| liftsv_cons: ∀T1s,T2s,T1,T2.
⇧*[f] T1 ≘ T2 → liftsv f T1s T2s →
liftsv f (T1 ⨮ T1s) (T2 ⨮ T2s)
(* Basic inversion lemmas ***************************************************)
fact liftsv_inv_nil1_aux (f):
- â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 X = â\92º â\86\92 Y = â\92º.
+ â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 X = â\93\94 â\86\92 Y = â\93\94.
#f #X #Y * -X -Y //
#T1s #T2s #T1 #T2 #_ #_ #H destruct
qed-.
(* Basic_2A1: includes: liftv_inv_nil1 *)
lemma liftsv_inv_nil1 (f):
- â\88\80Y. â\87§*[f] â\92º â\89\98 Y â\86\92 Y = â\92º.
+ â\88\80Y. â\87§*[f] â\93\94 â\89\98 Y â\86\92 Y = â\93\94.
/2 width=5 by liftsv_inv_nil1_aux/ qed-.
fact liftsv_inv_cons1_aux (f):
/2 width=3 by liftsv_inv_cons1_aux/ qed-.
fact liftsv_inv_nil2_aux (f):
- â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 Y = â\92º â\86\92 X = â\92º.
+ â\88\80X,Y. â\87§*[f] X â\89\98 Y â\86\92 Y = â\93\94 â\86\92 X = â\93\94.
#f #X #Y * -X -Y //
#T1s #T2s #T1 #T2 #_ #_ #H destruct
qed-.
lemma liftsv_inv_nil2 (f):
- â\88\80X. â\87§*[f] X â\89\98 â\92º â\86\92 X = â\92º.
+ â\88\80X. â\87§*[f] X â\89\98 â\93\94 â\86\92 X = â\93\94.
/2 width=5 by liftsv_inv_nil2_aux/ qed-.
fact liftsv_inv_cons2_aux (f):
lapply (aaa_inv_sort … HA) -HA #H destruct
>(lifts_inv_sort1 … H0) -H0
lapply (acr_gcr … H1RP H2RP (⓪)) #HAtom
- lapply (s2 â\80¦ HAtom G L2 (â\92º)) /3 width=7 by cp1, simple_atom/
+ lapply (s2 â\80¦ HAtom G L2 (â\93\94)) /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
elim (lsubc_inv_bind2 … H) -H *
[ #K2 #HK20 #H destruct
lapply (drops_isuni_fwd_drop2 … HLK2) // #HLK2b
- lapply (s5 â\80¦ HA ? G ? ? (â\92º) … HV0 ?) -HA
+ lapply (s5 â\80¦ HA ? G ? ? (â\93\94) … 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 â\80¦ HA â\80¦ G â\80¦ (â\92º) … (ⓝW2.V2) (ⓝV.V3) ????)
+ lapply (s5 â\80¦ HA â\80¦ G â\80¦ (â\93\94) … (ⓝW2.V2) (ⓝV.V3) ????)
[3: |*: /2 width=9 by drops_inv_gen, lifts_flat/ ] -HLK2
- lapply (s7 â\80¦ HA G L2 (â\92º)) -HA /3 width=7 by acr_lifts/
+ lapply (s7 â\80¦ HA G L2 (â\93\94)) -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)
lapply (acr_gcr … H1RP H2RP A) #HA
lapply (acr_gcr … H1RP H2RP B) #HB
lapply (s1 … HB) -HB #HB
- lapply (s6 â\80¦ HA G L2 (â\92º) (â\92º)) /5 width=10 by lsubc_bind, liftsv_nil, drops_skip, ext2_pair/
+ lapply (s6 â\80¦ HA G L2 (â\93\94) (â\93\94)) /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
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 â\80¦ HA G L2 (â\92º)) /3 width=10 by/
+ lapply (s7 â\80¦ HA G L2 (â\93\94)) /3 width=10 by/
]
qed.
[ #G #L #T #H
letin s ≝ 0 (* one sort must exist *)
lapply (cp1 … H1RP G L s) #HK
- lapply (s2 â\80¦ IHB G L (â\92º) … HK) // #HB
+ lapply (s2 â\80¦ IHB G L (â\93\94) … 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
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 â\80¦ HCA â\80¦ p G L0 (â\92º)) #H @H -H
-lapply (s6 â\80¦ HCA G L0 (â\92º) (â\92º) ?) // #H @H -H
+lapply (s3 â\80¦ HCA â\80¦ p G L0 (â\93\94)) #H @H -H
+lapply (s6 â\80¦ HCA G L0 (â\93\94) (â\93\94) ?) // #H @H -H
[ @(HA … HL0) //
| lapply (s1 … HCB) -HCB #HCB
- lapply (s7 â\80¦ H2RP G L0 (â\92º)) /3 width=1 by/
+ lapply (s7 â\80¦ H2RP G L0 (â\93\94)) /3 width=1 by/
]
qed.
(* Basic properties *********************************************************)
-lemma applv_nil: â\88\80T. â\92¶â\92º.T = T.
+lemma applv_nil: â\88\80T. â\92¶â\93\94.T = T.
// qed.
lemma applv_cons: ∀V,Vs,T. ⒶV⨮Vs.T = ⓐV.ⒶVs.T.
projects / helm.git / commitdiff