1
------------------------------------------------------------------------
2
-- Lists where at least one element satisfies a given property
3
------------------------------------------------------------------------
5
module Data.List.Any where
9
open import Data.Function
10
open import Data.List as List using (List; []; _∷_)
11
open import Data.Product as Prod using (∃; _×_; _,_)
13
open import Relation.Nullary
14
import Relation.Nullary.Decidable as Dec
15
open import Relation.Unary using () renaming (_⊆_ to _⋐_)
16
open import Relation.Binary
17
import Relation.Binary.InducedPreorders as Ind
18
open import Relation.Binary.List.Pointwise as ListEq using ([]; _∷_)
19
open import Relation.Binary.PropositionalEquality as PropEq
21
import Relation.Binary.Props.Preorder as PP
23
-- Any P xs means that at least one element in xs satisfies P.
25
data Any {A} (P : A → Set) : List A → Set where
26
here : ∀ {x xs} (px : P x) → Any P (x ∷ xs)
27
there : ∀ {x xs} (pxs : Any P xs) → Any P (x ∷ xs)
31
map : ∀ {A} {P Q : A → Set} → P ⋐ Q → Any P ⋐ Any Q
32
map g (here px) = here (g px)
33
map g (there pxs) = there (map g pxs)
35
-- If the head does not satisfy the predicate, then the tail will.
37
tail : ∀ {A x xs} {P : A → Set} → ¬ P x → Any P (x ∷ xs) → Any P xs
38
tail ¬px (here px) = ⊥-elim (¬px px)
39
tail ¬px (there pxs) = pxs
43
any : ∀ {A} {P : A → Set} →
44
(∀ x → Dec (P x)) → (xs : List A) → Dec (Any P xs)
46
any p (x ∷ xs) with p x
47
any p (x ∷ xs) | yes px = yes (here px)
48
any p (x ∷ xs) | no ¬px = Dec.map (there , tail ¬px) (any p xs)
50
-- index x∈xs is the list position (zero-based) which x∈xs points to.
52
index : ∀ {A} {P : A → Set} {xs} → Any P xs → Fin (List.length xs)
53
index (here px) = zero
54
index (there pxs) = suc (index pxs)
56
------------------------------------------------------------------------
57
-- List membership and some related definitions
59
module Membership (S : Setoid zero zero) where
62
open module S = Setoid S using (_≈_) renaming (Carrier to A)
63
open module LS = Setoid (ListEq.setoid S)
64
using () renaming (_≈_ to _≋_)
66
-- If a predicate P respects the underlying equality then Any P
67
-- respects the list equality.
69
lift-resp : ∀ {P} → P Respects _≈_ → Any P Respects _≋_
71
lift-resp resp (x≈y ∷ xs≈ys) (here px) = here (resp x≈y px)
72
lift-resp resp (x≈y ∷ xs≈ys) (there pxs) =
73
there (lift-resp resp xs≈ys pxs)
79
_∈_ : A → List A → Set
80
x ∈ xs = Any (_≈_ x) xs
82
_∉_ : A → List A → Set
89
_⊆_ : List A → List A → Set
90
xs ⊆ ys = ∀ {x} → x ∈ xs → x ∈ ys
92
_⊈_ : List A → List A → Set
95
-- Equality is respected by the predicate which is used to define
98
∈-resp-≈ : ∀ {x} → (_≈_ x) Respects _≈_
99
∈-resp-≈ = flip S.trans
101
-- List equality is respected by _∈_.
103
∈-resp-list-≈ : ∀ {x} → _∈_ x Respects _≋_
104
∈-resp-list-≈ = lift-resp ∈-resp-≈
106
-- _⊆_ is a preorder.
108
⊆-preorder : Preorder _ _ _
109
⊆-preorder = Ind.InducedPreorder₂ (ListEq.setoid S) _∈_ ∈-resp-list-≈
111
module ⊆-Reasoning where
112
import Relation.Binary.PreorderReasoning as PreR
113
open PreR ⊆-preorder public
114
renaming (_∼⟨_⟩_ to _⊆⟨_⟩_)
118
_∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
119
x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
121
-- Set equality, i.e. an equality which ignores order and
124
set-equality : Setoid _ _
125
set-equality = PP.inducedEquivalence ⊆-preorder
127
-- A variant of List.map.
129
map-with-∈ : ∀ {B : Set} (xs : List A) → (∀ {x} → x ∈ xs → B) → List B
131
map-with-∈ (x ∷ xs) f = f (here S.refl) ∷ map-with-∈ xs (f ∘ there)
133
-- Finds an element satisfying the predicate.
135
find : ∀ {P : A → Set} {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
136
find (here px) = (_ , here S.refl , px)
137
find (there pxs) = Prod.map id (Prod.map there id) (find pxs)
139
lose : ∀ {P x xs} → P Respects _≈_ → x ∈ xs → P x → Any P xs
140
lose resp x∈xs px = map (flip resp px) x∈xs
142
-- The code above instantiated (and slightly changed) for
143
-- propositional equality.
145
module Membership-≡ {A : Set} where
148
open module M = Membership (PropEq.setoid A) public
149
hiding ( lift-resp; lose
150
; ⊆-preorder; module ⊆-Reasoning; set-equality
153
lose : ∀ {P x xs} → x ∈ xs → P x → Any P xs
154
lose {P} = M.lose (PropEq.subst P)
156
-- _⊆_ is a preorder.
158
⊆-preorder : Preorder _ _ _
159
⊆-preorder = Ind.InducedPreorder₂ (PropEq.setoid (List A)) _∈_
160
(PropEq.subst (_∈_ _))
162
module ⊆-Reasoning where
163
import Relation.Binary.PreorderReasoning as PreR
164
open PreR ⊆-preorder public
165
renaming (_∼⟨_⟩_ to _⊆⟨_⟩_; _≈⟨_⟩_ to _≡⟨_⟩_)
169
_∈⟨_⟩_ : ∀ x {xs ys} → x ∈ xs → xs IsRelatedTo ys → x ∈ ys
170
x ∈⟨ x∈xs ⟩ xs⊆ys = (begin xs⊆ys) x∈xs
172
-- Set equality, i.e. an equality which ignores order and
175
set-equality : Setoid _ _
176
set-equality = PP.inducedEquivalence ⊆-preorder
178
------------------------------------------------------------------------
181
-- If any element satisfies P, then P is satisfied.
183
satisfied : ∀ {A} {P : A → Set} {xs} → Any P xs → ∃ P
184
satisfied = Prod.map id Prod.proj₂ ∘ Membership-≡.find
added
removed
src/Data/List/Any.agda
