Skip to content

Turn binary ++⁺ and related operators infix. #918

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
wants to merge 2 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
23 changes: 16 additions & 7 deletions src/Data/List/Base.agda
Original file line number Diff line number Diff line change
Expand Up @@ -308,18 +308,17 @@ _─_ : (xs : List A) → Fin (length xs) → List A
------------------------------------------------------------------------
-- Operations for reversing lists

reverseAcc : List A → List A → List A
reverseAcc = foldl (flip _∷_)

reverse : List A → List A
reverse = reverseAcc []

-- "Reverse append" xs ʳ++ ys = reverse xs ++ ys

infixr 5 _ʳ++_

_ʳ++_ : List A → List A → List A
_ʳ++_ = flip reverseAcc
xs ʳ++ ys = foldl (flip _∷_) ys xs

-- Reverse.

reverse : List A → List A
reverse = _ʳ++ []

-- Snoc.

Expand Down Expand Up @@ -390,3 +389,13 @@ boolSpan p (x ∷ xs) with p x

boolBreak : (A → Bool) → List A → (List A × List A)
boolBreak p = boolSpan (not ∘ p)

-- Version 1.2

reverseAcc : List A → List A → List A
reverseAcc = foldl (flip _∷_)

{-# WARNING_ON_USAGE reverseAcc
"Warning: reverseAcc was deprecated in v1.2.
Please use _ʳ++_ instead."
#-}
6 changes: 4 additions & 2 deletions src/Data/List/Membership/Propositional/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -103,8 +103,10 @@ module _ {v : A} where
∈-++⁺ˡ : ∀ {xs ys} → v ∈ xs → v ∈ xs ++ ys
∈-++⁺ˡ = Membershipₛ.∈-++⁺ˡ (P.setoid A)

∈-++⁺ʳ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
∈-++⁺ʳ = Membershipₛ.∈-++⁺ʳ (P.setoid A)
infixr 5 _∈-++⁺ʳ_

_∈-++⁺ʳ_ : ∀ xs {ys} → v ∈ ys → v ∈ xs ++ ys
_∈-++⁺ʳ_ = Membershipₛ._∈-++⁺ʳ_ (P.setoid A)

∈-++⁻ : ∀ xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
∈-++⁻ = Membershipₛ.∈-++⁻ (P.setoid A)
Expand Down
6 changes: 4 additions & 2 deletions src/Data/List/Membership/Setoid/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -149,8 +149,10 @@ module _ {c ℓ} (S : Setoid c ℓ) where
∈-++⁺ˡ : ∀ {v xs ys} → v ∈ xs → v ∈ xs ++ ys
∈-++⁺ˡ = Any.++⁺ˡ

∈-++⁺ʳ : ∀ {v} xs {ys} → v ∈ ys → v ∈ xs ++ ys
∈-++⁺ʳ = Any.++⁺ʳ
infixr 5 _∈-++⁺ʳ_

_∈-++⁺ʳ_ : ∀ {v} xs {ys} → v ∈ ys → v ∈ xs ++ ys
_∈-++⁺ʳ_ = Any._++⁺ʳ_

∈-++⁻ : ∀ {v} xs {ys} → v ∈ xs ++ ys → (v ∈ xs) ⊎ (v ∈ ys)
∈-++⁻ = Any.++⁻
Expand Down
11 changes: 7 additions & 4 deletions src/Data/List/Relation/Binary/BagAndSetEquality.agda
Original file line number Diff line number Diff line change
Expand Up @@ -145,9 +145,12 @@ module _ {ℓ k} {A B : Set ℓ} {f g : A → B} {xs ys} where

module _ {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} where

++-cong : xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
++-cong xs₁≈xs₂ ys₁≈ys₂ {x} =
infixr 5 _++-cong_

_++-cong_ : xs₁ ∼[ k ] xs₂ →
ys₁ ∼[ k ] ys₂ →
xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
_++-cong_ xs₁≈xs₂ ys₁≈ys₂ {x} =
x ∈ xs₁ ++ ys₁ ↔⟨ SK-sym $ ++↔ ⟩
(x ∈ xs₁ ⊎ x ∈ ys₁) ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ ⟩
(x ∈ xs₂ ⊎ x ∈ ys₂) ↔⟨ ++↔ ⟩
Expand Down Expand Up @@ -220,7 +223,7 @@ commutativeMonoid {a} k A = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = Eq.isEquivalence
; ∙-cong = ++-cong
; ∙-cong = _++-cong_
}
; assoc = λ xs ys zs →
Eq.reflexive (LP.++-assoc xs ys zs)
Expand Down
12 changes: 8 additions & 4 deletions src/Data/List/Relation/Binary/Equality/Setoid.agda
Original file line number Diff line number Diff line change
Expand Up @@ -85,8 +85,10 @@ module _ {b ℓ₂} (T : Setoid b ℓ₂) where
------------------------------------------------------------------------
-- _++_

