1
------------------------------------------------------------------------
2
-- The Agda standard library
4
-- Infinite merge operation for coinductive lists
5
------------------------------------------------------------------------
7
module Data.Colist.Infinite-merge where
9
open import Coinduction
10
open import Data.Colist as Colist hiding (_⋎_)
12
open import Data.Nat.Properties
13
open import Data.Product as Prod
16
open import Function.Equality using (_⟨$⟩_)
17
open import Function.Inverse as Inv using (_↔_; module Inverse)
18
import Function.Related as Related
19
open import Function.Related.TypeIsomorphisms
20
open import Induction.Nat
21
import Induction.WellFounded as WF
22
open import Relation.Binary.PropositionalEquality as P using (_≡_)
23
open import Relation.Binary.Sum
25
-- Some code that is used to work around Agda's syntactic guardedness
32
data ColistP {a} (A : Set a) : Set a where
34
_∷_ : A → ∞ (ColistP A) → ColistP A
35
_⋎_ : ColistP A → ColistP A → ColistP A
37
data ColistW {a} (A : Set a) : Set a where
39
_∷_ : A → ColistP A → ColistW A
41
program : ∀ {a} {A : Set a} → Colist A → ColistP A
43
program (x ∷ xs) = x ∷ ♯ program (♭ xs)
47
_⋎W_ : ∀ {a} {A : Set a} → ColistW A → ColistP A → ColistW A
49
(x ∷ xs) ⋎W ys = x ∷ (ys ⋎ xs)
51
whnf : ∀ {a} {A : Set a} → ColistP A → ColistW A
53
whnf (x ∷ xs) = x ∷ ♭ xs
54
whnf (xs ⋎ ys) = whnf xs ⋎W ys
58
⟦_⟧P : ∀ {a} {A : Set a} → ColistP A → Colist A
59
⟦ xs ⟧P = ⟦ whnf xs ⟧W
61
⟦_⟧W : ∀ {a} {A : Set a} → ColistW A → Colist A
63
⟦ x ∷ xs ⟧W = x ∷ ♯ ⟦ xs ⟧P
67
⋎-homP : ∀ {a} {A : Set a} (xs : ColistP A) {ys} →
68
⟦ xs ⋎ ys ⟧P ≈ ⟦ xs ⟧P Colist.⋎ ⟦ ys ⟧P
69
⋎-homP xs = ⋎-homW (whnf xs) _
71
⋎-homW : ∀ {a} {A : Set a} (xs : ColistW A) ys →
72
⟦ xs ⋎W ys ⟧W ≈ ⟦ xs ⟧W Colist.⋎ ⟦ ys ⟧P
73
⋎-homW (x ∷ xs) ys = x ∷ ♯ ⋎-homP ys
74
⋎-homW [] ys = begin ⟦ ys ⟧P ∎
75
where open ≈-Reasoning
77
⟦program⟧P : ∀ {a} {A : Set a} (xs : Colist A) →
80
⟦program⟧P (x ∷ xs) = x ∷ ♯ ⟦program⟧P (♭ xs)
82
Any-⋎P : ∀ {a p} {A : Set a} {P : A → Set p} xs {ys} →
83
Any P ⟦ program xs ⋎ ys ⟧P ↔ (Any P xs ⊎ Any P ⟦ ys ⟧P)
84
Any-⋎P {P = P} xs {ys} =
85
Any P ⟦ program xs ⋎ ys ⟧P ↔⟨ Any-cong Inv.id (⋎-homP (program xs)) ⟩
86
Any P (⟦ program xs ⟧P Colist.⋎ ⟦ ys ⟧P) ↔⟨ Any-⋎ _ ⟩
87
(Any P ⟦ program xs ⟧P ⊎ Any P ⟦ ys ⟧P) ↔⟨ Any-cong Inv.id (⟦program⟧P _) ⊎-cong (_ ∎) ⟩
88
(Any P xs ⊎ Any P ⟦ ys ⟧P) ∎
89
where open Related.EquationalReasoning
92
∀ {a p} {A : Set a} {P : A → Set p} xs {ys}
93
(p : Any P ⟦ program xs ⋎ ys ⟧P) →
94
index p ≥′ [ index , index ]′ (Inverse.to (Any-⋎P xs) ⟨$⟩ p)
96
with Any-resp id (⋎-homW (whnf (program xs)) _) p
97
| index-Any-resp {f = id} (⋎-homW (whnf (program xs)) _) p
98
index-Any-⋎P xs p | q | q≡p
99
with Inverse.to (Any-⋎ ⟦ program xs ⟧P) ⟨$⟩ q
100
| index-Any-⋎ ⟦ program xs ⟧P q
101
index-Any-⋎P xs p | q | q≡p | inj₂ r | r≤q rewrite q≡p = r≤q
102
index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q
103
with Any-resp id (⟦program⟧P xs) r
104
| index-Any-resp {f = id} (⟦program⟧P xs) r
105
index-Any-⋎P xs p | q | q≡p | inj₁ r | r≤q | s | s≡r
106
rewrite s≡r | q≡p = r≤q
108
-- Infinite variant of _⋎_.
112
merge′ : ∀ {a} {A : Set a} → Colist (A × Colist A) → ColistP A
114
merge′ ((x , xs) ∷ xss) = x ∷ ♯ (program xs ⋎ merge′ (♭ xss))
116
merge : ∀ {a} {A : Set a} → Colist (A × Colist A) → Colist A
117
merge xss = ⟦ merge′ xss ⟧P
119
-- Any lemma for merge.
122
∀ {a p} {A : Set a} {P : A → Set p} xss →
123
Any P (merge xss) ↔ Any (λ { (x , xs) → P x ⊎ Any P xs }) xss
124
Any-merge {P = P} = λ xss → record
125
{ to = P.→-to-⟶ (proj₁ ∘ to xss)
126
; from = P.→-to-⟶ from
127
; inverse-of = record
128
{ left-inverse-of = proj₂ ∘ to xss
129
; right-inverse-of = λ p → begin
130
proj₁ (to xss (from p)) ≡⟨ from-injective _ _ (proj₂ (to xss (from p))) ⟩
137
-- The from function.
139
Q = λ { (x , xs) → P x ⊎ Any P xs }
141
from : ∀ {xss} → Any Q xss → Any P (merge xss)
142
from (here (inj₁ p)) = here p
143
from (here (inj₂ p)) = there (Inverse.from (Any-⋎P _) ⟨$⟩ inj₁ p)
144
from (there {x = _ , xs} p) = there (Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ (from p))
149
∀ {a p} {A : Set a} {P : A → Set p} {x xs} {p q : Any P _} →
150
_≡_ {A = Any P (x ∷ xs)} (there p) (there q) → p ≡ q
151
drop-there P.refl = P.refl
153
drop-inj₁ : ∀ {a b} {A : Set a} {B : Set b} {x y} →
154
_≡_ {A = A ⊎ B} (inj₁ x) (inj₁ y) → x ≡ y
155
drop-inj₁ P.refl = P.refl
157
drop-inj₂ : ∀ {a b} {A : Set a} {B : Set b} {x y} →
158
_≡_ {A = A ⊎ B} (inj₂ x) (inj₂ y) → x ≡ y
159
drop-inj₂ P.refl = P.refl
161
-- The from function is injective.
163
from-injective : ∀ {xss} (p₁ p₂ : Any Q xss) →
164
from p₁ ≡ from p₂ → p₁ ≡ p₂
165
from-injective (here (inj₁ p)) (here (inj₁ .p)) P.refl = P.refl
166
from-injective (here (inj₁ _)) (here (inj₂ _)) ()
167
from-injective (here (inj₂ _)) (here (inj₁ _)) ()
168
from-injective (here (inj₂ p₁)) (here (inj₂ p₂)) eq =
169
P.cong (here ∘ inj₂) $
171
Inverse.injective (Inv.sym (Any-⋎P _)) {x = inj₁ p₁} {y = inj₁ p₂} $
173
from-injective (here (inj₁ _)) (there _) ()
174
from-injective (here (inj₂ p₁)) (there p₂) eq
175
with Inverse.injective (Inv.sym (Any-⋎P _))
176
{x = inj₁ p₁} {y = inj₂ (from p₂)}
179
from-injective (there _) (here (inj₁ _)) ()
180
from-injective (there p₁) (here (inj₂ p₂)) eq
181
with Inverse.injective (Inv.sym (Any-⋎P _))
182
{x = inj₂ (from p₁)} {y = inj₁ p₂}
185
from-injective (there {x = _ , xs} p₁) (there p₂) eq =
187
from-injective p₁ p₂ $
189
Inverse.injective (Inv.sym (Any-⋎P xs))
190
{x = inj₂ (from p₁)} {y = inj₂ (from p₂)} $
193
-- The to function (defined as a right inverse of from).
195
Input = ∃ λ xss → Any P (merge xss)
198
Pred (xss , p) = ∃ λ (q : Any Q xss) → from q ≡ p
200
to : ∀ xss p → Pred (xss , p)
202
WF.All.wfRec (WF.Inverse-image.well-founded size <-well-founded) _
206
size (_ , p) = index p
208
step : ∀ p → WF.WfRec (_<′_ on size) Pred p → Pred p
210
step ((x , xs) ∷ xss , here p) rec = here (inj₁ p) , P.refl
211
step ((x , xs) ∷ xss , there p) rec
212
with Inverse.to (Any-⋎P xs) ⟨$⟩ p
213
| Inverse.left-inverse-of (Any-⋎P xs) p
215
step ((x , xs) ∷ xss , there .(Inverse.from (Any-⋎P xs) ⟨$⟩ inj₁ q)) rec | inj₁ q | P.refl | _ = here (inj₂ q) , P.refl
216
step ((x , xs) ∷ xss , there .(Inverse.from (Any-⋎P xs) ⟨$⟩ inj₂ q)) rec | inj₂ q | P.refl | q≤p =
218
(P.cong (there ∘ _⟨$⟩_ (Inverse.from (Any-⋎P xs)) ∘ inj₂))
219
(rec (♭ xss , q) (s≤′s q≤p))
221
-- Every member of xss is a member of merge xss, and vice versa (with
222
-- equal multiplicities).
224
∈-merge : ∀ {a} {A : Set a} {y : A} xss →
225
y ∈ merge xss ↔ ∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)
226
∈-merge {y = y} xss =
227
y ∈ merge xss ↔⟨ Any-merge _ ⟩
228
Any (λ { (x , xs) → y ≡ x ⊎ y ∈ xs }) xss ↔⟨ Any-∈ ⟩
229
(∃ λ { (x , xs) → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs) }) ↔⟨ Σ-assoc ⟩
230
(∃₂ λ x xs → (x , xs) ∈ xss × (y ≡ x ⊎ y ∈ xs)) ∎
231
where open Related.EquationalReasoning
added
removed
src/Data/Colist/Infinite-merge.agda
