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

…2365)

* refactor towards `if_then_else_` and away from `yes`/`no`

* reverted chnages to `derun` proofs

* undo last reversion!

* layout

src/Data/List/Base.agda

@@ -364,45 +364,49 @@ 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
@@ -453,9 +457,11 @@ 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)

src/Data/List/Properties.agda

@@ -1156,13 +1156,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
@@ -1178,8 +1178,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
@@ -1190,13 +1190,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
@@ -1234,13 +1234,13 @@ module _ {R : Rel A p} (R? : B.Decidable R) where
 
  derun-reject : ∀ {x y} xs → R x y → derun R? (x ∷ y ∷ xs) ≡ derun R? (y ∷ xs)
  derun-reject {x} {y} xs Rxy with R? x y
- ... | yes _ = refl
- ... | no ¬Rxy = contradiction Rxy ¬Rxy
+ ... | true because _  = refl
+ ... | false because [¬Rxy] = contradiction Rxy (invert [¬Rxy])
 
  derun-accept : ∀ {x y} xs → ¬ R x y → derun R? (x ∷ y ∷ xs) ≡ x ∷ derun R? (y ∷ xs)
  derun-accept {x} {y} xs ¬Rxy with R? x y
- ... | yes Rxy = contradiction Rxy ¬Rxy
- ... | no _ = refl
+ ... | true because [Rxy] = contradiction (invert [Rxy]) ¬Rxy
+ ... | false because _  = refl
 
 ------------------------------------------------------------------------
 -- partition
@@ -1253,7 +1253,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)