++⁺ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
++⁺ = PW.++⁺
infixr 5 _++⁺_

_++⁺_ : ∀ {ws xs ys zs} → ws ≋ xs → ys ≋ zs → ws ++ ys ≋ xs ++ zs
_++⁺_ = PW._++⁺_

++-cancelˡ : ∀ xs {ys zs} → xs ++ ys ≋ xs ++ zs → ys ≋ zs
++-cancelˡ = PW.++-cancelˡ
Expand Down Expand Up @@ -123,8 +125,10 @@ module _ {P : Pred A p} (P? : U.Decidable P) (resp : P Respects _≈_)
------------------------------------------------------------------------
-- reverse

ʳ++⁺ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
ʳ++⁺ = PW.ʳ++⁺
infixr 5 _ʳ++⁺_

_ʳ++⁺_ : ∀{xs xs′ ys ys′} → xs ≋ xs′ → ys ≋ ys′ → xs ʳ++ ys ≋ xs′ ʳ++ ys′
_ʳ++⁺_ = PW._ʳ++⁺_

reverse⁺ : ∀ {xs ys} → xs ≋ ys → reverse xs ≋ reverse ys
reverse⁺ = PW.reverse⁺
Original file line number Diff line number Diff line change
Expand Up @@ -82,28 +82,36 @@ module _ {a b} {A : Set a} {B : Set b} (f : A → B) where

module _ {a} {A : Set a} where

infixr 5 _++⁺ˡ_ _++⁺ʳ_

++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
++⁺ˡ [] ys↭zs = ys↭zs
++⁺ˡ (x ∷ xs) ys↭zs = prep x (++⁺ˡ xs ys↭zs)
_++⁺ˡ_ : ∀ xs {ys zs : List A} →
ys ↭ zs →
xs ++ ys ↭ xs ++ zs
[] ++⁺ˡ ys↭zs = ys↭zs
(x ∷ xs) ++⁺ˡ ys↭zs = prep x (xs ++⁺ˡ ys↭zs)

++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
++⁺ʳ zs refl = refl
++⁺ʳ zs (prep x ↭) = prep x (++⁺ʳ zs ↭)
++⁺ʳ zs (swap x y ↭) = swap x y (++⁺ʳ zs ↭)
++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
_++⁺ʳ_ : ∀ {xs ys : List A} →
xs ↭ ys →
∀ zs →
xs ++ zs ↭ ys ++ zs
refl ++⁺ʳ zs = refl
prep x ↭ ++⁺ʳ zs = prep x (↭ ++⁺ʳ zs)
swap x y ↭ ++⁺ʳ zs = swap x y (↭ ++⁺ʳ zs)
trans ↭₁ ↭₂ ++⁺ʳ zs = trans (↭₁ ++⁺ʳ zs) (↭₂ ++⁺ʳ zs)

++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
infixr 5 _++⁺_

_++⁺_ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
ws↭xs ++⁺ ys↭zs = trans (ws↭xs ++⁺ʳ _) (_ ++⁺ˡ ys↭zs)

-- Some useful lemmas

zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
zoom h {t} = (h ++⁺ˡ_) ∘ (_++⁺ʳ t)

inject : ∀ (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep v xs↭zs)) (++⁺ʳ _ ws↭ys)
inject v ws↭ys xs↭zs = trans (_ ++⁺ˡ prep v xs↭zs) (ws↭ys ++⁺ʳ _)

shift : ∀ v (xs ys : List A) → xs ++ [ v ] ++ ys ↭ v ∷ xs ++ ys
shift v [] ys = refl
Expand Down Expand Up @@ -183,15 +191,15 @@ module _ {a} {A : Set a} where
++-comm (x ∷ xs) ys = begin
x ∷ xs ++ ys ↭⟨ prep x (++-comm xs ys) ⟩
x ∷ ys ++ xs ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
(x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (shift x ys []))
(x ∷ ys ++ []) ++ xs ↭⟨ ↭-sym (shift x ys []) ++⁺ʳ xs
(ys ++ [ x ]) ++ xs ↭⟨ ++-assoc ys [ x ] xs ⟩
ys ++ ([ x ] ++ xs) ≡⟨⟩
ys ++ (x ∷ xs) ∎

++-isMagma : IsMagma _↭_ _++_
++-isMagma = record
{ isEquivalence = ↭-isEquivalence
; ∙-cong = ++⁺
; ∙-cong = _++⁺_
}

++-magma : Magma _ _
Expand Down Expand Up @@ -238,7 +246,7 @@ module _ {a} {A : Set a} where
shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
shifts xs ys {zs} = begin
xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩
(xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys)
(xs ++ ys) ++ zs ↭⟨ ++-comm xs ys ++⁺ʳ zs
(ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
ys ++ xs ++ zs ∎

Expand Down
32 changes: 17 additions & 15 deletions src/Data/List/Relation/Binary/Permutation/Setoid/Properties.agda
Original file line number Diff line number Diff line change
Expand Up @@ -138,18 +138,20 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
x ∷ w ∷ xs ++ ys <<⟨ refl ⟩
w ∷ x ∷ xs ++ ys ∎

++⁺ˡ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
++⁺ˡ [] ys↭zs = ys↭zs
++⁺ˡ (x ∷ xs) ys↭zs = prep ≈-refl (++⁺ˡ xs ys↭zs)
infixr 5 _++⁺ˡ_ _++⁺ʳ_ _++⁺_

++⁺ʳ : ∀ {xs ys : List A} zs → xs ↭ ys → xs ++ zs ↭ ys ++ zs
++⁺ʳ zs refl = refl
++⁺ʳ zs (prep x ↭) = prep x (++⁺ʳ zs ↭)
++⁺ʳ zs (swap x y ↭) = swap x y (++⁺ʳ zs ↭)
++⁺ʳ zs (trans ↭₁ ↭₂) = trans (++⁺ʳ zs ↭₁) (++⁺ʳ zs ↭₂)
_++⁺ˡ_ : ∀ xs {ys zs : List A} → ys ↭ zs → xs ++ ys ↭ xs ++ zs
[] ++⁺ˡ ys↭zs = ys↭zs
(x ∷ xs) ++⁺ˡ ys↭zs = prep ≈-refl (xs ++⁺ˡ ys↭zs)

++⁺ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
++⁺ ws↭xs ys↭zs = trans (++⁺ʳ _ ws↭xs) (++⁺ˡ _ ys↭zs)
_++⁺ʳ_ : ∀ {xs ys : List A} → xs ↭ ys → ∀ zs → xs ++ zs ↭ ys ++ zs
refl ++⁺ʳ zs = refl
prep x ↭ ++⁺ʳ zs = prep x (↭ ++⁺ʳ zs)
swap x y ↭ ++⁺ʳ zs = swap x y (↭ ++⁺ʳ zs)
trans ↭₁ ↭₂ ++⁺ʳ zs = trans (↭₁ ++⁺ʳ zs) (↭₂ ++⁺ʳ zs)

_++⁺_ : _++_ Preserves₂ _↭_ ⟶ _↭_ ⟶ _↭_
ws↭xs ++⁺ ys↭zs = trans (ws↭xs ++⁺ʳ _ ) (_ ++⁺ˡ ys↭zs)

-- Algebraic properties

Expand All @@ -170,7 +172,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
++-comm (x ∷ xs) ys = begin
x ∷ xs ++ ys ↭⟨ prep ≈-refl (++-comm xs ys) ⟩
x ∷ ys ++ xs ≡⟨ cong (λ v → x ∷ v ++ xs) (≡.sym (Lₚ.++-identityʳ _)) ⟩
(x ∷ ys ++ []) ++ xs ↭⟨ ++⁺ʳ xs (↭-sym (shift ≈-refl ys []))
(x ∷ ys ++ []) ++ xs ↭⟨ ↭-sym (shift ≈-refl ys []) ++⁺ʳ xs
(ys ++ [ x ]) ++ xs ↭⟨ ++-assoc ys [ x ] xs ⟩
ys ++ ([ x ] ++ xs) ≡⟨⟩
ys ++ (x ∷ xs) ∎
Expand All @@ -180,7 +182,7 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
++-isMagma : IsMagma _↭_ _++_
++-isMagma = record
{ isEquivalence = ↭-isEquivalence
; ∙-cong = ++⁺
; ∙-cong = _++⁺_
}

++-isSemigroup : IsSemigroup _↭_ _++_
Expand Down Expand Up @@ -227,16 +229,16 @@ shift {v} {w} v≈w (x ∷ xs) ys = begin
-- Some other useful lemmas

zoom : ∀ h {t xs ys : List A} → xs ↭ ys → h ++ xs ++ t ↭ h ++ ys ++ t
zoom h {t} = ++⁺ˡ h ∘ ++⁺ʳ t
zoom h {t} = (h ++⁺ˡ_) ∘ (_++⁺ʳ t)

inject : ∀ (v : A) {ws xs ys zs} → ws ↭ ys → xs ↭ zs →
ws ++ [ v ] ++ xs ↭ ys ++ [ v ] ++ zs
inject v ws↭ys xs↭zs = trans (++⁺ˡ _ (prep ≈-refl xs↭zs)) (++⁺ʳ _ ws↭ys)
inject v ws↭ys xs↭zs = trans (_ ++⁺ˡ prep ≈-refl xs↭zs) (ws↭ys ++⁺ʳ _)

shifts : ∀ xs ys {zs : List A} → xs ++ ys ++ zs ↭ ys ++ xs ++ zs
shifts xs ys {zs} = begin
xs ++ ys ++ zs ↭˘⟨ ++-assoc xs ys zs ⟩
(xs ++ ys) ++ zs ↭⟨ ++⁺ʳ zs (++-comm xs ys)
(xs ++ ys) ++ zs ↭⟨ ++-comm xs ys ++⁺ʳ zs
(ys ++ xs) ++ zs ↭⟨ ++-assoc ys xs zs ⟩
ys ++ xs ++ zs ∎

Expand Down
42 changes: 29 additions & 13 deletions src/Data/List/Relation/Binary/Pointwise.agda
Original file line number Diff line number Diff line change
Expand Up @@ -203,10 +203,14 @@ module _ {_∼_ : REL A B ℓ} where

module _ {_∼_ : REL A B ℓ} where

++⁺ : ∀ {ws xs ys zs} → Pointwise _∼_ ws xs → Pointwise _∼_ ys zs →
Pointwise _∼_ (ws ++ ys) (xs ++ zs)
++⁺ [] ys∼zs = ys∼zs
++⁺ (w∼x ∷ ws∼xs) ys∼zs = w∼x ∷ ++⁺ ws∼xs ys∼zs
infixr 5 _++⁺_

_++⁺_ : ∀ {ws xs ys zs} →
Pointwise _∼_ ws xs →
Pointwise _∼_ ys zs →
Pointwise _∼_ (ws ++ ys) (xs ++ zs)
[] ++⁺ ys∼zs = ys∼zs
(w∼x ∷ ws∼xs) ++⁺ ys∼zs = w∼x ∷ ws∼xs ++⁺ ys∼zs

module _ {_∼_ : Rel₂ A ℓ} where

Expand All @@ -228,29 +232,28 @@ module _ {_∼_ : Rel₂ A ℓ} where

module _ {_∼_ : REL A B ℓ} where

concat⁺ : ∀ {xss yss} → Pointwise (Pointwise _∼_) xss yss →
concat⁺ : ∀ {xss yss} →
Pointwise (Pointwise _∼_) xss yss →
Pointwise _∼_ (concat xss) (concat yss)
concat⁺ [] = []
concat⁺ (xs∼ys ∷ xss∼yss) = ++⁺ xs∼ys (concat⁺ xss∼yss)
concat⁺ (xs∼ys ∷ xss∼yss) = xs∼ys ++⁺ concat⁺ xss∼yss

------------------------------------------------------------------------
-- reverse

module _ {R : REL A B ℓ} where

reverseAcc⁺ : ∀ {as bs as′ bs′} → Pointwise R as′ bs′ → Pointwise R as bs →
Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs)
reverseAcc⁺ rs′ [] = rs′
reverseAcc⁺ rs′ (r ∷ rs) = reverseAcc⁺ (r ∷ rs′) rs
infixr 5 _ʳ++⁺_

ʳ++⁺ : ∀ {as bs as′ bs′} →
++⁺_ : ∀ {as bs as′ bs′} →
Pointwise R as bs →
Pointwise R as′ bs′ →
Pointwise R (as ʳ++ as′) (bs ʳ++ bs′)
ʳ++⁺ rs rs′ = reverseAcc⁺ rs′ rs
[] ʳ++⁺ rs′ = rs′
(r ∷ rs) ʳ++⁺ rs′ = rs ʳ++⁺ (r ∷ rs′)

reverse⁺ : ∀ {as bs} → Pointwise R as bs → Pointwise R (reverse as) (reverse bs)
reverse⁺ = reverseAcc⁺ []
reverse⁺ = _ʳ++⁺ []

------------------------------------------------------------------------
-- map
Expand Down Expand Up @@ -364,3 +367,16 @@ decidable-≡ = ≡-dec
"Warning: decidable-≡ was deprecated in v1.0.
Please use ≡-dec from `Data.List.Properties` instead."
#-}

-- Version 1.2

reverseAcc⁺ : ∀ {R : REL A B ℓ} {as bs as′ bs′} →
Pointwise R as′ bs′ →
Pointwise R as bs →
Pointwise R (as ʳ++ as′) (bs ʳ++ bs′) -- Pointwise R (reverseAcc as′ as) (reverseAcc bs′ bs)
reverseAcc⁺ rs′ = _ʳ++⁺ rs′

{-# WARNING_ON_USAGE reverseAcc⁺
"Warning: reverseAcc⁺ was deprecated in v1.2.
Please use _ʳ++⁺_ instead."
#-}
Original file line number Diff line number Diff line change
Expand Up @@ -69,10 +69,14 @@ module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

module _ {a b r} {A : Set a} {B : Set b} {R : REL A B r} where

++⁺ : ∀ {as bs cs ds} → Pointwise R as bs →
Prefix R cs ds → Prefix R (as ++ cs) (bs ++ ds)
++⁺ [] cs⊆ds = cs⊆ds
++⁺ (r ∷ rs) cs⊆ds = r ∷ (++⁺ rs cs⊆ds)
infixr 5 _++⁺_

_++⁺_ : ∀ {as bs cs ds} →
Pointwise R as bs →
Prefix R cs ds →
Prefix R (as ++ cs) (bs ++ ds)
[] ++⁺ cs⊆ds = cs⊆ds
(r ∷ rs) ++⁺ cs⊆ds = r ∷ (rs ++⁺ cs⊆ds)

++⁻ : ∀ {as bs cs ds} → length as ≡ length bs →
Prefix R (as ++ cs) (bs ++ ds) → Prefix R cs ds
Expand Down
Loading