9
9
open import Category.Monad
10
10
open import Coinduction
11
open import Data.Bool using (Bool; true; false)
12
open import Data.Empty using (⊥)
13
open import Data.Maybe using (Maybe; nothing; just)
14
open import Data.Nat using (ℕ; zero; suc)
15
open import Data.Conat using (Coℕ; zero; suc)
16
open import Data.List using (List; []; _∷_)
17
open import Data.List.NonEmpty using (List⁺; _∷_)
18
renaming ([_] to [_]⁺)
11
open import Data.Bool using (Bool; true; false)
19
12
open import Data.BoundedVec.Inefficient as BVec
20
13
using (BoundedVec; []; _∷_)
21
open import Data.Product using (_,_)
22
open import Data.Sum using (_⊎_; inj₁; inj₂)
14
open import Data.Conat using (Coℕ; zero; suc)
15
open import Data.Empty using (⊥)
16
open import Data.Maybe using (Maybe; nothing; just; Is-just)
17
open import Data.Nat using (ℕ; zero; suc; _≥′_; ≤′-refl; ≤′-step)
18
open import Data.Nat.Properties using (s≤′s)
19
open import Data.List using (List; []; _∷_)
20
open import Data.List.NonEmpty using (List⁺; _∷_)
21
open import Data.Product as Prod using (∃; _×_; _,_)
22
open import Data.Sum as Sum using (_⊎_; inj₁; inj₂; [_,_]′)
23
23
open import Function
24
open import Function.Equality using (_⟨$⟩_)
25
open import Function.Inverse as Inv using (_↔_; module Inverse)
24
26
open import Level using (_⊔_)
25
27
open import Relation.Binary
26
28
import Relation.Binary.InducedPreorders as Ind
27
open import Relation.Binary.PropositionalEquality using (_≡_)
29
open import Relation.Binary.PropositionalEquality as P using (_≡_)
28
30
open import Relation.Nullary
29
31
open import Relation.Nullary.Negation
30
open RawMonad (¬¬-Monad {p = Level.zero})
33
module ¬¬Monad {p} where
34
open RawMonad (¬¬-Monad {p}) public
35
open ¬¬Monad -- we don't want the RawMonad content to be opened publicly
32
37
------------------------------------------------------------------------
91
96
(x ∷ xs) ++ ys = x ∷ ♯ (♭ xs ++ ys)
98
-- Interleaves the two colists (until the shorter one, if any, has
103
_⋎_ : ∀ {a} {A : Set a} → Colist A → Colist A → Colist A
105
(x ∷ xs) ⋎ ys = x ∷ ♯ (ys ⋎ ♭ xs)
93
107
concat : ∀ {a} {A : Set a} → Colist (List⁺ A) → Colist A
95
concat ([ x ]⁺ ∷ xss) = x ∷ ♯ concat (♭ xss)
96
concat ((x ∷ xs) ∷ xss) = x ∷ ♯ concat (xs ∷ xss)
109
concat ((x ∷ []) ∷ xss) = x ∷ ♯ concat (♭ xss)
110
concat ((x ∷ (y ∷ xs)) ∷ xss) = x ∷ ♯ concat ((y ∷ xs) ∷ xss)
98
112
[_] : ∀ {a} {A : Set a} → A → Colist A
101
115
------------------------------------------------------------------------
118
-- Any lemma for map.
120
Any-map : ∀ {a b p} {A : Set a} {B : Set b} {P : B → Set p}
122
Any P (map f xs) ↔ Any (P ∘ f) xs
123
Any-map {P = P} {f} = λ {xs} → record
124
{ to = P.→-to-⟶ (to xs)
125
; from = P.→-to-⟶ (from xs)
126
; inverse-of = record
127
{ left-inverse-of = from∘to xs
128
; right-inverse-of = to∘from xs
132
to : ∀ xs → Any P (map f xs) → Any (P ∘ f) xs
134
to (x ∷ xs) (here px) = here px
135
to (x ∷ xs) (there p) = there (to (♭ xs) p)
137
from : ∀ xs → Any (P ∘ f) xs → Any P (map f xs)
139
from (x ∷ xs) (here px) = here px
140
from (x ∷ xs) (there p) = there (from (♭ xs) p)
142
from∘to : ∀ xs (p : Any P (map f xs)) → from xs (to xs p) ≡ p
144
from∘to (x ∷ xs) (here px) = P.refl
145
from∘to (x ∷ xs) (there p) = P.cong there (from∘to (♭ xs) p)
147
to∘from : ∀ xs (p : Any (P ∘ f) xs) → to xs (from xs p) ≡ p
149
to∘from (x ∷ xs) (here px) = P.refl
150
to∘from (x ∷ xs) (there p) = P.cong there (to∘from (♭ xs) p)
152
-- Any lemma for _⋎_. This lemma implies that every member of xs or ys
153
-- is a member of xs ⋎ ys, and vice versa.
155
Any-⋎ : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
156
Any P (xs ⋎ ys) ↔ (Any P xs ⊎ Any P ys)
157
Any-⋎ {P = P} = λ xs → record
158
{ to = P.→-to-⟶ (to xs)
159
; from = P.→-to-⟶ (from xs)
160
; inverse-of = record
161
{ left-inverse-of = from∘to xs
162
; right-inverse-of = to∘from xs
166
to : ∀ xs {ys} → Any P (xs ⋎ ys) → Any P xs ⊎ Any P ys
168
to (x ∷ xs) (here px) = inj₁ (here px)
169
to (x ∷ xs) (there p) = [ inj₂ , inj₁ ∘ there ]′ (to _ p)
173
from-left : ∀ {xs ys} → Any P xs → Any P (xs ⋎ ys)
174
from-left (here px) = here px
175
from-left {ys = ys} (there p) = there (from-right ys p)
177
from-right : ∀ xs {ys} → Any P ys → Any P (xs ⋎ ys)
179
from-right (x ∷ xs) p = there (from-left p)
181
from : ∀ xs {ys} → Any P xs ⊎ Any P ys → Any P (xs ⋎ ys)
182
from xs = Sum.[ from-left , from-right xs ]
184
from∘to : ∀ xs {ys} (p : Any P (xs ⋎ ys)) → from xs (to xs p) ≡ p
185
from∘to [] p = P.refl
186
from∘to (x ∷ xs) (here px) = P.refl
187
from∘to (x ∷ xs) {ys = ys} (there p) with to ys p | from∘to ys p
188
from∘to (x ∷ xs) {ys = ys} (there .(from-left q)) | inj₁ q | P.refl = P.refl
189
from∘to (x ∷ xs) {ys = ys} (there .(from-right ys q)) | inj₂ q | P.refl = P.refl
193
to∘from-left : ∀ {xs ys} (p : Any P xs) →
194
to xs {ys = ys} (from-left p) ≡ inj₁ p
195
to∘from-left (here px) = P.refl
196
to∘from-left {ys = ys} (there p)
197
rewrite to∘from-right ys p = P.refl
199
to∘from-right : ∀ xs {ys} (p : Any P ys) →
200
to xs (from-right xs p) ≡ inj₂ p
201
to∘from-right [] p = P.refl
202
to∘from-right (x ∷ xs) {ys = ys} p
203
rewrite to∘from-left {xs = ys} {ys = ♭ xs} p = P.refl
205
to∘from : ∀ xs {ys} (p : Any P xs ⊎ Any P ys) → to xs (from xs p) ≡ p
206
to∘from xs = Sum.[ to∘from-left , to∘from-right xs ]
208
------------------------------------------------------------------------
104
211
-- xs ≈ ys means that xs and ys are equal.
146
253
map-cong f [] = []
147
254
map-cong f (x ∷ xs≈) = f x ∷ ♯ map-cong f (♭ xs≈)
256
-- Any respects pointwise implication (for the predicate) and equality
260
∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs ys} →
261
(∀ {x} → P x → Q x) → xs ≈ ys → Any P xs → Any Q ys
262
Any-resp f (x ∷ xs≈) (here px) = here (f px)
263
Any-resp f (x ∷ xs≈) (there p) = there (Any-resp f (♭ xs≈) p)
265
-- Any maps pointwise isomorphic predicates and equal colists to
269
∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q} {xs ys} →
270
(∀ {x} → P x ↔ Q x) → xs ≈ ys → Any P xs ↔ Any Q ys
271
Any-cong {A = A} P↔Q xs≈ys = record
272
{ to = P.→-to-⟶ (Any-resp (_⟨$⟩_ (Inverse.to P↔Q)) xs≈ys)
273
; from = P.→-to-⟶ (Any-resp (_⟨$⟩_ (Inverse.from P↔Q)) (sym xs≈ys))
274
; inverse-of = record
275
{ left-inverse-of = resp∘resp P↔Q xs≈ys (sym xs≈ys)
276
; right-inverse-of = resp∘resp (Inv.sym P↔Q) (sym xs≈ys) xs≈ys
280
open Setoid (setoid _) using (sym)
282
resp∘resp : ∀ {p q} {P : A → Set p} {Q : A → Set q} {xs ys}
283
(P↔Q : ∀ {x} → P x ↔ Q x)
284
(xs≈ys : xs ≈ ys) (ys≈xs : ys ≈ xs) (p : Any P xs) →
285
Any-resp (_⟨$⟩_ (Inverse.from P↔Q)) ys≈xs
286
(Any-resp (_⟨$⟩_ (Inverse.to P↔Q)) xs≈ys p) ≡ p
287
resp∘resp P↔Q (x ∷ xs≈) (.x ∷ ys≈) (here px) =
288
P.cong here (Inverse.left-inverse-of P↔Q px)
289
resp∘resp P↔Q (x ∷ xs≈) (.x ∷ ys≈) (there p) =
290
P.cong there (resp∘resp P↔Q (♭ xs≈) (♭ ys≈) p)
292
------------------------------------------------------------------------
295
-- Converts Any proofs to indices into the colist. The index can also
296
-- be seen as the size of the proof.
298
index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} → Any P xs → ℕ
299
index (here px) = zero
300
index (there p) = suc (index p)
302
-- The position returned by index is guaranteed to be within bounds.
304
lookup-index : ∀ {a p} {A : Set a} {P : A → Set p} {xs} (p : Any P xs) →
305
Is-just (lookup (index p) xs)
306
lookup-index (here px) = just _
307
lookup-index (there p) = lookup-index p
309
-- Any-resp preserves the index.
312
∀ {a p q} {A : Set a} {P : A → Set p} {Q : A → Set q}
313
{f : ∀ {x} → P x → Q x} {xs ys}
314
(xs≈ys : xs ≈ ys) (p : Any P xs) →
315
index (Any-resp f xs≈ys p) ≡ index p
316
index-Any-resp (x ∷ xs≈) (here px) = P.refl
317
index-Any-resp (x ∷ xs≈) (there p) =
318
P.cong suc (index-Any-resp (♭ xs≈) p)
320
-- The left-to-right direction of Any-⋎ returns a proof whose size is
321
-- no larger than that of the input proof.
324
∀ {a p} {A : Set a} {P : A → Set p} xs {ys} (p : Any P (xs ⋎ ys)) →
325
index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎ xs) ⟨$⟩ p)
326
index-Any-⋎ [] p = ≤′-refl
327
index-Any-⋎ (x ∷ xs) (here px) = ≤′-refl
328
index-Any-⋎ (x ∷ xs) {ys = ys} (there p)
329
with Inverse.to (Any-⋎ ys) ⟨$⟩ p | index-Any-⋎ ys p
330
... | inj₁ q | q≤p = ≤′-step q≤p
331
... | inj₂ q | q≤p = s≤′s q≤p
149
333
------------------------------------------------------------------------
150
334
-- Memberships, subsets, prefixes
171
355
[] : ∀ {ys} → [] ⊑ ys
172
356
_∷_ : ∀ x {xs ys} (p : ∞ (♭ xs ⊑ ♭ ys)) → x ∷ xs ⊑ x ∷ ys
358
-- Any can be expressed using _∈_ (and vice versa).
360
Any-∈ : ∀ {a p} {A : Set a} {P : A → Set p} {xs} →
361
Any P xs ↔ ∃ λ x → x ∈ xs × P x
362
Any-∈ {P = P} = record
364
; from = P.→-to-⟶ (λ { (x , x∈xs , p) → from x∈xs p })
365
; inverse-of = record
366
{ left-inverse-of = from∘to
367
; right-inverse-of = λ { (x , x∈xs , p) → to∘from x∈xs p }
371
to : ∀ {xs} → Any P xs → ∃ λ x → x ∈ xs × P x
372
to (here p) = _ , here P.refl , p
373
to (there p) = Prod.map id (Prod.map there id) (to p)
375
from : ∀ {x xs} → x ∈ xs → P x → Any P xs
376
from (here P.refl) p = here p
377
from (there x∈xs) p = there (from x∈xs p)
379
to∘from : ∀ {x xs} (x∈xs : x ∈ xs) (p : P x) →
380
to (from x∈xs p) ≡ (x , x∈xs , p)
381
to∘from (here P.refl) p = P.refl
382
to∘from (there x∈xs) p =
383
P.cong (Prod.map id (Prod.map there id)) (to∘from x∈xs p)
385
from∘to : ∀ {xs} (p : Any P xs) →
386
let (x , x∈xs , px) = to p in from x∈xs px ≡ p
387
from∘to (here _) = P.refl
388
from∘to (there p) = P.cong there (from∘to p)
174
390
-- Prefixes are subsets.
176
392
⊑⇒⊆ : ∀ {a} → {A : Set a} → _⊑_ {A = A} ⇒ _⊆_
added
removed
src/Data/Colist.agda
