From c4916a370eaa4b5e4bc42e950b960179d307ff14 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 15 Apr 2024 16:34:25 +0100 Subject: [PATCH 1/4] refactor towards `if_then_else_` and away from `yes`/`no` --- src/Data/List/Base.agda | 31 +++++++++++-------------------- src/Data/List/Properties.agda | 30 +++++++++++++++--------------- 2 files changed, 26 insertions(+), 35 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 8b988c646d..75466e0a06 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -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 @@ -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) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2d3c9e20e0..2c0410e5d8 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -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 @@ -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 @@ -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 @@ -1021,13 +1021,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 @@ -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) From 76afe8a79f1ee549bb486cc249509049da42d0fe Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 17 Apr 2024 07:52:13 +0100 Subject: [PATCH 2/4] reverted chnages to `derun` proofs --- src/Data/List/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index 2c0410e5d8..f7d8dd5531 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -1021,13 +1021,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 - ... | true because _ = refl - ... | false because [¬Rxy] = contradiction Rxy (invert [¬Rxy]) + ... | yes _ = refl + ... | no ¬Rxy = contradiction Rxy ¬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 - ... | true because [Rxy] = contradiction (invert [Rxy]) ¬Rxy - ... | false because _ = refl + ... | yes Rxy = contradiction Rxy ¬Rxy + ... | no _ = refl ------------------------------------------------------------------------ -- partition From 5ae64d36c29ff2fccb56fed64521cf2d96c8ade6 Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Wed, 17 Apr 2024 08:05:00 +0100 Subject: [PATCH 3/4] undo last reversion! --- src/Data/List/Properties.agda | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Data/List/Properties.agda b/src/Data/List/Properties.agda index f7d8dd5531..2c0410e5d8 100644 --- a/src/Data/List/Properties.agda +++ b/src/Data/List/Properties.agda @@ -1021,13 +1021,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 From f6673bdf8ae30e14ee1719770472e1f30b99759b Mon Sep 17 00:00:00 2001 From: jamesmckinna Date: Mon, 22 Apr 2024 06:01:04 +0100 Subject: [PATCH 4/4] layout --- src/Data/List/Base.agda | 33 ++++++++++++++++++++++++--------- 1 file changed, 24 insertions(+), 9 deletions(-) diff --git a/src/Data/List/Base.agda b/src/Data/List/Base.agda index 75466e0a06..23eccb3717 100644 --- a/src/Data/List/Base.agda +++ b/src/Data/List/Base.agda @@ -369,37 +369,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) = if does (P? x) then x ∷ takeWhile P? xs else [] +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) = if does (P? x) then dropWhile P? xs else 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) = let xs′ = filter P? xs - in if does (P? x) then x ∷ xs′ else 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) = let ys , zs = partition P? xs - in if does (P? x) then (x ∷ ys , zs) else (ys , x ∷ zs) +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) = if does (P? x) then Product.map (x ∷_) id (span P? xs) else ([] , ys) +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 @@ -450,8 +462,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 ∷ _)) = let ys = derun R? xs - in if does (R? x y) then ys else 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)