-
Notifications
You must be signed in to change notification settings - Fork 11
/
example_relabeling.v
210 lines (187 loc) · 7.37 KB
/
example_relabeling.v
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
(* monae: Monadic equational reasoning in Coq *)
(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *)
From mathcomp Require Import all_ssreflect.
From mathcomp Require boolp.
Require Import preamble hierarchy monad_lib fail_lib state_lib.
(******************************************************************************)
(* Tree relabeling *)
(* *)
(* see Sect. 9 of J. Gibbons, R. Hinze, Just do it: simple monadic equational *)
(* reasoning, ICFP 2011 *)
(******************************************************************************)
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Local Open Scope monae_scope.
Section Tree.
Variable A : Type.
Inductive Tree := Tip (a : A) | Bin of Tree & Tree.
Fixpoint foldt B (f : A -> B) (g : B * B -> B) (t : Tree) : B :=
match t with
| Tip a => f a
| Bin t u => g (foldt f g t, foldt f g u)
end.
Section foldt_universal.
Variables (B : Type) (h : Tree -> B) (f : A -> B) (g : B * B -> B).
Hypothesis H1 : h \o Tip = f.
Hypothesis H2 : h \o uncurry Bin = g \o (fun x => (h x.1, h x.2)).
Lemma foldt_universal : h = foldt f g.
Proof.
rewrite boolp.funeqE; elim => [a|]; first by rewrite -H1.
by move=> t1 IH1 t2 IH2 /=; rewrite -IH1 -IH2 -(uncurryE Bin) -compE H2.
Qed.
End foldt_universal.
Definition size_Tree (t : Tree) := foldt (const 1) uaddn t.
Lemma size_Tree_Bin : size_Tree \o uncurry Bin = uaddn \o size_Tree^`2.
Proof. by rewrite boolp.funeqE; case. Qed.
Fixpoint labels (t : Tree) : seq A :=
match t with
| Tip a => [:: a]
| Bin t u => labels t ++ labels u
end.
End Tree.
Arguments Tip {A}.
Arguments Bin {A}.
Section tree_relabelling.
Variable Symbol : eqType. (* TODO: ideally, we would like a generic type here with a succ function *)
Variable M : failFreshMonad Symbol.
Variable q : pred (seq Symbol * seq Symbol).
Hypothesis promotable_q : promotable (@distinct _ M) q.
Local Open Scope mprog.
Definition relabel : Tree Symbol -> M (Tree Symbol) :=
foldt (M # Tip \o const fresh) (fmap (uncurry Bin) \o mpair).
Let drTip {A} : A -> M _ := (M # wrap) \o const fresh.
Let drBin {N : failMonad} : (N _ * N _ -> N _) :=
(fmap ucat) \o bassert q \o mpair.
(* extracting the distinct symbol list *)
Definition dlabels {N : failMonad} : Tree Symbol -> N (seq Symbol) :=
foldt (Ret \o wrap) drBin.
Lemma dlabelsC t u (m : _ -> _ -> M (seq Symbol * seq Symbol)%type) :
dlabels t >>= (fun x => relabel u >>= fun x0 => m x0 x) =
relabel u >>= (fun x0 => dlabels t >>= fun x => m x0 x).
Proof.
elim: t u m => [a u /= m|t1 H1 t2 H2 u m].
rewrite /dlabels /= bindretf.
by under [in RHS]eq_bind do rewrite bindretf.
rewrite (_ : dlabels _ = drBin (dlabels t1, dlabels t2)) //.
rewrite [in RHS]/drBin [in RHS]/bassert 2!compE ![in RHS]bindA.
transitivity (do x0 <- relabel u;
(do x <- dlabels t1;
do x <- (do x1 <- (do y <- dlabels t2; Ret (x, y));
(do x <- assert q x1; (Ret \o ucat) x));
m x0 x))%Do; last first.
bind_ext => u'; rewrite bind_fmap bindA; bind_ext => sS.
rewrite 4!bindA; bind_ext => x; rewrite 2!bindretf bindA.
by under eq_bind do rewrite bindretf.
rewrite -H1.
rewrite [in LHS]/drBin bind_fmap [in LHS]/bassert /= ![in LHS]bindA.
bind_ext => s.
rewrite !bindA.
transitivity (do x0 <- relabel u;
(do x <- dlabels t2; (do x <-
(do x1 <- Ret (s, x); (do x3 <- assert q x1; Ret (ucat x3)));
m x0 x)))%Do; last by bind_ext => y2; rewrite bindA.
rewrite -H2.
bind_ext => s'.
rewrite !bindretf.
rewrite assertE.
rewrite bindA.
transitivity (guard (q (s, s')) >>
(do x1 <- (Ret \o ucat) (s, s'); relabel u >>= (m^~ x1)))%Do.
bind_ext; case; by rewrite 2!bindretf.
rewrite guardsC; last exact: failfresh_bindmfail.
rewrite !bindA !bindretf !bindA.
bind_ext => u'.
rewrite bindA guardsC; last exact: failfresh_bindmfail.
by rewrite bindA bindretf.
Qed.
(* see gibbons2011icfp Sect. 9.3 *)
Lemma join_and_pairs :
(Join \o (M # mpair) \o mpair) \o ((fmap dlabels) \o relabel)^`2 =
(mpair \o Join^`2) \o ((fmap dlabels) \o relabel)^`2.
Proof.
rewrite boolp.funeqE => -[x1 x2].
rewrite 3!compE.
rewrite joinE.
rewrite fmapE.
rewrite 2![in RHS]compE.
rewrite [in RHS]/mpair.
rewrite [in LHS]/mpair.
move H : (fmap dlabels) => h.
rewrite /=.
rewrite 2![in RHS]joinE.
rewrite 3!bindA.
rewrite -H.
rewrite !fmapE.
rewrite 3!bindA.
bind_ext => {}x1.
rewrite 2!bindretf 2!bindA.
under eq_bind do rewrite 3!bindretf.
rewrite -dlabelsC.
bind_ext => ?.
rewrite /=.
rewrite bindA.
by under [in RHS]eq_bind do rewrite bindretf.
Qed.
(* first property of Sect. 9.3 *)
Lemma dlabels_relabel_is_fold : relabel >=> dlabels = foldt drTip drBin.
Proof.
apply foldt_universal.
(* relabel >=> dlabels \o Tip = drTip *)
rewrite kleisli_def -3!compA.
rewrite (_ : relabel \o Tip = (M # Tip) \o const fresh) //.
rewrite (compA (fmap dlabels)) -functor_o.
rewrite (_ : dlabels \o Tip = ret _ \o wrap) //.
rewrite functor_o.
by rewrite compA (compA Join) joinMret compidf.
(* relabel >=> dlabels \o Bin = drBin \o _ *)
rewrite [in LHS]kleisli_def -(compA _ relabel).
rewrite (_ : _ \o _ Bin =
(fmap (uncurry Bin)) \o mpair \o relabel^`2); last first.
by rewrite boolp.funeqE; case.
rewrite -(compA (fmap (uncurry Bin))) -compA (compA (fmap dlabels)) -functor_o.
rewrite (_ : _ \o _ Bin =
(fmap ucat) \o bassert q \o mpair \o dlabels^`2); last first.
by rewrite boolp.funeqE; case.
transitivity ((fmap ucat) \o Join \o (fmap (bassert q \o mpair)) \o mpair \o
(fmap dlabels \o relabel)^`2).
rewrite [in RHS]natural -3![in RHS]compA; congr (_ \o _).
rewrite -[in RHS]naturality_mpair 2![RHS]compA; congr (_ \o _).
by rewrite -[X in _ = X \o _]functor_o -[RHS]functor_o -compA.
rewrite -(compA (fmap ucat)) [X in Join \o X]functor_o (compA Join).
rewrite commutativity_of_assertions. (* first non-trivial step *)
rewrite -(compA _ Join) (compA _ (bassert q)).
rewrite -(compA _ _ mpair) -(compA _ (_ \o mpair)).
by rewrite join_and_pairs. (* second non-trivial step *)
Qed.
(* second property of Sect. 9.3 *)
Lemma symbols_size_is_fold :
symbols \o (@size_Tree Symbol) = foldt drTip drBin.
Proof.
apply foldt_universal.
by rewrite -compA (_ : @size_Tree Symbol \o _ = const 1) // symbols_prop1.
pose p := @distinct _ M.
transitivity (bassert p \o symbols \o @size_Tree Symbol \o uncurry Bin
: (_ -> M _)).
by rewrite bassert_symbols.
transitivity ((bassert p) \o symbols \o uaddn \o (@size_Tree Symbol)^`2
: (_ -> M _)).
by rewrite -[in LHS]compA -[in RHS]compA size_Tree_Bin.
transitivity (bassert p \o (fmap ucat) \o mpair \o (symbols \o (@size_Tree Symbol))^`2
: (_ -> M _)).
rewrite -2!compA (compA symbols) symbols_prop2.
by rewrite -(compA (_ \o mpair)) (compA (bassert p)).
transitivity ((fmap ucat) \o bassert q \o mpair \o (bassert p \o symbols \o (@size_Tree Symbol))^`2
: (_ -> M _)).
(* assert p distributes over concatenation *)
by rewrite (promote_assert_sufficient_condition (@failfresh_bindmfail _ M) promotable_q).
transitivity ((fmap ucat) \o bassert q \o mpair \o (symbols \o (@size_Tree Symbol))^`2
: (_ -> M _)).
by rewrite bassert_symbols.
by [].
Qed.
(* main claim *)
Lemma dlabels_relabel_never_fails :
relabel >=> dlabels = symbols \o @size_Tree Symbol.
Proof. by rewrite dlabels_relabel_is_fold symbols_size_is_fold. Qed.
End tree_relabelling.