Skip to content

Improve Data.List.Base (fix #2359; deprecate use of with #2123) #2365

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.

Sign up for GitHub

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

Merged
merged 4 commits into from
Apr 22, 2024
Merged

Improve Data.List.Base (fix #2359; deprecate use of with #2123) #2365

Show file tree
Hide file tree
Changes from 2 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
c4916a3
refactor towards `if_then_else_` and away from `yes`/`no`
jamesmckinna Apr 15, 2024
76afe8a
reverted chnages to `derun` proofs
jamesmckinna Apr 17, 2024
5ae64d3
undo last reversion!
jamesmckinna Apr 17, 2024
f6673bd
layout
jamesmckinna Apr 22, 2024
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
31 changes: 11 additions & 20 deletions src/Data/List/Base.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -369,45 +369,37 @@ removeAt (x ∷ xs) (suc i) = x ∷ removeAt xs i

takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
takeWhile P? [] = []
takeWhile P? (x ∷ xs) with does (P? x)
... | true = x ∷ takeWhile P? xs
... | false = []
takeWhile P? (x ∷ xs) = if does (P? x) then x ∷ takeWhile P? xs else []

takeWhileᵇ : (A → Bool) → List A → List A
takeWhileᵇ p = takeWhile (T? ∘ p)

dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
dropWhile P? [] = []
dropWhile P? (x ∷ xs) with does (P? x)
... | true = dropWhile P? xs
... | false = x ∷ xs
dropWhile P? (x ∷ xs) = if does (P? x) then dropWhile P? xs else x ∷ xs

dropWhileᵇ : (A → Bool) → List A → List A
dropWhileᵇ p = dropWhile (T? ∘ p)

filter : ∀ {P : Pred A p} → Decidable P → List A → List A
filter P? [] = []
filter P? (x ∷ xs) with does (P? x)
... | false = filter P? xs
... | true = x ∷ filter P? xs
filter P? (x ∷ xs) = let xs′ = filter P? xs
in if does (P? x) then x ∷ xs′ else xs′

filterᵇ : (A → Bool) → List A → List A
filterᵇ p = filter (T? ∘ p)

partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
partition P? [] = ([] , [])
partition P? (x ∷ xs) with does (P? x) | partition P? xs
... | true | (ys , zs) = (x ∷ ys , zs)
... | false | (ys , zs) = (ys , x ∷ zs)
partition P? [] = [] , []
partition P? (x ∷ xs) = let ys , zs = partition P? xs
in if does (P? x) then (x ∷ ys , zs) else (ys , x ∷ zs)

partitionᵇ : (A → Bool) → List A → List A × List A
partitionᵇ p = partition (T? ∘ p)

span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
span P? [] = ([] , [])
span P? ys@(x ∷ xs) with does (P? x)
... | true = Product.map (x ∷_) id (span P? xs)
... | false = ([] , ys)
span P? [] = [] , []
span P? ys@(x ∷ xs) = if does (P? x) then Product.map (x ∷_) id (span P? xs) else ([] , ys)


spanᵇ : (A → Bool) → List A → List A × List A
Expand Down Expand Up @@ -458,9 +450,8 @@ wordsByᵇ p = wordsBy (T? ∘ p)
derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A
derun R? [] = []
derun R? (x ∷ []) = x ∷ []
derun R? (x ∷ xs@(y ∷ _)) with does (R? x y) | derun R? xs
... | true | ys = ys
... | false | ys = x ∷ ys
derun R? (x ∷ xs@(y ∷ _)) = let ys = derun R? xs
in if does (R? x y) then ys else x ∷ ys

derunᵇ : (A → A → Bool) → List A → List A
derunᵇ r = derun (T? ∘₂ r)
Expand Down
22 changes: 11 additions & 11 deletions src/Data/List/Properties.agda
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -943,13 +943,13 @@ module _ {P : Pred A p} (P? : Decidable P) where
filter-all : ∀ {xs} → All P xs → filter P? xs ≡ xs
filter-all {[]} [] = refl
filter-all {x ∷ xs} (px ∷ pxs) with P? x
... | no ¬px = contradiction px ¬px
... | true because _ = cong (x ∷_) (filter-all pxs)
... | false because [¬px] = contradiction px (invert [¬px])
... | true because _ = cong (x ∷_) (filter-all pxs)

filter-notAll : ∀ xs → Any (∁ P) xs → length (filter P? xs) < length xs
filter-notAll (x ∷ xs) (here ¬px) with P? x
... | false because _ = s≤s (length-filter xs)
... | yes px = contradiction px ¬px
... | false because _ = s≤s (length-filter xs)
... | true because [px] = contradiction (invert [px]) ¬px
filter-notAll (x ∷ xs) (there any) with ih ← filter-notAll xs any | does (P? x)
... | false = m≤n⇒m≤1+n ih
... | true = s≤s ih
Expand All @@ -965,8 +965,8 @@ module _ {P : Pred A p} (P? : Decidable P) where
filter-none : ∀ {xs} → All (∁ P) xs → filter P? xs ≡ []
filter-none {[]} [] = refl
filter-none {x ∷ xs} (¬px ∷ ¬pxs) with P? x
... | false because _ = filter-none ¬pxs
... | yes px = contradiction px ¬px
... | false because _ = filter-none ¬pxs
... | true because [px] = contradiction (invert [px]) ¬px

filter-complete : ∀ {xs} → length (filter P? xs) ≡ length xs →
filter P? xs ≡ xs
Expand All @@ -977,13 +977,13 @@ module _ {P : Pred A p} (P? : Decidable P) where

filter-accept : ∀ {x xs} → P x → filter P? (x ∷ xs) ≡ x ∷ (filter P? xs)
filter-accept {x} Px with P? x
... | true because _ = refl
... | no ¬Px = contradiction Px ¬Px
... | true because _ = refl
... | false because [¬Px] = contradiction Px (invert [¬Px])

filter-reject : ∀ {x xs} → ¬ P x → filter P? (x ∷ xs) ≡ filter P? xs
filter-reject {x} ¬Px with P? x
... | yes Px = contradiction Px ¬Px
... | false because _ = refl
... | true because [Px] = contradiction (invert [Px]) ¬Px
... | false because _ = refl

filter-idem : filter P? ∘ filter P? ≗ filter P?
filter-idem [] = refl
Expand Down Expand Up @@ -1040,7 +1040,7 @@ module _ {P : Pred A p} (P? : Decidable P) where
... | true = cong (Product.map (x ∷_) id) ih
... | false = cong (Product.map id (x ∷_)) ih

length-partition : ∀ xs → (let (ys , zs) = partition P? xs) →
length-partition : ∀ xs → (let ys , zs = partition P? xs) →
length ys ≤ length xs × length zs ≤ length xs
length-partition [] = z≤n , z≤n
length-partition (x ∷ xs) with ih ← length-partition xs | does (P? x)
Expand Down
Loading