Make decidable versions of sublist functions the default (agda#2186)

* Make decdable versions of sublist functions the default

* Remove imports Bool.Properties

* Address comments

Author: MatthewDaggitt

src/Data/List/Base.agda

@@ -23,11 +23,11 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base
   using (id; _∘_ ; _∘′_; _∘₂_; _$_; const; flip)
 open import Level using (Level)
-open import Relation.Nullary.Decidable.Core using (does; ¬?)
 open import Relation.Unary using (Pred; Decidable)
 open import Relation.Binary.Core using (Rel)
 import Relation.Binary.Definitions as B
 open import Relation.Binary.PropositionalEquality.Core using (_≡_)
+open import Relation.Nullary.Decidable.Core using (T?; does; ¬?)
 
 private
   variable
@@ -346,141 +346,160 @@ removeAt : (xs : List A) → Fin (length xs) → List A
 removeAt (x ∷ xs) zero     = xs
 removeAt (x ∷ xs) (suc i)  = x ∷ removeAt xs i
 
--- The following are functions which split a list up using boolean
--- predicates. However, in practice they are difficult to use and
--- prove properties about, and are mainly provided for advanced use
--- cases where one wants to minimise dependencies. In most cases
--- you probably want to use the versions defined below based on
--- decidable predicates. e.g. use `takeWhile (_≤? 10) xs`
--- instead of `takeWhileᵇ (_≤ᵇ 10) xs`
+------------------------------------------------------------------------
+-- Operations for filtering lists
+
+-- The following are a variety of functions that can be used to
+-- construct sublists using a predicate.
+--
+-- Each function has two forms. The first main variant uses a
+-- proof-relevant decidable predicate, while the second variant uses
+-- a irrelevant boolean predicate and are suffixed with a `ᵇ` character,
+-- typed as \^b.
+--
+-- The decidable versions have several advantages: 1) easier to prove
+-- properties, 2) better meta-variable inference and 3) most of the rest
+-- of the library is set-up to work with decidable predicates. However,
+-- in rare cases the boolean versions can be useful, mainly when one
+-- wants to minimise dependencies.
+--
+-- In summary, in most cases you probably want to use the decidable
+-- versions over the boolean versions, e.g. use `takeWhile (_≤? 10) xs`
+-- rather than `takeWhileᵇ (_≤ᵇ 10) xs`.
+
+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ᵇ : (A → Bool) → List A → List A
-takeWhileᵇ p []       = []
-takeWhileᵇ p (x ∷ xs) = if p x then x ∷ takeWhileᵇ p xs else []
+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ᵇ : (A → Bool) → List A → List A
-dropWhileᵇ p []       = []
-dropWhileᵇ p (x ∷ xs) = if p x then dropWhileᵇ p xs else x ∷ xs
+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ᵇ : (A → Bool) → List A → List A
-filterᵇ p []       = []
-filterᵇ p (x ∷ xs) = if p x then x ∷ filterᵇ p xs else filterᵇ p xs
+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ᵇ : (A → Bool) → List A → List A × List A
-partitionᵇ p []       = ([] , [])
-partitionᵇ p (x ∷ xs) = (if p x then Prod.map₁ else Prod.map₂′) (x ∷_) (partitionᵇ p xs)
+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  = Prod.map (x ∷_) id (span P? xs)
+... | false = ([] , ys)
+
 
 spanᵇ : (A → Bool) → List A → List A × List A
-spanᵇ p []       = ([] , [])
-spanᵇ p (x ∷ xs) = if p x
-  then Prod.map₁ (x ∷_) (spanᵇ p xs)
-  else ([] , x ∷ xs)
+spanᵇ p = span (T? ∘ p)
+
+break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
+break P? = span (¬? ∘ P?)
 
 breakᵇ : (A → Bool) → List A → List A × List A
-breakᵇ p = spanᵇ (not ∘ p)
+breakᵇ p = break (T? ∘ p)
+
+-- The predicate `P` represents the notion of newline character for the
+-- type `A`. It is used to split the input list into a list of lines.
+-- Some lines may be empty if the input contains at least two
+-- consecutive newline characters.
+linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
+linesBy {A = A} P? = go nothing where
 
-linesByᵇ : (A → Bool) → List A → List (List A)
-linesByᵇ {A = A} p = go nothing
-  where
   go : Maybe (List A) → List A → List (List A)
   go acc []       = maybe′ ([_] ∘′ reverse) [] acc
-  go acc (c ∷ cs) with p c
+  go acc (c ∷ cs) with does (P? c)
   ... | true  = reverse (Maybe.fromMaybe [] acc) ∷ go nothing cs
   ... | false = go (just (c ∷ Maybe.fromMaybe [] acc)) cs
 
-wordsByᵇ : (A → Bool) → List A → List (List A)
-wordsByᵇ {A = A} p = go []
-  where
+linesByᵇ : (A → Bool) → List A → List (List A)
+linesByᵇ p = linesBy (T? ∘ p)
+
+-- The predicate `P` represents the notion of space character for the
+-- type `A`. It is used to split the input list into a list of words.
+-- All the words are non empty and the output does not contain any space
+-- characters.
+wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
+wordsBy {A = A} P? = go [] where
+
   cons : List A → List (List A) → List (List A)
   cons [] ass = ass
   cons as ass = reverse as ∷ ass
 
   go : List A → List A → List (List A)
   go acc []       = cons acc []
