-
Notifications
You must be signed in to change notification settings - Fork 232
/
MonoidSolver.agda
270 lines (233 loc) · 10.4 KB
/
MonoidSolver.agda
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
------------------------------------------------------------------------
-- The Agda standard library
--
-- Reflection-based solver for monoid equalities
------------------------------------------------------------------------
--
-- This solver automates the construction of proofs of equivalences
-- between monoid expressions.
-- When called like so:
--
-- proof : ∀ x y z → (x ∙ y) ∙ z ≈ x ∙ (y ∙ z) ∙ ε
-- proof x y z = solve mon
--
-- The following diagram describes what happens under the hood:
--
-- ┌▸x ∙ (y ∙ (z ∙ ε)) ════ x ∙ (y ∙ (z ∙ ε))◂┐
-- │ ║ ║ │
-- │ ║ ║ │
-- [_⇓] ║ ║ [_⇓]
-- ╱ ║ ║ ╲
-- ╱ ║ ║ ╲
-- (x ∙′ y) ∙′ z homo homo x ∙′ (y ∙′ z) ∙′ ε′
-- ▴ ╲ ║ ║ ╱ ▴
-- │ ╲ ║ ║ ╱ │
-- │ [_↓] ║ ║ [_↓] │
-- │ │ ║ ║ │ │
-- │ │ ║ ║ │ │
-- │ └───▸(x ∙ y) ∙ z x ∙ (y ∙ z) ∙ ε◂─┘ │
-- │ │ │ │
-- │ │ │ │
-- └────reflection────┘ └───reflection──────┘
--
-- The actual output—the proof constructed by the solver—is represented
-- by the double-lined path (══).
--
-- We start at the bottom, with our two expressions.
-- Through reflection, we convert these two expressions to their AST
-- representations, in the Expr type.
-- We then can evaluate the AST in two ways: one simply gives us back
-- the two expressions we put in ([_↓]), and the other normalises
-- ([_⇓]).
-- We use the homo function to prove equivalence between these two
-- forms: joining up these two proofs gives us the desired overall
-- proof.
-- Note: What's going on with the Monoid parameter?
--
-- This module is not parameterised over a monoid, which is contrary
-- to what you might expect. Instead, we take the monoid record as an
-- argument to the solve macro, and then pass it around as an
-- argument wherever we need it.
--
-- We need to get the monoid record at the call site, not the import
-- site, to ensure that it's consistent with the rest of the context.
-- For instance, if we wanted to produce `x ∙ y` using the monoid record
-- as imported, we would run into problems:
-- * If we tried to just reflect on the expression itself
-- (quoteTerm (x ∙ y)) we would likely get some de Bruijn indices
-- wrong (in x and y), and ∙ might not even be in scope where the
-- user wants us to solve! If they're solving an expression like
-- x + (y + z), they can pass in the +-0-monoid, but don't have to
-- open it themselves.
-- * If instead we tried to construct a term which accesses the _∙_
-- field on the reflection of the record, we'd run into similar
-- problems again. While the record is a parameter for us, it might
-- not be for the user.
-- Basically, we need the Monoid we're looking at to be exactly the
-- same as the one the user is looking at, and in order to do that we
-- quote it at the call site.
{-# OPTIONS --cubical-compatible --safe #-}
module Tactic.MonoidSolver where
open import Algebra
open import Function.Base using (_⟨_⟩_)
open import Data.Bool.Base as Bool using (Bool; _∨_; if_then_else_)
open import Data.Maybe.Base as Maybe using (Maybe; just; nothing; maybe)
open import Data.List.Base as List using (List; _∷_; [])
open import Data.Nat.Base as ℕ using (ℕ; suc; zero)
open import Data.Product.Base as Product using (_×_; _,_)
open import Reflection.AST
open import Reflection.AST.Term
open import Reflection.AST.Argument
import Reflection.AST.Name as Name
open import Reflection.TCM
open import Reflection.TCM.Syntax
import Relation.Binary.Reasoning.Setoid as ≈-Reasoning
------------------------------------------------------------------------
-- The Expr type with homomorphism proofs
------------------------------------------------------------------------
infixl 7 _∙′_
data Expr {a} (A : Set a) : Set a where
_∙′_ : Expr A → Expr A → Expr A
ε′ : Expr A
[_↑] : A → Expr A
module _ {m₁ m₂} (monoid : Monoid m₁ m₂) where
open Monoid monoid
open ≈-Reasoning setoid
-- Convert the AST to an expression (i.e. evaluate it) without
-- normalising.
[_↓] : Expr Carrier → Carrier
[ x ∙′ y ↓] = [ x ↓] ∙ [ y ↓]
[ ε′ ↓] = ε
[ [ x ↑] ↓] = x
-- Convert an AST to an expression (i.e. evaluate it) while
-- normalising.
--
-- This first function actually converts an AST to the Cayley
-- representation of the underlying monoid.
-- This obeys the monoid laws up to beta-eta equality, which is the
-- property which gives us the "normalising" behaviour we want.
[_⇓]′ : Expr Carrier → Carrier → Carrier
[ x ∙′ y ⇓]′ z = [ x ⇓]′ ([ y ⇓]′ z)
[ ε′ ⇓]′ y = y
[ [ x ↑] ⇓]′ y = x ∙ y
[_⇓] : Expr Carrier → Carrier
[ x ⇓] = [ x ⇓]′ ε
homo′ : ∀ x y → [ x ⇓] ∙ y ≈ [ x ⇓]′ y
homo′ ε′ y = identityˡ y
homo′ [ x ↑] y = ∙-congʳ (identityʳ x)
homo′ (x ∙′ y) z = begin
[ x ∙′ y ⇓] ∙ z ≡⟨⟩
[ x ⇓]′ [ y ⇓] ∙ z ≈⟨ ∙-congʳ (homo′ x [ y ⇓]) ⟨
([ x ⇓] ∙ [ y ⇓]) ∙ z ≈⟨ assoc [ x ⇓] [ y ⇓] z ⟩
[ x ⇓] ∙ ([ y ⇓] ∙ z) ≈⟨ ∙-congˡ (homo′ y z) ⟩
[ x ⇓] ∙ ([ y ⇓]′ z) ≈⟨ homo′ x ([ y ⇓]′ z) ⟩
[ x ⇓]′ ([ y ⇓]′ z) ∎
homo : ∀ x → [ x ⇓] ≈ [ x ↓]
homo ε′ = refl
homo [ x ↑] = identityʳ x
homo (x ∙′ y) = begin
[ x ∙′ y ⇓] ≡⟨⟩
[ x ⇓]′ [ y ⇓] ≈⟨ homo′ x [ y ⇓] ⟨
[ x ⇓] ∙ [ y ⇓] ≈⟨ ∙-cong (homo x) (homo y) ⟩
[ x ↓] ∙ [ y ↓] ∎
------------------------------------------------------------------------
-- Helpers for reflection
------------------------------------------------------------------------
getArgs : Term → Maybe (Term × Term)
getArgs (def _ xs) = go xs
where
go : List (Arg Term) → Maybe (Term × Term)
go (vArg x ∷ vArg y ∷ []) = just (x , y)
go (x ∷ xs) = go xs
go _ = nothing
getArgs _ = nothing
------------------------------------------------------------------------
-- Getting monoid names
------------------------------------------------------------------------
-- We try to be flexible here, by matching two kinds of names.
-- The first is the field accessor for the monoid record itself.
-- However, users will likely want to use the solver with
-- expressions like:
--
-- xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
--
-- So we also evaluate the field accessor to find functions like ++.
record MonoidNames : Set where
field
is-∙ : Name → Bool
is-ε : Name → Bool
buildMatcher : Name → Maybe Name → Name → Bool
buildMatcher n nothing x = n Name.≡ᵇ x
buildMatcher n (just m) x = n Name.≡ᵇ x ∨ m Name.≡ᵇ x
findMonoidNames : Term → TC MonoidNames
findMonoidNames mon = do
∙-altName ← normalise (def (quote Monoid._∙_) (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
ε-altName ← normalise (def (quote Monoid.ε) (2 ⋯⟅∷⟆ mon ⟨∷⟩ []))
pure record
{ is-∙ = buildMatcher (quote Monoid._∙_) (getName ∙-altName)
; is-ε = buildMatcher (quote Monoid.ε) (getName ε-altName)
}
------------------------------------------------------------------------
-- Building Expr
------------------------------------------------------------------------
-- We now define a function that takes an AST representing the LHS
-- or RHS of the equation to solve and converts it into an AST
-- respresenting the corresponding Expr.
″ε″ : Term
″ε″ = quote ε′ ⟨ con ⟩ []
[_↑]′ : Term → Term
[ t ↑]′ = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])
module _ (names : MonoidNames) where
open MonoidNames names
mutual
″∙″ : List (Arg Term) → Term
″∙″ (x ⟨∷⟩ y ⟨∷⟩ []) = quote _∙′_ ⟨ con ⟩ buildExpr x ⟨∷⟩ buildExpr y ⟨∷⟩ []
″∙″ (x ∷ xs) = ″∙″ xs
″∙″ _ = unknown
buildExpr : Term → Term
buildExpr t@(def n xs) =
if is-∙ n
then ″∙″ xs
else if is-ε n
then ″ε″
else
[ t ↑]′
buildExpr t@(con n xs) =
if is-∙ n
then ″∙″ xs
else if is-ε n
then ″ε″
else [ t ↑]′
buildExpr t = quote [_↑] ⟨ con ⟩ (t ⟨∷⟩ [])
------------------------------------------------------------------------
-- Constructing the solution
------------------------------------------------------------------------
-- This function joins up the two homomorphism proofs. It constructs
-- a proof of the following form:
--
-- trans (sym (homo x)) (homo y)
--
-- where x and y are the Expr representations of each side of the
-- goal equation.
constructSoln : Term → MonoidNames → Term → Term → Term
constructSoln mon names lhs rhs =
quote Monoid.trans ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
(quote Monoid.sym ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩
(quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names lhs ⟨∷⟩ []) ⟨∷⟩ [])
⟨∷⟩
(quote homo ⟨ def ⟩ 2 ⋯⟅∷⟆ mon ⟨∷⟩ buildExpr names rhs ⟨∷⟩ []) ⟨∷⟩
[]
------------------------------------------------------------------------
-- Macro
------------------------------------------------------------------------
solve-macro : Term → Term → TC _
solve-macro mon hole = do
hole′ ← inferType hole >>= normalise
names ← findMonoidNames mon
just (lhs , rhs) ← pure (getArgs hole′)
where nothing → typeError (termErr hole′ ∷ [])
let soln = constructSoln mon names lhs rhs
unify hole soln
macro
solve : Term → Term → TC _
solve = solve-macro