/
M.lean
301 lines (257 loc) · 11.2 KB
/
M.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
/-
Copyright (c) 2018 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad, Mario Carneiro, Simon Hudon
-/
import data.pfunctor.univariate
import data.pfunctor.multivariate.basic
/-!
# The M construction as a multivariate polynomial functor.
M types are potentially infinite tree-like structures. They are defined
as the greatest fixpoint of a polynomial functor.
## Main definitions
* `M.mk` - constructor
* `M.dest` - destructor
* `M.corec` - corecursor: useful for formulating infinite, productive computations
* `M.bisim` - bisimulation: proof technique to show the equality of infinite objects
## Implementation notes
Dual view of M-types:
* `Mp`: polynomial functor
* `M`: greatest fixed point of a polynomial functor
Specifically, we define the polynomial functor `Mp` as:
* A := a possibly infinite tree-like structure without information in the nodes
* B := given the tree-like structure `t`, `B t` is a valid path
from the root of `t` to any given node.
As a result `Mp.obj α` is made of a dataless tree and a function from
its valid paths to values of `α`
The difference with the polynomial functor of an initial algebra is
that `A` is a possibly infinite tree.
## Reference
* [Jeremy Avigad, Mario M. Carneiro and Simon Hudon, *Data Types as Quotients of Polynomial Functors*][avigad-carneiro-hudon2019]
-/
universe u
open_locale mvfunctor
namespace mvpfunctor
open typevec
variables {n : ℕ} (P : mvpfunctor.{u} (n+1))
/-- A path from the root of a tree to one of its node -/
inductive M.path : P.last.M → fin2 n → Type u
| root (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : pfunctor.M.dest x = ⟨a, f⟩)
(i : fin2 n) (c : P.drop.B a i) :
M.path x i
| child (x : P.last.M) (a : P.A) (f : P.last.B a → P.last.M) (h : pfunctor.M.dest x = ⟨a, f⟩)
(j : P.last.B a) (i : fin2 n) (c : M.path (f j) i) :
M.path x i
instance M.path.inhabited (x : P.last.M) {i} [inhabited (P.drop.B x.head i)] :
inhabited (M.path P x i) :=
⟨ M.path.root _ (pfunctor.M.head x) (pfunctor.M.children x)
(pfunctor.M.cases_on' x $
by intros; simp [pfunctor.M.dest_mk]; ext; rw pfunctor.M.children_mk; refl) _
(default _) ⟩
/-- Polynomial functor of the M-type of `P`. `A` is a data-less
possibly infinite tree whereas, for a given `a : A`, `B a` is a valid
path in tree `a` so that `Wp.obj α` is made of a tree and a function
from its valid paths to the values it contains -/
def Mp : mvpfunctor n :=
{ A := P.last.M, B := M.path P }
/-- `n`-ary M-type for `P` -/
def M (α : typevec n) : Type* := P.Mp.obj α
instance mvfunctor_M : mvfunctor P.M := by delta M; apply_instance
instance inhabited_M {α : typevec _}
[I : inhabited P.A]
[Π (i : fin2 n), inhabited (α i)] :
inhabited (P.M α) :=
@obj.inhabited _ (Mp P) _ (@pfunctor.M.inhabited P.last I) _
/-- construct through corecursion the shape of an M-type
without its contents -/
def M.corec_shape {β : Type u}
(g₀ : β → P.A)
(g₂ : Π b : β, P.last.B (g₀ b) → β) :
β → P.last.M :=
pfunctor.M.corec (λ b, ⟨g₀ b, g₂ b⟩)
/-- Proof of type equality as an arrow -/
def cast_dropB {a a' : P.A} (h : a = a') : P.drop.B a ⟹ P.drop.B a' :=
λ i b, eq.rec_on h b
/-- Proof of type equality as a function -/
def cast_lastB {a a' : P.A} (h : a = a') : P.last.B a → P.last.B a' :=
λ b, eq.rec_on h b
/-- Using corecursion, construct the contents of an M-type -/
def M.corec_contents {α : typevec.{u} n} {β : Type u}
(g₀ : β → P.A)
(g₁ : Π b : β, P.drop.B (g₀ b) ⟹ α)
(g₂ : Π b : β, P.last.B (g₀ b) → β) :
Π x b, x = M.corec_shape P g₀ g₂ b → M.path P x ⟹ α
| ._ b h ._ (M.path.root x a f h' i c) :=
have a = g₀ b,
by { rw [h, M.corec_shape, pfunctor.M.dest_corec] at h', cases h', refl },
g₁ b i (P.cast_dropB this i c)
| ._ b h ._ (M.path.child x a f h' j i c) :=
have h₀ : a = g₀ b,
by { rw [h, M.corec_shape, pfunctor.M.dest_corec] at h', cases h', refl },
have h₁ : f j = M.corec_shape P g₀ g₂ (g₂ b (cast_lastB P h₀ j)),
by { rw [h, M.corec_shape, pfunctor.M.dest_corec] at h', cases h', refl },
M.corec_contents (f j) (g₂ b (P.cast_lastB h₀ j)) h₁ i c
/-- Corecursor for M-type of `P` -/
def M.corec' {α : typevec n} {β : Type u}
(g₀ : β → P.A)
(g₁ : Π b : β, P.drop.B (g₀ b) ⟹ α)
(g₂ : Π b : β, P.last.B (g₀ b) → β) :
β → P.M α :=
λ b, ⟨M.corec_shape P g₀ g₂ b, M.corec_contents P g₀ g₁ g₂ _ _ rfl⟩
/-- Corecursor for M-type of `P` -/
def M.corec {α : typevec n} {β : Type u} (g : β → P.obj (α.append1 β)) :
β → P.M α :=
M.corec' P
(λ b, (g b).fst)
(λ b, drop_fun (g b).snd)
(λ b, last_fun (g b).snd)
/-- Implementation of destructor for M-type of `P` -/
def M.path_dest_left {α : typevec n} {x : P.last.M}
{a : P.A} {f : P.last.B a → P.last.M} (h : pfunctor.M.dest x = ⟨a, f⟩)
(f' : M.path P x ⟹ α) :
P.drop.B a ⟹ α :=
λ i c, f' i (M.path.root x a f h i c)
/-- Implementation of destructor for M-type of `P` -/
def M.path_dest_right {α : typevec n} {x : P.last.M}
{a : P.A} {f : P.last.B a → P.last.M} (h : pfunctor.M.dest x = ⟨a, f⟩)
(f' : M.path P x ⟹ α) :
Π j : P.last.B a, M.path P (f j) ⟹ α :=
λ j i c, f' i (M.path.child x a f h j i c)
/-- Destructor for M-type of `P` -/
def M.dest' {α : typevec n} {x : P.last.M}
{a : P.A} {f : P.last.B a → P.last.M} (h : pfunctor.M.dest x = ⟨a, f⟩)
(f' : M.path P x ⟹ α) :
P.obj (α.append1 (P.M α)) :=
⟨a, split_fun (M.path_dest_left P h f') (λ x, ⟨f x, M.path_dest_right P h f' x⟩)⟩
/-- Destructor for M-types -/
def M.dest {α : typevec n} (x : P.M α) : P.obj (α ::: P.M α) :=
M.dest' P (sigma.eta $ pfunctor.M.dest x.fst).symm x.snd
/-- Constructor for M-types -/
def M.mk {α : typevec n} : P.obj (α.append1 (P.M α)) → P.M α :=
M.corec _ (λ i, append_fun id (M.dest P) <$$> i)
theorem M.dest'_eq_dest' {α : typevec n} {x : P.last.M}
{a₁ : P.A} {f₁ : P.last.B a₁ → P.last.M} (h₁ : pfunctor.M.dest x = ⟨a₁, f₁⟩)
{a₂ : P.A} {f₂ : P.last.B a₂ → P.last.M} (h₂ : pfunctor.M.dest x = ⟨a₂, f₂⟩)
(f' : M.path P x ⟹ α) : M.dest' P h₁ f' = M.dest' P h₂ f' :=
by cases h₁.symm.trans h₂; refl
theorem M.dest_eq_dest' {α : typevec n} {x : P.last.M}
{a : P.A} {f : P.last.B a → P.last.M} (h : pfunctor.M.dest x = ⟨a, f⟩)
(f' : M.path P x ⟹ α) : M.dest P ⟨x, f'⟩ = M.dest' P h f' :=
M.dest'_eq_dest' _ _ _ _
theorem M.dest_corec' {α : typevec.{u} n} {β : Type u}
(g₀ : β → P.A)
(g₁ : Π b : β, P.drop.B (g₀ b) ⟹ α)
(g₂ : Π b : β, P.last.B (g₀ b) → β)
(x : β) :
M.dest P (M.corec' P g₀ g₁ g₂ x) =
⟨g₀ x, split_fun (g₁ x) (M.corec' P g₀ g₁ g₂ ∘ (g₂ x))⟩ :=
rfl
theorem M.dest_corec {α : typevec n} {β : Type u} (g : β → P.obj (α.append1 β)) (x : β) :
M.dest P (M.corec P g x) = append_fun id (M.corec P g) <$$> g x :=
begin
transitivity, apply M.dest_corec',
cases g x with a f, dsimp,
rw mvpfunctor.map_eq, congr,
conv { to_rhs, rw [←split_drop_fun_last_fun f, append_fun_comp_split_fun] },
refl
end
lemma M.bisim_lemma {α : typevec n}
{a₁ : (Mp P).A} {f₁ : (Mp P).B a₁ ⟹ α}
{a' : P.A} {f' : (P.B a').drop ⟹ α} {f₁' : (P.B a').last → M P α}
(e₁ : M.dest P ⟨a₁, f₁⟩ = ⟨a', split_fun f' f₁'⟩) :
∃ g₁' (e₁' : pfunctor.M.dest a₁ = ⟨a', g₁'⟩),
f' = M.path_dest_left P e₁' f₁ ∧
f₁' = λ (x : (last P).B a'),
⟨g₁' x, M.path_dest_right P e₁' f₁ x⟩ :=
begin
generalize_hyp ef : @split_fun n _ (append1 α (M P α)) f' f₁' = ff at e₁,
cases e₁' : pfunctor.M.dest a₁ with a₁' g₁',
rw M.dest_eq_dest' _ e₁' at e₁,
cases e₁, exact ⟨_, e₁', split_fun_inj ef⟩,
end
theorem M.bisim {α : typevec n} (R : P.M α → P.M α → Prop)
(h : ∀ x y, R x y → ∃ a f f₁ f₂,
M.dest P x = ⟨a, split_fun f f₁⟩ ∧
M.dest P y = ⟨a, split_fun f f₂⟩ ∧
∀ i, R (f₁ i) (f₂ i))
(x y) (r : R x y) : x = y :=
begin
cases x with a₁ f₁,
cases y with a₂ f₂,
dsimp [Mp] at *,
have : a₁ = a₂, {
refine pfunctor.M.bisim
(λ a₁ a₂, ∃ x y, R x y ∧ x.1 = a₁ ∧ y.1 = a₂) _ _ _
⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩,
rintro _ _ ⟨⟨a₁, f₁⟩, ⟨a₂, f₂⟩, r, rfl, rfl⟩,
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h'⟩,
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩,
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', _, rfl⟩,
rw [e₁', e₂'],
exact ⟨_, _, _, rfl, rfl, λ b, ⟨_, _, h' b, rfl, rfl⟩⟩ },
subst this, congr, ext i p,
induction p with x a f h' i c x a f h' i c p IH generalizing f₁ f₂;
try {
rcases h _ _ r with ⟨a', f', f₁', f₂', e₁, e₂, h''⟩,
rcases M.bisim_lemma P e₁ with ⟨g₁', e₁', rfl, rfl⟩,
rcases M.bisim_lemma P e₂ with ⟨g₂', e₂', e₃, rfl⟩,
cases h'.symm.trans e₁',
cases h'.symm.trans e₂' },
{ exact (congr_fun (congr_fun e₃ i) c : _) },
{ exact IH _ _ (h'' _) }
end
theorem M.bisim₀ {α : typevec n} (R : P.M α → P.M α → Prop)
(h₀ : equivalence R)
(h : ∀ x y, R x y →
(id ::: quot.mk R) <$$> M.dest _ x = (id ::: quot.mk R) <$$> M.dest _ y)
(x y) (r : R x y) : x = y :=
begin
apply M.bisim P R _ _ _ r, clear r x y,
introv Hr, specialize h _ _ Hr, clear Hr,
rcases M.dest P x with ⟨ax,fx⟩, rcases M.dest P y with ⟨ay,fy⟩,
intro h, rw [map_eq,map_eq] at h, injection h with h₀ h₁, subst ay,
simp at h₁, clear h,
have Hdrop : drop_fun fx = drop_fun fy,
{ replace h₁ := congr_arg drop_fun h₁,
simpa using h₁, },
existsi [ax,drop_fun fx,last_fun fx,last_fun fy],
rw [split_drop_fun_last_fun,Hdrop,split_drop_fun_last_fun],
simp, intro i,
replace h₁ := congr_fun (congr_fun h₁ fin2.fz) i,
simp [(⊚),append_fun,split_fun] at h₁,
replace h₁ := quot.exact _ h₁,
rw relation.eqv_gen_iff_of_equivalence at h₁,
exact h₁, exact h₀
end
theorem M.bisim' {α : typevec n} (R : P.M α → P.M α → Prop)
(h : ∀ x y, R x y →
(id ::: quot.mk R) <$$> M.dest _ x = (id ::: quot.mk R) <$$> M.dest _ y)
(x y) (r : R x y) : x = y :=
begin
have := M.bisim₀ P (eqv_gen R) _ _,
{ solve_by_elim [eqv_gen.rel] },
{ apply eqv_gen.is_equivalence },
{ clear r x y, introv Hr,
have : ∀ x y, R x y → eqv_gen R x y := @eqv_gen.rel _ R,
induction Hr,
{ rw ← quot.factor_mk_eq R (eqv_gen R) this,
rwa [append_fun_comp_id,← mvfunctor.map_map,← mvfunctor.map_map,h] },
all_goals { cc } }
end
theorem M.dest_map {α β : typevec n} (g : α ⟹ β) (x : P.M α) :
M.dest P (g <$$> x) = append_fun g (λ x, g <$$> x) <$$> M.dest P x :=
begin
cases x with a f,
rw map_eq,
conv { to_rhs, rw [M.dest, M.dest', map_eq, append_fun_comp_split_fun] },
reflexivity
end
theorem M.map_dest {α β : typevec n} (g : α ::: P.M α ⟹ β ::: P.M β) (x : P.M α)
(h : ∀ x : P.M α, last_fun g x = (drop_fun g <$$> x : P.M β) ):
g <$$> M.dest P x = M.dest P (drop_fun g <$$> x) :=
begin
rw M.dest_map, congr,
apply eq_of_drop_last_eq; simp,
ext1, apply h
end
end mvpfunctor