-  go acc (c ∷ cs) with p c
+  go acc (c ∷ cs) with does (P? c)
   ... | true  = cons acc (go [] cs)
   ... | false = go (c ∷ acc) cs
 
+wordsByᵇ : (A → Bool) → List A → List (List A)
+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ᵇ : (A → A → Bool) → List A → List A
-derunᵇ r []           = []
-derunᵇ r (x ∷ [])     = x ∷ []
-derunᵇ r (x ∷ y ∷ xs) = if r x y
-  then derunᵇ r (y ∷ xs)
-  else x ∷ derunᵇ r (y ∷ xs)
+derunᵇ r = derun (T? ∘₂ r)
+
+deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A
+deduplicate R? [] = []
+deduplicate R? (x ∷ xs) = x ∷ filter (¬? ∘ R? x) (deduplicate R? xs)
 
 deduplicateᵇ : (A → A → Bool) → List A → List A
-deduplicateᵇ r [] = []
-deduplicateᵇ r (x ∷ xs) = x ∷ filterᵇ (not ∘ r x) (deduplicateᵇ r xs)
+deduplicateᵇ r = deduplicate (T? ∘₂ r)
 
 -- Finds the first element satisfying the boolean predicate
+find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A
+find P? []       = nothing
+find P? (x ∷ xs) = if does (P? x) then just x else find P? xs
+
 findᵇ : (A → Bool) → List A → Maybe A
-findᵇ p []       = nothing
-findᵇ p (x ∷ xs) = if p x then just x else findᵇ p xs
+findᵇ p = find (T? ∘ p)
 
 -- Finds the index of the first element satisfying the boolean predicate
-findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs)
-findIndexᵇ p []       = nothing
-findIndexᵇ p (x ∷ xs) = if p x
+findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs)
+findIndex P? [] = nothing
+findIndex P? (x ∷ xs) = if does (P? x)
   then just zero
-  else Maybe.map suc (findIndexᵇ p xs)
+  else Maybe.map suc (findIndex P? xs)
+
+findIndexᵇ : (A → Bool) → (xs : List A) → Maybe $ Fin (length xs)
+findIndexᵇ p = findIndex (T? ∘ p)
 
 -- Finds indices of all the elements satisfying the boolean predicate
-findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs)
-findIndicesᵇ p []       = []
-findIndicesᵇ p (x ∷ xs) = if p x
+findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs)
+findIndices P? []       = []
+findIndices P? (x ∷ xs) = if does (P? x)
   then zero ∷ indices
   else indices
-    where indices = map suc (findIndicesᵇ p xs)
-
--- Equivalent functions that use a decidable predicate instead of a
--- boolean function.
-
-takeWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
-takeWhile P? = takeWhileᵇ (does ∘ P?)
-
-dropWhile : ∀ {P : Pred A p} → Decidable P → List A → List A
-dropWhile P? = dropWhileᵇ (does ∘ P?)
+    where indices = map suc (findIndices P? xs)
 
-filter : ∀ {P : Pred A p} → Decidable P → List A → List A
-filter P? = filterᵇ (does ∘ P?)
-
-partition : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
-partition P? = partitionᵇ (does ∘ P?)
-
-span : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
-span P? = spanᵇ (does ∘ P?)
-
-break : ∀ {P : Pred A p} → Decidable P → List A → (List A × List A)
-break P? = breakᵇ (does ∘ P?)
-
--- The predicate `P` represents the notion of newline character for the
--- type `A`. It is used to split the input list into a list of lines.
--- Some lines may be empty if the input contains at least two
--- consecutive newline characters.
-linesBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
-linesBy P? = linesByᵇ (does ∘ P?)
-
--- The predicate `P` represents the notion of space character for the
--- type `A`. It is used to split the input list into a list of words.
--- All the words are non empty and the output does not contain any space
--- characters.
-wordsBy : ∀ {P : Pred A p} → Decidable P → List A → List (List A)
-wordsBy P? = wordsByᵇ (does ∘ P?)
-
-derun : ∀ {R : Rel A p} → B.Decidable R → List A → List A
-derun R? = derunᵇ (does ∘₂ R?)
-
-deduplicate : ∀ {R : Rel A p} → B.Decidable R → List A → List A
-deduplicate R? = deduplicateᵇ (does ∘₂ R?)
-
-find : ∀ {P : Pred A p} → Decidable P → List A → Maybe A
-find P? = findᵇ (does ∘ P?)
-
-findIndex : ∀ {P : Pred A p} → Decidable P → (xs : List A) → Maybe $ Fin (length xs)
-findIndex P? = findIndexᵇ (does ∘ P?)
-
-findIndices : ∀ {P : Pred A p} → Decidable P → (xs : List A) → List $ Fin (length xs)
-findIndices P? = findIndicesᵇ (does ∘ P?)
+findIndicesᵇ : (A → Bool) → (xs : List A) → List $ Fin (length xs)
+findIndicesᵇ p = findIndices (T? ∘ p)
 
 ------------------------------------------------------------------------
 -- Actions on single elements

