Skip to content

Commit 0e19b18

Browse files
yurrriqyurrriq
authored
Merge pull request #27 from clayrat/maps
Maps
2 parents 8497604 + 2882c1b commit 0e19b18

File tree

2 files changed

+346
-1
lines changed

2 files changed

+346
-1
lines changed

‎src/Logic.lidr

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -422,7 +422,7 @@ Idris's stdlib has a more general form of this, \idr{Iso}, in
422422
> not_true_iff_false : (Not (b = True)) <-> (b = False)
423423
> not_true_iff_false {b} = (not_true_is_false b, not_true_and_false b)
424424
> where
425-
> not_true_and_false : (b : Bool) -> (b = False) -> (b = True) -> Void
425+
> not_true_and_false : (b : Bool) -> (b = False) -> Not (b = True)
426426
> not_true_and_false False _ Refl impossible
427427
> not_true_and_false True Refl _ impossible
428428

‎src/Maps.lidr

Lines changed: 345 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,345 @@
1+
= Maps: Total and Partial Maps
2+
3+
> module Maps
4+
5+
Maps (or dictionaries) are ubiquitous data structures both generally and in the
6+
theory of programming languages in particular; we're going to need them in many
7+
places in the coming chapters. They also make a nice case study using ideas
8+
we've seen in previous chapters, including building data structures out of
9+
higher-order functions (from `Basics` and `Poly`) and the use of reflection to
10+
streamline proofs (from `IndProp`).
11+
12+
We'll define two flavors of maps: _total_ maps, which include a "default"
13+
element to be returned when a key being looked up doesn't exist, and _partial_
14+
maps, which return a \idr{Maybe} to indicate success or failure. The latter is
15+
defined in terms of the former, using \idr{Nothing} as the default element.
16+
17+
18+
== The Idris Standard Library
19+
20+
\todo[inline]{Edit}
21+
22+
One small digression before we get to maps.
23+
24+
Unlike the chapters we have seen so far, this one does not `Require Import` the
25+
chapter before it (and, transitively, all the earlier chapters). Instead, in
26+
this chapter and from now, on we're going to import the definitions and theorems
27+
we need directly from Idris's standard library stuff. You should not notice much
28+
difference, though, because we've been careful to name our own definitions and
29+
theorems the same as their counterparts in the standard library, wherever they
30+
overlap.
31+
32+
```coq
33+
Require Import Idris.Arith.Arith.
34+
Require Import Idris.Bool.Bool.
35+
Require Import Idris.Strings.String.
36+
Require Import Idris.Logic.FunctionalExtensionality.
37+
```
38+
39+
Documentation for the standard library can be found at
40+
\url{https://www.idris-lang.org/docs/current/}.
41+
42+
The \idr{:search} command is a good way to look for theorems involving objects
43+
of specific types. Take a minute now to experiment with it.
44+
45+
46+
== Identifiers
47+
48+
First, we need a type for the keys that we use to index into our maps. For this
49+
purpose, we again use the type \idr{Id} from the `Lists` chapter. To make this
50+
chapter self contained, we repeat its definition here, together with the
51+
equality comparison function for \idr{Id} and its fundamental property.
52+
53+
> data Id : Type where
54+
> MkId : String -> Id
55+
56+
> beq_id : (x1, x2 : Id) -> Bool
57+
> beq_id (MkId n1) (MkId n2) = decAsBool $ decEq n1 n2
58+
59+
\todo[inline]{Edit}
60+
61+
(The function \idr{decEq} comes from Idris's string library. If you check its
62+
result type, you'll see that it does not actually return a \idr{Bool}, but
63+
rather a type that looks like \idr{Either (x = y) (Not (x = y))}, called a
64+
{Dec}, which can be thought of as an "evidence-carrying boolean." Formally, an
65+
element of \idr{Dec (x=y)} is either a proof that two things are equal or a
66+
proof that they are unequal, together with a tag indicating which. But for
67+
present purposes you can think of it as just a fancy \idr{Bool}.)
68+
69+
> beq_id_refl : (x : Id) -> True = beq_id x x
70+
> beq_id_refl (MkId n) with (decEq n n)
71+
> beq_id_refl _ | Yes _ = Refl
72+
> beq_id_refl _ | No contra = absurd $ contra Refl
73+
74+
The following useful property of \idr{beq_id} follows from an analogous lemma
75+
about strings:
76+
77+
\todo[inline]{Copied \idr{<->} for now}
78+
79+
> iff : {p,q : Type} -> Type
80+
> iff {p} {q} = (p -> q, q -> p)
81+
82+
> syntax [p] "<->" [q] = iff {p} {q}
83+
84+
\todo[inline]{Somehow this doesn't work if put under \idr{where} as usual}
85+
86+
> bto : (beq_id x y = True) -> x = y
87+
> bto {x=MkId n1} {y=MkId n2} prf with (decEq n1 n2)
88+
> bto Refl | (Yes eq) = cong {f=MkId} eq
89+
> bto prf | (No _) = absurd prf
90+
> bfro : (x = y) -> beq_id x y = True
91+
> bfro {x=MkId n1} {y=MkId n2} prf with (decEq n1 n2)
92+
> bfro _ | (Yes _) = Refl
93+
> bfro prf | (No contra) = absurd $ contra $ idInj prf
94+
> where
95+
> idInj : MkId x = MkId y -> x = y
96+
> idInj Refl = Refl
97+
98+
> beq_id_true_iff : (beq_id x y = True) <-> x = y
99+
> beq_id_true_iff = (bto, bfro)
100+
101+
Similarly:
102+
103+
\todo[inline]{Copied and inlined \idr{not_true_iff_false} from \idr{Logic} here
104+
for now}
105+
106+
> not_true_and_false : (b = False) -> Not (b = True)
107+
> not_true_and_false {b=False} _ Refl impossible
108+
> not_true_and_false {b=True} Refl _ impossible
109+
> not_true_is_false : Not (b = True) -> b = False
110+
> not_true_is_false {b=False} h = Refl
111+
> not_true_is_false {b=True} h = absurd $ h Refl
112+
113+
> beq_id_false_iff : (beq_id x y = False) <-> Not (x = y)
114+
> beq_id_false_iff = (to, fro)
115+
> where
116+
> to : (beq_id x y = False) -> Not (x = y)
117+
> to beqf = not_true_and_false beqf . bfro
118+
> fro : (Not (x = y)) -> beq_id x y = False
119+
> fro noteq = not_true_is_false $ noteq . bto
120+
121+
122+
== Total Maps
123+
124+
Our main job in this chapter will be to build a definition of partial maps that
125+
is similar in behavior to the one we saw in the `Lists` chapter, plus
126+
accompanying lemmas about its behavior.
127+
128+
This time around, though, we're going to use _functions_, rather than lists of
129+
key-value pairs, to build maps. The advantage of this representation is that it
130+
offers a more _extensional_ view of maps, where two maps that respond to queries
131+
in the same way will be represented as literally the same thing (the very same
132+
function), rather than just "equivalent" data structures. This, in turn,
133+
simplifies proofs that use maps.
134+
135+
We build partial maps in two steps. First, we define a type of _total maps_ that
136+
return a default value when we look up a key that is not present in the map.
137+
138+
> total_map : Type -> Type
139+
> total_map a = Id -> a
140+
141+
Intuitively, a total map over an element type \idr{a} is just a function that
142+
can be used to look up \idr{Id}s, yielding \idr{a}s.
143+
144+
The function \idr{t_empty} yields an empty total map, given a default element;
145+
this map always returns the default element when applied to any id.
146+
147+
> t_empty : (v : a) -> total_map a
148+
> t_empty v = \_ => v
149+
150+
We can also write this as:
151+
152+
```idris
153+
t_empty = const
154+
```
155+
156+
More interesting is the \idr{update} function, which (as before) takes a map
157+
\idr{m}, a key \idr{x}, and a value \idr{v} and returns a new map that takes
158+
\idr{x} to \idr{v} and takes every other key to whatever \idr{m} does.
159+
160+
> t_update : (x : Id) -> (v : a) -> (m : total_map a) -> total_map a
161+
> t_update x v m = \x' => if beq_id x x' then v else m x'
162+
163+
This definition is a nice example of higher-order programming: \idr{t_update}
164+
takes a _function_ \idr{m} and yields a new function \idr{\x' => ...} that
165+
behaves like the desired map.
166+
167+
For example, we can build a map taking \idr{Id}s to \idr{Bool}s, where \idr{Id
168+
3} is mapped to \idr{True} and every other key is mapped to \idr{False}, like
169+
this:
170+
171+
\todo[inline]{Seems like a wrong description in the book here}
172+
173+
> examplemap : total_map Bool
174+
> examplemap = t_update (MkId "foo") False $
175+
> t_update (MkId "bar") True $
176+
> t_empty False
177+
178+
This completes the definition of total maps. Note that we don't need to define a
179+
\idr{find} operation because it is just function application!
180+
181+
> update_example1 : examplemap (MkId "baz") = False
182+
> update_example1 = Refl
183+
184+
> update_example2 : examplemap (MkId "foo") = False
185+
> update_example2 = Refl
186+
187+
> update_example3 : examplemap (MkId "quux") = False
188+
> update_example3 = Refl
189+
190+
> update_example4 : examplemap (MkId "bar") = True
191+
> update_example4 = Refl
192+
193+
To use maps in later chapters, we'll need several fundamental facts about how
194+
they behave. Even if you don't work the following exercises, make sure you
195+
thoroughly understand the statements of the lemmas! (Some of the proofs require
196+
the functional extensionality axiom, which is discussed in the `Logic` chapter.)
197+
198+
199+
==== Exercise: 1 star, optional (t_apply_empty)
200+
201+
First, the empty map returns its default element for all keys:
202+
203+
> t_apply_empty : t_empty v x = v
204+
> t_apply_empty = ?t_apply_empty_rhs
205+
206+
$\square$
207+
208+
209+
==== Exercise: 2 stars, optional (t_update_eq)
210+
211+
Next, if we update a map \idr{m} at a key \idr{x} with a new value \idr{v} and
212+
then look up \idr{x} in the map resulting from the \idr{update}, we get back
213+
\idr{v}:
214+
215+
> t_update_eq : (t_update x v m) x = v
216+
> t_update_eq = ?t_update_eq_rhs
217+
218+
$\square$
219+
220+
221+
==== Exercise: 2 stars, optional (t_update_neq)
222+
223+
On the other hand, if we update a map \idr{m} at a key \idr{x1} and then look up
224+
a _different_ key \idr{x2} in the resulting map, we get the same result that
225+
\idr{m} would have given:
226+
227+
> t_update_neq : Not (x1 = x2) -> (t_update x1 v m) x2 = m x2
228+
> t_update_neq neq = ?t_update_neq_rhs
229+
230+
$\square$
231+
232+
233+
==== Exercise: 2 stars, optional (t_update_shadow)
234+
235+
If we update a map \idr{m} at a key \idr{x} with a value \idr{v1} and then
236+
update again with the same key \idr{x} and another value \idr{v2}, the resulting
237+
map behaves the same (gives the same result when applied to any key) as the
238+
simpler map obtained by performing just the second \idr{update} on \idr{m}:
239+
240+
> t_update_shadow : t_update x v2 $ t_update x v1 m = t_update x v2 m
241+
> t_update_shadow = ?t_update_shadow_rhs
242+
243+
$\square$
244+
245+
For the final two lemmas about total maps, it's convenient to use the reflection
246+
idioms introduced in chapter `IndProp`. We begin by proving a fundamental
247+
_reflection lemma_ relating the equality proposition on \idr{Id}s with the
248+
boolean function \idr{beq_id}.
249+
250+
251+
==== Exercise: 2 stars, optional (beq_idP)
252+
253+
Use the proof of \idr{beq_natP} in chapter `IndProp` as a template to prove the
254+
following:
255+
256+
\todo[inline]{Copied \idr{Reflect} for now}
257+
258+
> data Reflect : Type -> Bool -> Type where
259+
> ReflectT : (p : Type) -> Reflect p True
260+
> ReflectF : (p : Type) -> (Not p) -> Reflect p False
261+
262+
> beq_idP : Reflect (x = y) (beq_id x y)
263+
> beq_idP = ?beq_idP_rhs
264+
265+
$\square$
266+
267+
Now, given \idr{Id}s \idr{x1} and \idr{x2}, we can use \idr{with (beq_idP x1
268+
x2)} to simultaneously perform case analysis on the result of \idr{beq_id x1 x2}
269+
and generate hypotheses about the equality (in the sense of \idr{=}) of \idr{x1}
270+
and \idr{x2}.
271+
272+
273+
==== Exercise: 2 stars (t_update_same)
274+
275+
With the example in chapter `IndProp` as a template, use \idr{beq_idP} to prove
276+
the following theorem, which states that if we update a map to assign key
277+
\idr{x} the same value as it already has in \idr{m}, then the result is equal to
278+
\idr{m}:
279+
280+
> t_update_same : t_update x (m x) m = m
281+
> t_update_same = ?t_update_same_rhs
282+
283+
$\square$
284+
285+
286+
==== Exercise: 3 stars, recommended (t_update_permute)
287+
288+
Use \idr{beq_idP} to prove one final property of the \idr{update} function: If
289+
we update a map \idr{m} at two distinct keys, it doesn't matter in which order
290+
we do the updates.
291+
292+
> t_update_permute : Not (x2 = x1) -> t_update x1 v1 $ t_update x2 v2 m
293+
> = t_update x2 v2 $ t_update x1 v1 m
294+
> t_update_permute neq = ?t_update_permute_rhs
295+
296+
$\square$
297+
298+
299+
== Partial maps
300+
301+
Finally, we define _partial maps_ on top of total maps. A partial map with
302+
elements of type \idr{a} is simply a total map with elements of type \idr{Maybe
303+
a} and default element \idr{Nothing}.
304+
305+
> partial_map : Type -> Type
306+
> partial_map a = total_map (Maybe a)
307+
308+
> empty : partial_map a
309+
> empty = t_empty Nothing
310+
311+
> update : (x : Id) -> (v : a) -> (m : partial_map a) -> partial_map a
312+
> update x v m = t_update x (Just v) m
313+
314+
We now straightforwardly lift all of the basic lemmas about total maps to
315+
partial maps.
316+
317+
> apply_empty : empty {a} x = Nothing {a}
318+
> apply_empty = Refl
319+
320+
> update_eq : (update x v m) x = Just v
321+
> update_eq {x} {v} {m} =
322+
> rewrite t_update_eq {x} {v=Just v} {m} in
323+
> Refl
324+
325+
> update_neq : Not (x2 = x1) -> (update x2 v m) x1 = m x1
326+
> update_neq {x1} {x2} {v} {m} neq =
327+
> rewrite t_update_neq neq {x1=x2} {x2=x1} {v=Just v} {m} in
328+
> Refl
329+
330+
> update_shadow : update x v2 $ update x v1 m = update x v2 m
331+
> update_shadow {x} {v1} {v2} {m} =
332+
> rewrite t_update_shadow {x} {v1=Just v1} {v2=Just v2} {m} in
333+
> Refl
334+
335+
> update_same : m x = Just v -> update x v m = m
336+
> update_same {x} {m} {v} prf =
337+
> rewrite sym prf in
338+
> rewrite t_update_same {x} {m} in
339+
> Refl
340+
341+
> update_permute : Not (x2 = x1) -> update x1 v1 $ update x2 v2 m
342+
> = update x2 v2 $ update x1 v1 m
343+
> update_permute {x1} {x2} {v1} {v2} {m} neq =
344+
> rewrite t_update_permute neq {x1} {x2} {v1=Just v1} {v2=Just v2} {m} in
345+
> Refl

0 commit comments

Comments
 (0)