Created
October 3, 2019 13:46
-
-
Save jespercockx/ddb5b31d4566fe189b455fab755fc0b3 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
How to formalize stuff in Agda | |
============================== | |
Preliminaries | |
------------- | |
For this presentation, we keep the dependencies to a minimum. | |
``` | |
open import Agda.Primitive | |
open import Agda.Builtin.Nat | |
open import Agda.Builtin.Equality | |
``` | |
A `variable` declaration allows us to use variables without binding | |
them explicitly. This means they are implicitly universally quantified | |
in the types where they occur. | |
``` | |
variable | |
A B C : Set | |
x y z : A | |
k l m n : Nat | |
``` | |
(Unary) natural numbers are defined as the datatype `Nat` with two | |
constructors `zero : Nat` and `suc : Nat → Nat`. | |
``` | |
_ : Nat | |
_ = zero + 7 * (suc 3 - 1) | |
``` | |
We can define polymorphic types and functions by pattern matching on | |
them. For example, here is the equivalent of Haskell's `Maybe` type. | |
``` | |
data Maybe (A : Set) : Set where | |
just : A → Maybe A | |
nothing : Maybe A | |
mapMaybe : (A → B) → (Maybe A → Maybe B) | |
mapMaybe f x = {!!} | |
``` | |
Note how `A` and `B` are implicitly quantified in the type of | |
`mapMaybe`! | |
The Curry-Howard correspondence | |
------------------------------- | |
Under the Curry-Howard correspondence, we can interpret logical | |
propositions (A ∧ B, ¬A, A ⇒ B, ...) as the types of all their | |
possible proofs. | |
A proof of 'A and B' is a *pair* (x , y) of a proof `x : A` and an | |
proof `y : B`. | |
``` | |
record _×_ (A B : Set) : Set where | |
constructor _,_ | |
field | |
fst : A | |
snd : B | |
open _×_ | |
``` | |
A proof of 'A or B' is either `inl x` for a proof `x : A` or `inr y` | |
for a proof `y : B`. | |
``` | |
data _⊎_ (A B : Set) : Set where | |
inl : A → A ⊎ B | |
inr : B → A ⊎ B | |
``` | |
A proof of 'A implies B' is a transformation from proofs `x : A` to | |
proofs of `B`, i.e. a function of type `A → B`. | |
'true' has exactly one proof `tt : ⊤`. | |
``` | |
record ⊤ : Set where | |
constructor tt -- no fields | |
``` | |
'false' has no proofs. | |
``` | |
data ⊥ : Set where -- no constructor | |
``` | |
'not A' can be defined as 'A implies false'. | |
``` | |
¬_ : Set → Set | |
¬ A = A → ⊥ | |
``` | |
### Exercises | |
``` | |
-- “If A then B implies A” | |
ex₁ : A → (B → A) | |
ex₁ = {!!} | |
-- “If A and true then A or false” | |
ex₂ : (A × ⊤) → (A ⊎ ⊥) | |
ex₂ = {!!} | |
-- “If A implies B and B implies C then A implies C ” | |
ex₃ : (A → B) → (B → C) → (A → B) | |
ex₃ = {!!} | |
-- “Either A or not A” | |
ex₄ : A ⊎ (¬ A) | |
ex₄ = {!!} | |
-- “It is not the case that not (either A or not A)” | |
ex₅ : ¬ (¬ (A ⊎ (¬ A))) | |
ex₅ = {!!} | |
``` | |
Equality | |
-------- | |
To state many properties of our programs, we need the notion of | |
equality. In Agda, equality is defined as the datatype `_≡_` with one | |
constructor `refl : x ≡ x`. | |
``` | |
_ : x ≡ x | |
_ = refl | |
sym : x ≡ y → y ≡ x | |
sym x≡y = {!!} | |
trans : x ≡ y → y ≡ z → x ≡ z | |
trans x≡y y≡z = {!!} | |
cong : (f : A → B) → x ≡ y → f x ≡ f y | |
cong f x≡y = {!!} | |
``` | |
Ordering natural numbers | |
------------------------ | |
The standard ordering on natural numbers can be defined as an *indexed | |
datatype* with two indices of type `Nat`: | |
``` | |
module Nat-≤ where | |
data _≤_ : Nat → Nat → Set where | |
≤-zero : zero ≤ n | |
≤-suc : m ≤ n → suc m ≤ suc n | |
≤-refl : n ≤ n | |
≤-refl = {!!} | |
≤-trans : k ≤ l → l ≤ m → k ≤ m | |
≤-trans = {!!} | |
≤-antisym : m ≤ n → n ≤ m → m ≡ n | |
≤-antisym = {!!} | |
``` | |
We define separate 'instance' versions of the constructors to help us | |
later on. A definition `inst : A` that is marked as an 'instance' will | |
be used to automatically construct arguments to functions of type | |
`{{x : A}} → B`. | |
``` | |
instance | |
≤-zero-I : zero ≤ n | |
≤-zero-I = ≤-zero | |
≤-suc-I : {{x ≤ y}} → suc x ≤ suc y | |
≤-suc-I {{x≤y}} = ≤-suc x≤y | |
``` | |
Partial orders | |
-------------- | |
We'd like to talk not just about orderings on concrete types like | |
`Nat`, but also about the general concept of a 'partial order'. | |
``` | |
record Ord (A : Set) : Set₁ where | |
field | |
_≤_ : A → A → Set | |
≤-refl : x ≤ x | |
≤-trans : x ≤ y → y ≤ z → x ≤ z | |
≤-antisym : x ≤ y → y ≤ x → x ≡ y | |
_≥_ : A → A → Set | |
x ≥ y = y ≤ x | |
open Ord {{...}} | |
instance | |
Ord-Nat : Ord Nat | |
_≤_ {{Ord-Nat}} = Nat-≤._≤_ | |
≤-refl {{Ord-Nat}} = Nat-≤.≤-refl | |
≤-trans {{Ord-Nat}} = Nat-≤.≤-trans | |
≤-antisym {{Ord-Nat}} = Nat-≤.≤-antisym | |
instance | |
Ord-⊤ : Ord ⊤ | |
_≤_ {{Ord-⊤}} = {!!} | |
≤-refl {{Ord-⊤}} = {!!} | |
≤-trans {{Ord-⊤}} = {!!} | |
≤-antisym {{Ord-⊤}} = {!!} | |
module Example (A : Set) {{A-≤ : Ord A}} where | |
cycle : {x y z : A} → x ≤ y → y ≤ z → z ≤ x → x ≡ y | |
cycle x≤y y≤z z≤x = {!!} | |
``` | |
For working with binary search trees, we need to be able to decide for | |
any two elements which is the bigger one, i.e. we need a *total*, | |
*decidable* order. | |
``` | |
data Tri {{_ : Ord A}} : A → A → Set where | |
less : x ≤ y → Tri x y | |
equal : x ≡ y → Tri x y | |
greater : x ≥ y → Tri x y | |
record TDO (A : Set) : Set₁ where | |
field | |
{{Ord-A}} : Ord A | |
tri : (x y : A) → Tri x y | |
open TDO {{...}} public | |
triNat : (x y : Nat) → Tri x y | |
triNat x y = {!!} | |
instance | |
TDO-Nat : TDO Nat | |
Ord-A {{TDO-Nat}} = Ord-Nat | |
tri {{TDO-Nat}} = triNat | |
``` | |
Binary search trees | |
------------------- | |
In a dependently typed language, we can encode invariants of our data | |
structures by using *indexed datatypes*. In this example, we will | |
implement binary search trees by a lower and upper bound to the | |
elements they contain. | |
Since the lower bound may be -∞ and the upper bound may be +∞, we | |
start by providing a generic way to extend a partially ordered set | |
with those two elements. | |
``` | |
data [_]∞ (A : Set) : Set where | |
-∞ : [ A ]∞ | |
[_] : A → [ A ]∞ | |
+∞ : [ A ]∞ | |
variable | |
lower upper : [ A ]∞ | |
module Ord-[]∞ {A : Set} {{ A-≤ : Ord A}} where | |
data _≤∞_ : [ A ]∞ → [ A ]∞ → Set where | |
-∞-≤ : -∞ ≤∞ y | |
[]-≤ : x ≤ y → [ x ] ≤∞ [ y ] | |
+∞-≤ : x ≤∞ +∞ | |
instance | |
Ord-[]∞ : {{_ : Ord A}} → Ord [ A ]∞ | |
_≤_ {{Ord-[]∞}} = _≤∞_ | |
≤-refl {{Ord-[]∞}} = {!!} | |
≤-trans {{Ord-[]∞}} = {!!} | |
≤-antisym {{Ord-[]∞}} = {!!} | |
open Ord-[]∞ public | |
``` | |
Again we define 'instance' versions of the constructors. | |
``` | |
module _ {{_ : Ord A}} where | |
instance | |
-∞-≤-I : {y : [ A ]∞} → -∞ ≤ y | |
-∞-≤-I = -∞-≤ | |
+∞-≤-I : {x : [ A ]∞} → x ≤ +∞ | |
+∞-≤-I = +∞-≤ | |
[]-≤-I : {x y : A} {{x≤y : x ≤ y}} → [ x ] ≤ [ y ] | |
[]-≤-I {{x≤y = x≤y}} = []-≤ x≤y | |
``` | |
Now we are (finally) ready to define binary search trees. | |
``` | |
data BST (A : Set) {{_ : Ord A}} (lower upper : [ A ]∞) : Set where | |
leaf : {{l≤u : lower ≤ upper}} → BST A lower upper | |
node : (x : A) → BST A lower [ x ] → BST A [ x ] upper → BST A lower upper | |
_ : BST Nat -∞ +∞ | |
_ = node 42 | |
(node 6 leaf leaf) | |
(node 9000 leaf leaf) | |
``` | |
Note how instances help by automatically filling in the proofs! | |
Next up: defining a lookup function. The result of this function is | |
not just a boolean true/false, but a *proof* that the element is | |
indeed in the tree. | |
``` | |
module Lookup {{_ : TDO A}} where | |
data _∈_ {lower} {upper} (x : A) : (t : BST A lower upper) → Set where | |
here : ∀ {t₁ t₂} → x ≡ y → x ∈ node y t₁ t₂ | |
left : ∀ {t₁ t₂} → x ∈ t₁ → x ∈ node y t₁ t₂ | |
right : ∀ {t₁ t₂} → x ∈ t₂ → x ∈ node y t₁ t₂ | |
lookup : ∀ {lower} {upper} | |
→ (x : A) (t : BST A lower upper) → Maybe (x ∈ t) | |
lookup x t = {!!} | |
``` | |
Similarly, we can define an insertion function. Here, we need to | |
enforce the precondition that the element we want to insert is between | |
the bounds. | |
``` | |
module Insert {{_ : TDO A}} where | |
insert : (x : A) {{l≤x : lower ≤ [ x ]}} {{x≤u : [ x ] ≤ upper}} | |
→ (t : BST A lower upper) → BST A lower upper | |
insert x t = {!!} | |
``` | |
To prove correctness of insertion, we have to show that `y ∈ insert x | |
t` is equivalent to `x ≡ y ⊎ y ∈ t`. | |
``` | |
module Insert-Correct (x : A) {{_ : lower ≤ [ x ]}} {{_ : [ x ] ≤ upper}} where | |
open Lookup | |
insert-sound : (t : BST A lower upper) | |
→ (x ≡ y) ⊎ (y ∈ t) → y ∈ insert x t | |
insert-sound t = {!t!} | |
insert-complete : (t : BST A lower upper) | |
→ y ∈ insert x t → (x ≡ y) ⊎ (y ∈ t) | |
insert-complete t = {!!} | |
``` |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment