• API
• FAQ
• Tools
• Archive
SHARE
TWEET

# Untitled

a guest Oct 21st, 2019 74 Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1. How to formalize stuff in Agda
2. ==============================
3.
4. Preliminaries
5. -------------
6.
7. For this presentation, we keep the dependencies to a minimum.
8.
9. ```
10. open import Agda.Primitive
11. open import Agda.Builtin.Nat
12. open import Agda.Builtin.Equality
13. ```
14.
15. A `variable` declaration allows us to use variables without binding
16. them explicitly. This means they are implicitly universally quantified
17. in the types where they occur.
18.
19. ```
20. variable
21.   A B C : Set
22.   x y z : A
23.   k l m n : Nat
24. ```
25.
26. (Unary) natural numbers are defined as the datatype `Nat` with two
27. constructors `zero : Nat` and `suc : Nat → Nat`.
28.
29. ```
30. _ : Nat
31. _ = zero + 7 * (suc 3 - 1)
32. ```
33.
34. We can define polymorphic types and functions by pattern matching on
35. them. For example, here is the equivalent of Haskell's `Maybe` type.
36.
37. ```
38. data Maybe (A : Set) : Set where
39.   just    : A → Maybe A
40.   nothing :     Maybe A
41.
42. mapMaybe : (A → B) → (Maybe A → Maybe B)
43. mapMaybe f x = {!!}
44. ```
45.
46. Note how `A` and `B` are implicitly quantified in the type of
47. `mapMaybe`!
48.
49.
50.
51.
52. The Curry-Howard correspondence
53. -------------------------------
54.
55. Under the Curry-Howard correspondence, we can interpret logical
56. propositions (A ∧ B, ¬A, A ⇒ B, ...) as the types of all their
57. possible proofs.
58.
59. A proof of 'A and B' is a *pair* (x , y) of a proof `x : A` and an
60. proof `y : B`.
61.
62. ```
63. record _×_ (A B : Set) : Set where
64.   constructor _,_
65.   field
66.     fst : A
67.     snd : B
68. open _×_
69. ```
70.
71. A proof of 'A or B' is either `inl x` for a proof `x : A` or `inr y`
72. for a proof `y : B`.
73.
74. ```
75. data _⊎_ (A B : Set) : Set where
76.   inl : A → A ⊎ B
77.   inr : B → A ⊎ B
78. ```
79.
80. A proof of 'A implies B' is a transformation from proofs `x : A` to
81. proofs of `B`, i.e. a function of type `A → B`.
82.
83. 'true' has exactly one proof `tt : ⊤`.
84.
85. ```
86. record ⊤ : Set where
87.   constructor tt     -- no fields
88. ```
89.
90. 'false' has no proofs.
91.
92. ```
93. data ⊥ : Set where   -- no constructor
94. ```
95.
96. 'not A' can be defined as 'A implies false'.
97.
98. ```
99. ¬_ : Set → Set
100. ¬ A = A → ⊥
101. ```
102.
103. ### Exercises
104.
105. ```
106. -- “If A then B implies A”
107. ex₁ : A → (B → A)
108. ex₁ = {!!}
109.
110. -- “If A and true then A or false”
111. ex₂ : (A × ⊤) → (A ⊎ ⊥)
112. ex₂ = {!!}
113.
114. -- “If A implies B and B implies C then A implies C ”
115. ex₃ : (A → B) → (B → C) → (A → B)
116. ex₃ = {!!}
117.
118. -- “Either A or not A”
119. ex₄ : A ⊎ (¬ A)
120. ex₄ = {!!}
121.
122. -- “It is not the case that not (either A or not A)”
123. ex₅ : ¬ (¬ (A ⊎ (¬ A)))
124. ex₅ = {!!}
125.
126. ```
127.
128. Equality
129. --------
130.
131. To state many properties of our programs, we need the notion of
132. equality. In Agda, equality is defined as the datatype `_≡_` with one
133. constructor `refl : x ≡ x`.
134.
135. ```
136.
137. _ : x ≡ x
138. _ = refl
139.
140. sym : x ≡ y → y ≡ x
141. sym x≡y = {!!}
142.
143. trans : x ≡ y → y ≡ z → x ≡ z
144. trans x≡y y≡z = {!!}
145.
146. cong : (f : A → B) → x ≡ y → f x ≡ f y
147. cong f x≡y = {!!}
148. ```
149.
150.
151. Ordering natural numbers
152. ------------------------
153.
154.
155. The standard ordering on natural numbers can be defined as an *indexed
156. datatype* with two indices of type `Nat`:
157.
158. ```
159. module Nat-≤ where
160.   data _≤_ : Nat → Nat → Set where
161.     ≤-zero :         zero  ≤ n
162.     ≤-suc  : m ≤ n → suc m ≤ suc n
163.
164.   ≤-refl : n ≤ n
165.   ≤-refl = {!!}
166.
167.   ≤-trans : k ≤ l → l ≤ m → k ≤ m
168.   ≤-trans = {!!}
169.
170.   ≤-antisym : m ≤ n → n ≤ m → m ≡ n
171.   ≤-antisym = {!!}
172. ```
173.
174. We define separate 'instance' versions of the constructors to help us
175. later on. A definition `inst : A` that is marked as an 'instance' will
176. be used to automatically construct arguments to functions of type
177. `{{x : A}} → B`.
178.
179. ```
180.   instance
181.     ≤-zero-I : zero ≤ n
182.     ≤-zero-I = ≤-zero
183.
184.     ≤-suc-I : {{x ≤ y}} → suc x ≤ suc y
185.     ≤-suc-I {{x≤y}} = ≤-suc x≤y
186. ```
187.
188.
189.
190. Partial orders
191. --------------
192.
193. We'd like to talk not just about orderings on concrete types like
194. `Nat`, but also about the general concept of a 'partial order'.
195.
196. ```
197. record Ord (A : Set) : Set₁ where
198.   field
199.     _≤_       : A → A → Set
200.     ≤-refl    : x ≤ x
201.     ≤-trans   : x ≤ y → y ≤ z → x ≤ z
202.     ≤-antisym : x ≤ y → y ≤ x → x ≡ y
203.
204.   _≥_ : A → A → Set
205.   x ≥ y = y ≤ x
206.
207. open Ord {{...}}
208.
209. instance
210.   Ord-Nat : Ord Nat
211.   _≤_       {{Ord-Nat}} = Nat-≤._≤_
212.   ≤-refl    {{Ord-Nat}} = Nat-≤.≤-refl
213.   ≤-trans   {{Ord-Nat}} = Nat-≤.≤-trans
214.   ≤-antisym {{Ord-Nat}} = Nat-≤.≤-antisym
215.
216. instance
217.   Ord-⊤ : Ord ⊤
218.   _≤_       {{Ord-⊤}} = {!!}
219.   ≤-refl    {{Ord-⊤}} = {!!}
220.   ≤-trans   {{Ord-⊤}} = {!!}
221.   ≤-antisym {{Ord-⊤}} = {!!}
222.
223. module Example (A : Set) {{A-≤ : Ord A}} where
224.
225.   cycle : {x y z : A} → x ≤ y → y ≤ z → z ≤ x → x ≡ y
226.   cycle x≤y y≤z z≤x = {!!}
227. ```
228.
229. For working with binary search trees, we need to be able to decide for
230. any two elements which is the bigger one, i.e. we need a *total*,
231. *decidable* order.
232.
233. ```
234. data Tri {{_ : Ord A}} : A → A → Set where
235.   less    : x ≤ y → Tri x y
236.   equal   : x ≡ y → Tri x y
237.   greater : x ≥ y → Tri x y
238.
239. record TDO (A : Set) : Set₁ where
240.   field
241.     {{Ord-A}} : Ord A
242.     tri       : (x y : A) → Tri x y
243.
244. open TDO {{...}} public
245.
246. triNat : (x y : Nat) → Tri x y
247. triNat x y = {!!}
248.
249. instance
250.   TDO-Nat : TDO Nat
251.   Ord-A {{TDO-Nat}} = Ord-Nat
252.   tri   {{TDO-Nat}} = triNat
253. ```
254.
255.
256.
257. Binary search trees
258. -------------------
259.
260. In a dependently typed language, we can encode invariants of our data
261. structures by using *indexed datatypes*. In this example, we will
262. implement binary search trees by a lower and upper bound to the
263. elements they contain.
264.
265. Since the lower bound may be -∞ and the upper bound may be +∞, we
266. start by providing a generic way to extend a partially ordered set
267. with those two elements.
268.
269. ```
270. data [_]∞ (A : Set) : Set where
271.   -∞  :     [ A ]∞
272.   [_] : A → [ A ]∞
273.   +∞  :     [ A ]∞
274.
275. variable
276.   lower upper : [ A ]∞
277.
278. module Ord-[]∞ {A : Set} {{ A-≤ : Ord A}} where
279.
280.   data _≤∞_ : [ A ]∞ → [ A ]∞ → Set where
281.     -∞-≤ :          -∞   ≤∞   y
282.     []-≤ : x ≤ y → [ x ] ≤∞ [ y ]
283.     +∞-≤ :           x   ≤∞  +∞
284.
285.   instance
286.     Ord-[]∞ : {{_ : Ord A}} → Ord [ A ]∞
287.     _≤_       {{Ord-[]∞}} = _≤∞_
288.     ≤-refl    {{Ord-[]∞}} = {!!}
289.     ≤-trans   {{Ord-[]∞}} = {!!}
290.     ≤-antisym {{Ord-[]∞}} = {!!}
291.
292. open Ord-[]∞ public
293.
294. ```
295.
296. Again we define 'instance' versions of the constructors.
297.
298. ```
299. module _ {{_ : Ord A}} where
300.
301.   instance
302.     -∞-≤-I : {y : [ A ]∞} → -∞ ≤ y
303.     -∞-≤-I = -∞-≤
304.
305.     +∞-≤-I : {x : [ A ]∞} → x ≤ +∞
306.     +∞-≤-I = +∞-≤
307.
308.     []-≤-I : {x y : A} {{x≤y : x ≤ y}} → [ x ] ≤ [ y ]
309.     []-≤-I {{x≤y = x≤y}} = []-≤ x≤y
310. ```
311.
312. Now we are (finally) ready to define binary search trees.
313.
314. ```
315. data BST (A : Set) {{_ : Ord A}} (lower upper : [ A ]∞) : Set where
316.   leaf : {{l≤u : lower ≤ upper}} → BST A lower upper
317.   node : (x : A) → BST A lower [ x ] → BST A [ x ] upper → BST A lower upper
318.
319. _ : BST Nat -∞ +∞
320. _ = node 42
321.       (node 6    leaf leaf)
322.       (node 9000 leaf leaf)
323. ```
324.
325. Note how instances help by automatically filling in the proofs!
326.
327.
328.
329. Next up: defining a lookup function. The result of this function is
330. not just a boolean true/false, but a *proof* that the element is
331. indeed in the tree.
332.
333.
334. ```
335. module Lookup {{_ : TDO A}} where
336.
337.   data _∈_ {lower} {upper} (x : A) : (t : BST A lower upper) → Set where
338.     here  : ∀ {t₁ t₂} → x ≡ y  → x ∈ node y t₁ t₂
339.     left  : ∀ {t₁ t₂} → x ∈ t₁ → x ∈ node y t₁ t₂
340.     right : ∀ {t₁ t₂} → x ∈ t₂ → x ∈ node y t₁ t₂
341.
342.   lookup : ∀ {lower} {upper}
343.          → (x : A) (t : BST A lower upper) → Maybe (x ∈ t)
344.   lookup x t = {!!}
345. ```
346.
347.
348. Similarly, we can define an insertion function. Here, we need to
349. enforce the precondition that the element we want to insert is between
350. the bounds.
351.
352. ```
353. module Insert {{_ : TDO A}} where
354.
355.   insert : (x : A) {{l≤x : lower ≤ [ x ]}} {{x≤u : [ x ] ≤ upper}}
356.          → (t : BST A lower upper) → BST A lower upper
357.   insert x t = {!!}
358. ```
359.
360. To prove correctness of insertion, we have to show that `y ∈ insert x
361. t` is equivalent to `x ≡ y ⊎ y ∈ t`.
362.
363. ```
364.   module Insert-Correct (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}} where
365.
366.     open Lookup
367.
368.     insert-sound : (t : BST A lower upper)
369.                  → (x ≡ y) ⊎ (y ∈ t) → y ∈ insert x t
370.     insert-sound t = {!t!}
371.
372.     insert-complete : (t : BST A lower upper)
373.                     → y ∈ insert x t → (x ≡ y) ⊎ (y ∈ t)
374.     insert-complete t = {!!}
375.
376. ```
RAW Paste Data
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.

Top