Skip to content

Commit f35135d

Browse files
authored
Add filter-≐ (#2501)
* Add filter-≐ * Avoid rewrite
1 parent 397ab08 commit f35135d

File tree

2 files changed

+12
-3
lines changed

2 files changed

+12
-3
lines changed

CHANGELOG.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,7 @@ Additions to existing modules
185185
product≢0 : All NonZero ns → NonZero (product ns)
186186
∈⇒≤product : All NonZero ns → n ∈ ns → n ≤ product ns
187187
concatMap-++ : concatMap f (xs ++ ys) ≡ concatMap f xs ++ concatMap f ys
188+
filter-≐ : P ≐ Q → filter P? ≗ filter Q?
188189
```
189190

190191
* In `Data.List.Relation.Unary.Any.Properties`:

src/Data/List/Properties.agda

Lines changed: 11 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,16 +45,16 @@ open import Relation.Binary.PropositionalEquality.Properties as ≡
4545
open import Relation.Binary.Core using (Rel)
4646
open import Relation.Nullary.Reflects using (invert)
4747
open import Relation.Nullary using (¬_; Dec; does; _because_; yes; no; contradiction)
48-
open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_)
49-
open import Relation.Unary using (Pred; Decidable; ∁)
48+
open import Relation.Nullary.Decidable as Decidable using (isYes; map′; ⌊_⌋; ¬?; _×-dec_; dec-true; dec-false)
49+
open import Relation.Unary using (Pred; Decidable; ∁; _≐_)
5050
open import Relation.Unary.Properties using (∁?)
5151
import Data.Nat.GeneralisedArithmetic as ℕ
5252

5353
open ≡-Reasoning
5454

5555
private
5656
variable
57-
a b c d e p ℓ : Level
57+
a b c d e p q : Level
5858
A : Set a
5959
B : Set b
6060
C : Set c
@@ -1236,6 +1236,14 @@ module _ {P : Pred A p} (P? : Decidable P) where
12361236
... | true = cong (x ∷_) ih
12371237
... | false = ih
12381238

1239+
module _ {P : Pred A p} {Q : Pred A q} (P? : Decidable P) (Q? : Decidable Q) where
1240+
1241+
filter-≐ : P ≐ Q filter P? ≗ filter Q?
1242+
filter-≐ P≐Q [] = refl
1243+
filter-≐ P≐Q (x ∷ xs) with P? x
1244+
... | yes P[x] = trans (cong (x ∷_) (filter-≐ P≐Q xs)) (sym (filter-accept Q? (proj₁ P≐Q P[x])))
1245+
... | no ¬P[x] = trans (filter-≐ P≐Q xs) (sym (filter-reject Q? (¬P[x] ∘ proj₂ P≐Q)))
1246+
12391247
------------------------------------------------------------------------
12401248
-- derun and deduplicate
12411249

0 commit comments

Comments
 (0)