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
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- An example of how to use `Wrap` to help term inference.
------------------------------------------------------------------------
{-# OPTIONS --cubical-compatible --safe #-}
module README.Data.Wrap where
open import Data.Wrap
open import Algebra
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product.Base using (_,_; ∃; ∃₂; _×_)
open import Level using (Level)
private
variable
c ℓ : Level
A : Set c
m n : ℕ
------------------------------------------------------------------------
-- `Wrap` for remembering instances
------------------------------------------------------------------------
module Instances where
-- `Monoid.Carrier` gets the carrier set from a monoid, and thus has
-- type `Monoid c ℓ → Set c`.
-- Using `Wrap`, we can convert `Monoid.Carrier` into an equivalent
-- “wrapped” version: `MonoidEl`.
MonoidEl : Monoid c ℓ → Set c
MonoidEl = Wrap Monoid.Carrier
-- We can turn any monoid into the equivalent monoid where the elements
-- and equations have been wrapped.
-- The translation mainly consists of wrapping and unwrapping everything
-- via the `Wrap` constructor, `[_]`.
-- Notice that the equality field is wrapping the binary relation
-- `_≈_ : (x y : Carrier) → Set ℓ`, giving an example of how `Wrap` works
-- for arbitrary n-ary relations.
Wrap-monoid : Monoid c ℓ → Monoid c ℓ
Wrap-monoid M = record
{ Carrier = MonoidEl M
; _≈_ = λ ([ x ]) ([ y ]) → Wrap _≈_ x y
; _∙_ = λ ([ x ]) ([ y ]) → [ x ∙ y ]
; ε = [ ε ]
; isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = record
{ refl = [ refl ]
; sym = λ ([ xy ]) → [ sym xy ]
; trans = λ ([ xy ]) ([ yz ]) → [ trans xy yz ]
}
; ∙-cong = λ ([ xx ]) ([ yy ]) → [ ∙-cong xx yy ]
}
; assoc = λ ([ x ]) ([ y ]) ([ z ]) → [ assoc x y z ]
}
; identity = (λ ([ x ]) → [ identityˡ x ])
, (λ ([ x ]) → [ identityʳ x ])
}
}
where open Monoid M
-- Usually, we would only open one monoid at a time.
-- If we were to open two monoids `M` and `N` simultaneously, Agda would
-- get confused whenever it came across, for example, `_∙_`, not knowing
-- whether it came from `M` or `N`.
-- This is true whether or not `M` and `N` can be disambiguated by some
-- other means (such as by their `Carrier`s).
-- However, with wrapped monoids, we are going to remember the monoid
-- while checking any monoid expressions, so we can afford to have just
-- one, polymorphic, version of `_∙_` visible globally.
open module Wrap-monoid {c ℓ} {M : Monoid c ℓ} = Monoid (Wrap-monoid M)
-- Now we can test out this construct on some existing monoids.
open import Data.Nat.Properties
-- Notice that, while the following two definitions appear to be defined
-- by the same expression, their types are genuinely different.
-- Whereas `Carrier +-0-monoid = ℕ = Carrier *-1-monoid`, `MonoidEl M`
-- does not compute, and thus
-- `MonoidEl +-0-monoid ≠ MonoidEl *-1-monoid` definitionally.
-- This lets us use the respective monoids when checking the respective
-- definitions.
test-+ : MonoidEl +-0-monoid
test-+ = ([ 3 ] ∙ ε) ∙ [ 2 ]
test-* : MonoidEl *-1-monoid
test-* = ([ 3 ] ∙ ε) ∙ [ 2 ]
-- The reader is invited to normalise these two definitions
-- (`C-c C-n`, then type in the name).
-- `test-+` is interpreted using (ℕ, +, 0), and thus computes to `[ 5 ]`.
-- Meanwhile, `test-*` is interpreted using (ℕ, *, 1), and thus computes
-- to `[ 6 ]`.
------------------------------------------------------------------------
-- `Wrap` for dealing with functions spoiling unification
------------------------------------------------------------------------
module Unification where
open import Relation.Binary.PropositionalEquality
module Naïve where
-- We want to work with factorisations of natural numbers in a
-- “proof-relevant” style. We could draw out `Factor m n o` as
-- m
-- /*\
-- n o.
Factor : (m n o : ℕ) → Set
Factor m n o = m ≡ n * o
-- We can prove a basic lemma about `Factor`: the following tree rotation
-- can be done, due to associativity of `_*_`.
-- m m
-- /*\ /*\
-- no p ----> n op
-- /*\ /*\
-- n o o p
assoc-→ : ∀ {m n o p} →
(∃ λ no → Factor m no p × Factor no n o) →
(∃ λ op → Factor m n op × Factor op o p)
assoc-→ {m} {n} {o} {p} (._ , refl , refl) = _ , *-assoc n o p , refl
-- We must give at least some arguments to `*-assoc`, as Agda is unable to
-- unify `? * ? * ?` with `n * o * p`, as `_*_` is a function and not
-- necessarily injective (and indeed not injective when one of its
-- arguments is 0).
-- We now want to use this lemma in a more complex proof:
-- m m
-- /*\ /*\
-- nop q n opq
-- /*\ ----> /*\
-- no p o pq
-- /*\ /*\
-- n o p q
test : ∀ {m n o p q} →
(∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) →
(∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q)
test {n = n} (no , nop , fm , fnop , fno) =
let _ , fm , fpq = assoc-→ {n = no} (_ , fm , fnop) in
let _ , fm , fopq = assoc-→ {n = n} (_ , fm , fno) in
_ , _ , fm , fopq , fpq
-- This works okay, but where we have written `{n = no}` and similar, we
-- are being forced to deal with details we don't really care about. Agda
-- should be able to fill in the vertices given part of a tree, but can't
-- due to similar reasons as before: `Factor ? ? ?` doesn't unify against
-- `Factor m no p`, because both instances of `Factor` compute and we're
-- left trying to unify `? * ?` against `no * p`.
module Wrapped where
-- We can use `Wrap` to stop the computation of `Factor`.
Factor : (m n o : ℕ) → Set
Factor = Wrap λ m n o → m ≡ n * o
-- Because `assoc-→` needs access to the implementation of `Factor`, the
-- proof is exactly as before except for using `[_]` to wrap and unwrap.
assoc-→ : ∀ {m n o p} →
(∃ λ no → Factor m no p × Factor no n o) →
(∃ λ op → Factor m n op × Factor op o p)
assoc-→ {m} {n} {o} {p} (._ , [ refl ] , [ refl ]) =
_ , [ *-assoc n o p ] , [ refl ]
-- The difference is that now we have our basic lemma, the complex proof
-- can work purely in terms of `Factor` trees. In particular,
-- `Factor ? ? ?` now does unify with `Factor m no p`, so we don't have to
-- give `no` explicitly again.
test : ∀ {m n o p q} →
(∃₂ λ no nop → Factor m nop q × Factor nop no p × Factor no n o) →
(∃₂ λ pq opq → Factor m n opq × Factor opq o pq × Factor pq p q)
test (_ , _ , fm , fnop , fno) =
let _ , fm , fpq = assoc-→ (_ , fm , fnop) in
let _ , fm , fopq = assoc-→ (_ , fm , fno) in
_ , _ , fm , fopq , fpq
|
