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. OK, I Understand
 
Top