src/Data/List/Relation/Unary/Unique/DecSetoid/Properties.agda

@@ -12,7 +12,6 @@ open import Data.List.Relation.Unary.All.Properties using (all-filter)
 open import Data.List.Relation.Unary.Unique.Setoid.Properties
 open import Level
 open import Relation.Binary.Bundles using (DecSetoid)
-open import Relation.Nullary.Decidable using (¬?)
 
 module Data.List.Relation.Unary.Unique.DecSetoid.Properties where
 
@@ -30,5 +29,4 @@ module _ (DS : DecSetoid a ℓ) where
 
   deduplicate-! : ∀ xs → Unique (deduplicate _≟_ xs)
   deduplicate-! []       = []
-  deduplicate-! (x ∷ xs) = all-filter (λ y → ¬? (x ≟ y)) (deduplicate _≟_ xs)
-                         ∷ filter⁺ S  (λ y → ¬? (x ≟ y)) (deduplicate-! xs)
+  deduplicate-! (x ∷ xs) = all-filter _ (deduplicate _≟_ xs) ∷ filter⁺ S _ (deduplicate-! xs)

src/Data/String/Base.agda

@@ -22,7 +22,7 @@ open import Level using (Level; 0ℓ)
 open import Relation.Binary.Core using (Rel)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl)
 open import Relation.Unary using (Pred; Decidable)
-open import Relation.Nullary.Decidable.Core using (does)
+open import Relation.Nullary.Decidable.Core using (does; T?)
 
 ------------------------------------------------------------------------
 -- From Agda.Builtin: type and renamed primitives
@@ -160,11 +160,11 @@ fromAlignment Right  = padLeft ' '
 ------------------------------------------------------------------------
 -- Splitting strings
 
-wordsByᵇ : (Char → Bool) → String → List String
-wordsByᵇ p = List.map fromList ∘ List.wordsByᵇ p ∘ toList
-
 wordsBy : ∀ {p} {P : Pred Char p} → Decidable P → String → List String
-wordsBy P? = wordsByᵇ (does ∘ P?)
+wordsBy P? = List.map fromList ∘ List.wordsBy P? ∘ toList
+
+wordsByᵇ : (Char → Bool) → String → List String
+wordsByᵇ p = wordsBy (T? ∘ p)
 
 words : String → List String
 words = wordsByᵇ Char.isSpace
@@ -173,11 +173,11 @@ words = wordsByᵇ Char.isSpace
 _ : words " abc  b   " ≡ "abc" ∷ "b" ∷ []
 _ = refl
 
-linesByᵇ : (Char → Bool) → String → List String
-linesByᵇ p = List.map fromList ∘ List.linesByᵇ p ∘ toList
-
 linesBy : ∀ {p} {P : Pred Char p} → Decidable P → String → List String
-linesBy P? = linesByᵇ (does ∘ P?)
+linesBy P? = List.map fromList ∘ List.linesBy P? ∘ toList
+
+linesByᵇ : (Char → Bool) → String → List String
+linesByᵇ p = linesBy (T? ∘ p)
 
 lines : String → List String
 lines = linesByᵇ ('\n' Char.≈ᵇ_)

src/Data/Vec/Base.agda

@@ -8,7 +8,7 @@
 
 module Data.Vec.Base where
 
-open import Data.Bool.Base using (Bool; if_then_else_)
+open import Data.Bool.Base using (Bool; true; false; if_then_else_)
 open import Data.Nat.Base
 open import Data.Fin.Base using (Fin; zero; suc)
 open import Data.List.Base as List using (List)
@@ -17,7 +17,7 @@ open import Data.These.Base as These using (These; this; that; these)
 open import Function.Base using (const; _∘′_; id; _∘_)
 open import Level using (Level)
 open import Relation.Binary.PropositionalEquality.Core using (_≡_; refl; trans; cong)
-open import Relation.Nullary.Decidable.Core using (does)
+open import Relation.Nullary.Decidable.Core using (does; T?)
 open import Relation.Unary using (Pred; Decidable)
 
 private
@@ -230,12 +230,14 @@ foldl₁ _⊕_ (x ∷ xs) = foldl _ _⊕_ x xs
 sum : Vec ℕ n → ℕ
 sum = foldr _ _+_ 0
 
-countᵇ : (A → Bool) → Vec A n → ℕ
-countᵇ p []       = zero
-countᵇ p (x ∷ xs) = if p x then suc (countᵇ p xs) else countᵇ p xs
-
 count : ∀ {P : Pred A p} → Decidable P → Vec A n → ℕ
-count P? = countᵇ (does ∘ P?)
+count P? []       = zero
+count P? (x ∷ xs) with does (P? x)
+... | true  = suc (count P? xs)
+... | false = count P? xs
+
+countᵇ : (A → Bool) → Vec A n → ℕ
+countᵇ p = count (T? ∘ p)
 
 ------------------------------------------------------------------------
 -- Operations for building vectors