11
11
open import Algebra
12
12
open import Algebra.FunctionProperties
13
13
open import Category.Monad
14
open import Data.Empty
15
14
open import Data.List as List
16
15
import Data.List.Properties as LP
17
16
open import Data.List.Any as Any using (Any); open Any.Any
18
17
open import Data.List.Any.Properties
19
18
open import Data.Product
20
19
open import Data.Sum
22
20
open import Function
23
21
open import Function.Equality using (_⟨$⟩_)
24
22
import Function.Equivalence as FE
25
open import Function.Inverse as Inv using (_⇿_; module Inverse)
26
open import Function.Inverse.TypeIsomorphisms
23
open import Function.Inverse as Inv using (_↔_; module Inverse)
24
open import Function.Related as Related using (↔⇒; ⌊_⌋; ⌊_⌋→; ⇒→)
25
open import Function.Related.TypeIsomorphisms
28
26
open import Relation.Binary
29
27
import Relation.Binary.EqReasoning as EqR
30
import Relation.Binary.Sigma.Pointwise as Σ
31
28
open import Relation.Binary.PropositionalEquality as P
32
using (_≡_; _≗_; _with-≡_)
30
open import Relation.Binary.Sum
33
31
open import Relation.Nullary
35
33
open Any.Membership-≡
37
module Eq {k a} {A : Set a} = Setoid ([ k ]-Equality A)
35
module Eq {k a} {A : Set a} = Setoid ([ k ]-Equality A)
36
module Ord {k a} {A : Set a} = Preorder ([ k ]-Order A)
38
37
module ×⊎ {k ℓ} = CommutativeSemiring (×⊎-CommutativeSemiring k ℓ)
39
38
open module ListMonad {ℓ} = RawMonad (List.monad {ℓ = ℓ})
40
39
module ListMonoid {a} {A : Set a} = Monoid (List.monoid A)
43
commutativeMonoid : ∀ {a} → Kind → Set a → CommutativeMonoid _ _
44
commutativeMonoid {a} k A = record
46
; _≈_ = λ xs ys → xs ≈[ k ] ys
49
; isCommutativeMonoid = record
50
{ isSemigroup = record
51
{ isEquivalence = Eq.isEquivalence
52
; assoc = λ xs ys zs →
53
Eq.reflexive (ListMonoid.assoc xs ys zs)
54
; ∙-cong = λ {xs₁ xs₂ xs₃ xs₄} xs₁≈xs₂ xs₃≈xs₄ {x} →
55
x ∈ xs₁ ++ xs₃ ⇿⟨ sym $ ++⇿ {a = a} {p = a} ⟩
56
(x ∈ xs₁ ⊎ x ∈ xs₃) ≈⟨ xs₁≈xs₂ ⟨ ×⊎.+-cong ⟩ xs₃≈xs₄ ⟩
57
(x ∈ xs₂ ⊎ x ∈ xs₄) ⇿⟨ ++⇿ {a = a} {p = a} ⟩
60
; identityˡ = λ xs {x} → x ∈ xs ∎
61
; comm = λ xs ys {x} →
62
x ∈ xs ++ ys ⇿⟨ ++⇿++ {a = a} {p = a} xs ys ⟩
66
where open Inv.EquationalReasoning
69
empty-unique : ∀ {k a} {A : Set a} {xs : List A} →
70
xs ≈[ k ] [] → xs ≡ []
71
empty-unique {xs = []} _ = P.refl
72
empty-unique {xs = _ ∷ _} ∷≈[]
73
with FE.Equivalent.to (Inv.⇒⇔ ∷≈[]) ⟨$⟩ here P.refl
77
++-idempotent : ∀ {a} {A : Set a} →
78
Idempotent (λ (xs ys : List A) → xs ≈[ set ] ys) _++_
79
++-idempotent {a} xs {x} =
80
x ∈ xs ++ xs ≈⟨ FE.equivalent ([ id , id ]′ ∘ _⟨$⟩_ (Inverse.from $ ++⇿ {a = a} {p = a}))
81
(_⟨$⟩_ (Inverse.to $ ++⇿ {a = a} {p = a}) ∘ inj₁) ⟩
83
where open Inv.EquationalReasoning
41
------------------------------------------------------------------------
44
-- _∷_ is a congruence.
46
∷-cong : ∀ {a k} {A : Set a} {x₁ x₂ : A} {xs₁ xs₂} →
47
x₁ ≡ x₂ → xs₁ ∼[ k ] xs₂ → x₁ ∷ xs₁ ∼[ k ] x₂ ∷ xs₂
48
∷-cong {x₂ = x} {xs₁} {xs₂} P.refl xs₁≈xs₂ {y} =
49
y ∈ x ∷ xs₁ ↔⟨ sym $ ∷↔ (_≡_ y) ⟩
50
(y ≡ x ⊎ y ∈ xs₁) ∼⟨ (y ≡ x ∎) ⊎-cong xs₁≈xs₂ ⟩
51
(y ≡ x ⊎ y ∈ xs₂) ↔⟨ ∷↔ (_≡_ y) ⟩
53
where open Related.EquationalReasoning
85
55
-- List.map is a congruence.
87
57
map-cong : ∀ {ℓ k} {A B : Set ℓ} {f₁ f₂ : A → B} {xs₁ xs₂} →
88
f₁ ≗ f₂ → xs₁ ≈[ k ] xs₂ →
89
List.map f₁ xs₁ ≈[ k ] List.map f₂ xs₂
58
f₁ ≗ f₂ → xs₁ ∼[ k ] xs₂ →
59
List.map f₁ xs₁ ∼[ k ] List.map f₂ xs₂
90
60
map-cong {ℓ} {f₁ = f₁} {f₂} {xs₁} {xs₂} f₁≗f₂ xs₁≈xs₂ {x} =
91
x ∈ List.map f₁ xs₁ ⇿⟨ sym $ map⇿ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
92
Any (λ y → x ≡ f₁ y) xs₁ ≈⟨ Any-cong (Inv.⇿⇒ ∘ helper) xs₁≈xs₂ ⟩
93
Any (λ y → x ≡ f₂ y) xs₂ ⇿⟨ map⇿ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
61
x ∈ List.map f₁ xs₁ ↔⟨ sym $ map↔ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
62
Any (λ y → x ≡ f₁ y) xs₁ ∼⟨ Any-cong (↔⇒ ∘ helper) xs₁≈xs₂ ⟩
63
Any (λ y → x ≡ f₂ y) xs₂ ↔⟨ map↔ {a = ℓ} {b = ℓ} {p = ℓ} ⟩
94
64
x ∈ List.map f₂ xs₂ ∎
96
open Inv.EquationalReasoning
66
open Related.EquationalReasoning
98
helper : ∀ y → x ≡ f₁ y ⇿ x ≡ f₂ y
68
helper : ∀ y → x ≡ f₁ y ↔ x ≡ f₂ y
100
70
{ to = P.→-to-⟶ (λ x≡f₁y → P.trans x≡f₁y ( f₁≗f₂ y))
101
71
; from = P.→-to-⟶ (λ x≡f₂y → P.trans x≡f₂y (P.sym $ f₁≗f₂ y))
78
-- _++_ is a congruence.
80
++-cong : ∀ {a k} {A : Set a} {xs₁ xs₂ ys₁ ys₂ : List A} →
81
xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
82
xs₁ ++ ys₁ ∼[ k ] xs₂ ++ ys₂
83
++-cong {a} {xs₁ = xs₁} {xs₂} {ys₁} {ys₂} xs₁≈xs₂ ys₁≈ys₂ {x} =
84
x ∈ xs₁ ++ ys₁ ↔⟨ sym $ ++↔ {a = a} {p = a} ⟩
85
(x ∈ xs₁ ⊎ x ∈ ys₁) ∼⟨ xs₁≈xs₂ ⊎-cong ys₁≈ys₂ ⟩
86
(x ∈ xs₂ ⊎ x ∈ ys₂) ↔⟨ ++↔ {a = a} {p = a} ⟩
88
where open Related.EquationalReasoning
113
90
-- concat is a congruence.
115
92
concat-cong : ∀ {a k} {A : Set a} {xss₁ xss₂ : List (List A)} →
116
xss₁ ≈[ k ] xss₂ → concat xss₁ ≈[ k ] concat xss₂
93
xss₁ ∼[ k ] xss₂ → concat xss₁ ∼[ k ] concat xss₂
117
94
concat-cong {a} {xss₁ = xss₁} {xss₂} xss₁≈xss₂ {x} =
118
x ∈ concat xss₁ ⇿⟨ sym $ concat⇿ {a = a} {p = a} ⟩
119
Any (Any (_≡_ x)) xss₁ ≈⟨ Any-cong (λ _ → _ ∎) xss₁≈xss₂ ⟩
120
Any (Any (_≡_ x)) xss₂ ⇿⟨ concat⇿ {a = a} {p = a} ⟩
95
x ∈ concat xss₁ ↔⟨ sym $ concat↔ {a = a} {p = a} ⟩
96
Any (Any (_≡_ x)) xss₁ ∼⟨ Any-cong (λ _ → _ ∎) xss₁≈xss₂ ⟩
97
Any (Any (_≡_ x)) xss₂ ↔⟨ concat↔ {a = a} {p = a} ⟩
122
where open Inv.EquationalReasoning
99
where open Related.EquationalReasoning
124
101
-- The list monad's bind is a congruence.
126
103
>>=-cong : ∀ {ℓ k} {A B : Set ℓ} {xs₁ xs₂} {f₁ f₂ : A → List B} →
127
xs₁ ≈[ k ] xs₂ → (∀ x → f₁ x ≈[ k ] f₂ x) →
128
(xs₁ >>= f₁) ≈[ k ] (xs₂ >>= f₂)
104
xs₁ ∼[ k ] xs₂ → (∀ x → f₁ x ∼[ k ] f₂ x) →
105
(xs₁ >>= f₁) ∼[ k ] (xs₂ >>= f₂)
129
106
>>=-cong {ℓ} {xs₁ = xs₁} {xs₂} {f₁} {f₂} xs₁≈xs₂ f₁≈f₂ {x} =
130
x ∈ (xs₁ >>= f₁) ⇿⟨ sym $ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
131
Any (λ y → x ∈ f₁ y) xs₁ ≈⟨ Any-cong (λ x → f₁≈f₂ x) xs₁≈xs₂ ⟩
132
Any (λ y → x ∈ f₂ y) xs₂ ⇿⟨ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
107
x ∈ (xs₁ >>= f₁) ↔⟨ sym $ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
108
Any (λ y → x ∈ f₁ y) xs₁ ∼⟨ Any-cong (λ x → f₁≈f₂ x) xs₁≈xs₂ ⟩
109
Any (λ y → x ∈ f₂ y) xs₂ ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
133
110
x ∈ (xs₂ >>= f₂) ∎
134
where open Inv.EquationalReasoning
111
where open Related.EquationalReasoning
136
113
-- _⊛_ is a congruence.
138
115
⊛-cong : ∀ {ℓ k} {A B : Set ℓ} {fs₁ fs₂ : List (A → B)} {xs₁ xs₂} →
139
fs₁ ≈[ k ] fs₂ → xs₁ ≈[ k ] xs₂ → fs₁ ⊛ xs₁ ≈[ k ] fs₂ ⊛ xs₂
116
fs₁ ∼[ k ] fs₂ → xs₁ ∼[ k ] xs₂ → fs₁ ⊛ xs₁ ∼[ k ] fs₂ ⊛ xs₂
140
117
⊛-cong fs₁≈fs₂ xs₁≈xs₂ =
141
118
>>=-cong fs₁≈fs₂ λ f →
142
119
>>=-cong xs₁≈xs₂ λ x →
144
where open Inv.EquationalReasoning
121
where open Related.EquationalReasoning
146
123
-- _⊗_ is a congruence.
148
125
⊗-cong : ∀ {ℓ k} {A B : Set ℓ} {xs₁ xs₂ : List A} {ys₁ ys₂ : List B} →
149
xs₁ ≈[ k ] xs₂ → ys₁ ≈[ k ] ys₂ →
150
(xs₁ ⊗ ys₁) ≈[ k ] (xs₂ ⊗ ys₂)
126
xs₁ ∼[ k ] xs₂ → ys₁ ∼[ k ] ys₂ →
127
(xs₁ ⊗ ys₁) ∼[ k ] (xs₂ ⊗ ys₂)
151
128
⊗-cong {ℓ} xs₁≈xs₂ ys₁≈ys₂ =
152
⊛-cong (⊛-cong (Eq.refl {x = [ _,_ {a = ℓ} {b = ℓ} ]})
129
⊛-cong (⊛-cong (Ord.refl {x = [ _,_ {a = ℓ} {b = ℓ} ]})
133
------------------------------------------------------------------------
136
-- _++_ and [] form a commutative monoid, with either bag or set
137
-- equality as the underlying equality.
139
commutativeMonoid : ∀ {a} → Symmetric-kind → Set a →
140
CommutativeMonoid _ _
141
commutativeMonoid {a} k A = record
143
; _≈_ = λ xs ys → xs ∼[ ⌊ k ⌋ ] ys
146
; isCommutativeMonoid = record
147
{ isSemigroup = record
148
{ isEquivalence = Eq.isEquivalence
149
; assoc = λ xs ys zs →
150
Eq.reflexive (ListMonoid.assoc xs ys zs)
153
; identityˡ = λ xs {x} → x ∈ xs ∎
154
; comm = λ xs ys {x} →
155
x ∈ xs ++ ys ↔⟨ ++↔++ {a = a} {p = a} xs ys ⟩
159
where open Related.EquationalReasoning
161
-- The only list which is bag or set equal to the empty list (or a
162
-- subset or subbag of the list) is the empty list itself.
164
empty-unique : ∀ {k a} {A : Set a} {xs : List A} →
165
xs ∼[ ⌊ k ⌋→ ] [] → xs ≡ []
166
empty-unique {xs = []} _ = P.refl
167
empty-unique {xs = _ ∷ _} ∷∼[] with ⇒→ ∷∼[] (here P.refl)
170
-- _++_ is idempotent (under set equality).
172
++-idempotent : ∀ {a} {A : Set a} →
173
Idempotent (λ (xs ys : List A) → xs ∼[ set ] ys) _++_
174
++-idempotent {a} xs {x} =
175
x ∈ xs ++ xs ∼⟨ FE.equivalence ([ id , id ]′ ∘ _⟨$⟩_ (Inverse.from $ ++↔ {a = a} {p = a}))
176
(_⟨$⟩_ (Inverse.to $ ++↔ {a = a} {p = a}) ∘ inj₁) ⟩
178
where open Related.EquationalReasoning
156
180
-- The list monad's bind distributes from the left over _++_.
158
182
>>=-left-distributive :
159
183
∀ {ℓ} {A B : Set ℓ} (xs : List A) {f g : A → List B} →
160
(xs >>= λ x → f x ++ g x) ≈[ bag ] (xs >>= f) ++ (xs >>= g)
184
(xs >>= λ x → f x ++ g x) ∼[ bag ] (xs >>= f) ++ (xs >>= g)
161
185
>>=-left-distributive {ℓ} xs {f} {g} {y} =
162
y ∈ (xs >>= λ x → f x ++ g x) ⇿⟨ sym $ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
163
Any (λ x → y ∈ f x ++ g x) xs ⇿⟨ sym (Any-cong (λ _ → ++⇿ {a = ℓ} {p = ℓ}) (_ ∎)) ⟩
164
Any (λ x → y ∈ f x ⊎ y ∈ g x) xs ⇿⟨ sym $ ⊎⇿ {a = ℓ} {p = ℓ} {q = ℓ} ⟩
165
(Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs) ⇿⟨ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟨ ×⊎.+-cong {ℓ = ℓ} ⟩ >>=⇿ {ℓ = ℓ} {p = ℓ} ⟩
166
(y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g)) ⇿⟨ ++⇿ {a = ℓ} {p = ℓ} ⟩
186
y ∈ (xs >>= λ x → f x ++ g x) ↔⟨ sym $ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
187
Any (λ x → y ∈ f x ++ g x) xs ↔⟨ sym (Any-cong (λ _ → ++↔ {a = ℓ} {p = ℓ}) (_ ∎)) ⟩
188
Any (λ x → y ∈ f x ⊎ y ∈ g x) xs ↔⟨ sym $ ⊎↔ {a = ℓ} {p = ℓ} {q = ℓ} ⟩
189
(Any (λ x → y ∈ f x) xs ⊎ Any (λ x → y ∈ g x) xs) ↔⟨ >>=↔ {ℓ = ℓ} {p = ℓ} ⟨ ×⊎.+-cong {ℓ = ℓ} ⟩ >>=↔ {ℓ = ℓ} {p = ℓ} ⟩
190
(y ∈ (xs >>= f) ⊎ y ∈ (xs >>= g)) ↔⟨ ++↔ {a = ℓ} {p = ℓ} ⟩
167
191
y ∈ (xs >>= f) ++ (xs >>= g) ∎
168
where open Inv.EquationalReasoning
192
where open Related.EquationalReasoning
170
194
-- The same applies to _⊛_.
172
196
⊛-left-distributive :
173
197
∀ {ℓ} {A B : Set ℓ} (fs : List (A → B)) xs₁ xs₂ →
174
fs ⊛ (xs₁ ++ xs₂) ≈[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
198
fs ⊛ (xs₁ ++ xs₂) ∼[ bag ] (fs ⊛ xs₁) ++ (fs ⊛ xs₂)
175
199
⊛-left-distributive {B = B} fs xs₁ xs₂ = begin
176
200
fs ⊛ (xs₁ ++ xs₂) ≡⟨ P.refl ⟩
177
201
(fs >>= λ f → xs₁ ++ xs₂ >>= return ∘ f) ≡⟨ (LP.Monad.cong (P.refl {x = fs}) λ f →
194
218
∀ {a} {A : Set a} {x : A} →
195
¬ (∀ {xs ys} → x ∷ xs ≈[ set ] x ∷ ys → xs ≈[ set ] ys)
219
¬ (∀ {xs ys} → x ∷ xs ∼[ set ] x ∷ ys → xs ∼[ set ] ys)
196
220
¬-drop-cons {x = x} drop-cons
197
with FE.Equivalent.to x≈[] ⟨$⟩ here P.refl
221
with FE.Equivalence.to x∼[] ⟨$⟩ here P.refl
199
x,x≈x : (x ∷ x ∷ []) ≈[ set ] [ x ]
223
x,x≈x : (x ∷ x ∷ []) ∼[ set ] [ x ]
200
224
x,x≈x = ++-idempotent [ x ]
202
x≈[] : [ x ] ≈[ set ] []
203
x≈[] = drop-cons x,x≈x
226
x∼[] : [ x ] ∼[ set ] []
227
x∼[] = drop-cons x,x≈x
206
230
-- However, the corresponding property does hold for bag equality.
208
232
drop-cons : ∀ {a} {A : Set a} {x : A} {xs ys} →
209
x ∷ xs ≈[ bag ] x ∷ ys → xs ≈[ bag ] ys
210
drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys {z} =
212
(∃ λ (z∈x∷xs : z ∈ x ∷ xs) → There z∈x∷xs) ⇿⟨ Σ.⇿ x∷xs≈x∷ys′ x∷xs≈x∷ys′-preserves-There ⟩
213
(∃ λ (z∈x∷ys : z ∈ x ∷ ys) → There z∈x∷ys) ⇿⟨ sym $ lemma ys ⟩
233
x ∷ xs ∼[ bag ] x ∷ ys → xs ∼[ bag ] ys
234
drop-cons {A = A} {x} {xs} {ys} x∷xs≈x∷ys {z} = record
235
{ to = P.→-to-⟶ $ f x∷xs≈x∷ys
236
; from = P.→-to-⟶ $ f $ Inv.sym x∷xs≈x∷ys
237
; inverse-of = record
238
{ left-inverse-of = f∘f x∷xs≈x∷ys
239
; right-inverse-of = f∘f $ Inv.sym x∷xs≈x∷ys
216
open Inv.EquationalReasoning
218
-- Inhabited for there but not here.
220
There : ∀ {z : A} {xs} → z ∈ xs → Set
224
-- There is proof irrelevant.
226
proof-irrelevance : ∀ {z xs} {z∈xs : z ∈ xs}
227
(p q : There z∈xs) → p ≡ q
228
proof-irrelevance {z∈xs = here _} () ()
229
proof-irrelevance {z∈xs = there _} _ _ = P.refl
233
lemma : ∀ xs → z ∈ xs ⇿ (∃ λ (z∈x∷xs : z ∈ x ∷ xs) → There z∈x∷xs)
236
; from = P.→-to-⟶ from
237
; inverse-of = record
238
{ left-inverse-of = λ _ → P.refl
239
; right-inverse-of = to∘from
243
to : z ∈ xs → (∃ λ (z∈x∷xs : z ∈ x ∷ xs) → There z∈x∷xs)
244
to z∈xs = (there z∈xs , _)
246
from : (∃ λ (z∈x∷xs : z ∈ x ∷ xs) → There z∈x∷xs) → z ∈ xs
248
from (there z∈xs , _) = z∈xs
250
to∘from : ∀ p → to (from p) ≡ p
251
to∘from (here z≡x , ())
252
to∘from (there z∈xs , _) = P.refl
254
-- The isomorphisms x∷xs≈x∷ys may not preserve There, because they
255
-- could map here P.refl to something other than here P.refl.
256
-- However, we can construct isomorphisms which do preserve There:
258
x∷xs≈x∷ys′ : x ∷ xs ≈[ bag ] x ∷ ys
260
{ to = P.→-to-⟶ $ f x∷xs≈x∷ys
261
; from = P.→-to-⟶ $ f $ Inv.sym x∷xs≈x∷ys
262
; inverse-of = record
263
{ left-inverse-of = f∘f x∷xs≈x∷ys
264
; right-inverse-of = f∘f $ Inv.sym x∷xs≈x∷ys
268
f : ∀ {xs ys} → x ∷ xs ≈[ bag ] x ∷ ys →
269
∀ {z} → z ∈ x ∷ xs → z ∈ x ∷ ys
270
f x∷xs≈x∷ys (here P.refl) = here P.refl
271
f x∷xs≈x∷ys (there z∈xs) with Inverse.to x∷xs≈x∷ys ⟨$⟩ there z∈xs
272
... | there z∈ys = there z∈ys
273
... | here P.refl = Inverse.to x∷xs≈x∷ys ⟨$⟩ here P.refl
276
(x∷xs≈x∷ys : x ∷ xs ≈[ bag ] x ∷ ys) →
277
∀ {z} (p : z ∈ x ∷ xs) →
278
f (Inv.sym x∷xs≈x∷ys) (f x∷xs≈x∷ys p) ≡ p
279
f∘f x∷xs≈x∷ys (here P.refl) = P.refl
280
f∘f x∷xs≈x∷ys (there z∈xs)
281
with Inverse.to x∷xs≈x∷ys ⟨$⟩ there z∈xs
282
| Inverse.left-inverse-of x∷xs≈x∷ys (there z∈xs)
283
... | there z∈ys | left rewrite left = P.refl
284
... | here P.refl | left
285
with Inverse.to x∷xs≈x∷ys ⟨$⟩ here P.refl
286
| Inverse.left-inverse-of x∷xs≈x∷ys (here P.refl)
287
... | there z∈xs′ | left′ rewrite left′ = left
288
... | here P.refl | left′ rewrite left′ = left
290
x∷xs≈x∷ys′-preserves-There :
291
∀ {z} {z∈x∷xs : z ∈ x ∷ xs} →
292
There z∈x∷xs ⇿ There (Inverse.to x∷xs≈x∷ys′ ⟨$⟩ z∈x∷xs)
293
x∷xs≈x∷ys′-preserves-There {z∈x∷xs = z∈x∷xs} = record
294
{ to = P.→-to-⟶ $ to z∈x∷xs
295
; from = P.→-to-⟶ $ from z∈x∷xs
296
; inverse-of = record
297
{ left-inverse-of = λ _ → proof-irrelevance _ _
298
; right-inverse-of = λ _ → proof-irrelevance _ _
302
open P.≡-Reasoning renaming (_∎ to _□)
304
to : ∀ {z} (z∈x∷xs : z ∈ x ∷ xs) →
305
There z∈x∷xs → There (Inverse.to x∷xs≈x∷ys′ ⟨$⟩ z∈x∷xs)
307
to (there z∈) _ with P.inspect (Inverse.to x∷xs≈x∷ys ⟨$⟩ there z∈)
308
... | there _ with-≡ eq rewrite eq = _
309
... | here P.refl with-≡ eq rewrite eq
310
with P.inspect (Inverse.to x∷xs≈x∷ys ⟨$⟩ here P.refl)
311
... | there _ with-≡ eq′ rewrite eq′ = _
312
... | here P.refl with-≡ eq′ rewrite eq′
314
there z∈ ≡⟨ P.sym $ Inverse.left-inverse-of x∷xs≈x∷ys _ ⟩
315
Inverse.from x∷xs≈x∷ys ⟨$⟩ (Inverse.to x∷xs≈x∷ys ⟨$⟩ there z∈) ≡⟨ P.cong (_⟨$⟩_ (Inverse.from x∷xs≈x∷ys)) eq ⟩
316
Inverse.from x∷xs≈x∷ys ⟨$⟩ here P.refl ≡⟨ P.cong (_⟨$⟩_ (Inverse.from x∷xs≈x∷ys)) (P.sym eq′) ⟩
317
Inverse.from x∷xs≈x∷ys ⟨$⟩ (Inverse.to x∷xs≈x∷ys ⟨$⟩ here P.refl) ≡⟨ Inverse.left-inverse-of x∷xs≈x∷ys _ ⟩
318
Any.here {xs = xs} (P.refl {x = x}) □
321
from : ∀ {z} (z∈x∷xs : z ∈ x ∷ xs) →
322
There (Inverse.to x∷xs≈x∷ys′ ⟨$⟩ z∈x∷xs) → There z∈x∷xs
323
from (here P.refl) ()
324
from (there z∈xs) _ = _
246
f : ∀ {xs ys z} → (z ∈ x ∷ xs) ↔ (z ∈ x ∷ ys) → z ∈ xs → z ∈ ys
247
f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
248
f inv z∈xs | there z∈ys | left⁺ = z∈ys
249
f inv z∈xs | here z≡x | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
250
f inv z∈xs | here z≡x | left⁺ | there z∈ys | left⁰ = z∈ys
251
f inv z∈xs | here P.refl | left⁺ | here P.refl | left⁰ with begin
252
here P.refl ≡⟨ P.sym left⁰ ⟩
253
from inv ⟨$⟩ here P.refl ≡⟨ left⁺ ⟩
258
(inv : (z ∈ x ∷ xs) ↔ (z ∈ x ∷ ys)) (p : z ∈ xs) →
259
f (Inv.sym inv) (f inv p) ≡ p
260
f∘f inv z∈xs with to inv ⟨$⟩ there z∈xs | left-inverse-of inv (there z∈xs)
261
f∘f inv z∈xs | there z∈ys | left⁺ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
262
f∘f inv z∈xs | there z∈ys | P.refl | .(there z∈xs) | _ = P.refl
263
f∘f inv z∈xs | here z≡x | left⁺ with to inv ⟨$⟩ here z≡x | left-inverse-of inv (here z≡x)
264
f∘f inv z∈xs | here z≡x | left⁺ | there z∈ys | left⁰ with from inv ⟨$⟩ there z∈ys | right-inverse-of inv (there z∈ys)
265
f∘f inv z∈xs | here z≡x | left⁺ | there z∈ys | P.refl | .(here z≡x) | _ with from inv ⟨$⟩ here z≡x
266
| right-inverse-of inv (here z≡x)
267
f∘f inv z∈xs | here z≡x | P.refl | there z∈ys | P.refl | .(here z≡x) | _ | .(there z∈xs) | _ = P.refl
268
f∘f inv z∈xs | here P.refl | left⁺ | here P.refl | left⁰ with begin
269
here P.refl ≡⟨ P.sym left⁰ ⟩
270
from inv ⟨$⟩ here P.refl ≡⟨ left⁺ ⟩
added
removed
src/Data/List/Any/BagAndSetEquality.agda
