From 9067c7a317a73639964a0272f499c07bc0c77dd4 Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Sun, 1 Oct 2017 21:36:21 +0100 Subject: [PATCH] basics of arithmetic --- src/Basics.lagda | 165 +++++++++++++++-------------------------------- 1 file changed, 53 insertions(+), 112 deletions(-) diff --git a/src/Basics.lagda b/src/Basics.lagda index ccd423d5..c4f1ae94 100644 --- a/src/Basics.lagda +++ b/src/Basics.lagda @@ -1,3 +1,4 @@ + --- title : "Basics: Functional Programming in Agda" layout : page @@ -5,133 +6,73 @@ permalink : /Basics --- \begin{code} -open import Relation.Binary.PropositionalEquality using (_≡_; refl) +open import Data.Nat using (ℕ; zero; suc) +open import Data.Empty using (⊥; ⊥-elim) +open import Relation.Nullary using (¬_; Dec; yes; no) +open import Relation.Binary.PropositionalEquality + using (_≡_; refl; _≢_; trans; sym) \end{code} -The functional programming style brings programming closer to -simple, everyday mathematics: If a procedure or method has no side -effects, then (ignoring efficiency) all we need to understand -about it is how it maps inputs to outputs -- that is, we can think -of it as just a concrete method for computing a mathematical -function. This is one sense of the word "functional" in -"functional programming." The direct connection between programs -and simple mathematical objects supports both formal correctness -proofs and sound informal reasoning about program behavior. - -The other sense in which functional programming is "functional" is -that it emphasizes the use of functions (or methods) as -_first-class_ values -- i.e., values that can be passed as -arguments to other functions, returned as results, included in -data structures, etc. The recognition that functions can be -treated as data in this way enables a host of useful and powerful -idioms. - -Other common features of functional languages include _algebraic -data types_ and _pattern matching_, which make it easy to -construct and manipulate rich data structures, and sophisticated -_polymorphic type systems_ supporting abstraction and code reuse. -Agda shares all of these features. - -This chapter introduces the most essential elements of Agda. - -## Enumerated Types - -One unusual aspect of Agda is that its set of built-in -features is _extremely_ small. For example, instead of providing -the usual palette of atomic data types (booleans, integers, -strings, etc.), Agda offers a powerful mechanism for defining new -data types from scratch, from which all these familiar types arise -as instances. - -Naturally, the Agda distribution comes with an extensive standard -library providing definitions of booleans, numbers, and many -common data structures like lists and hash tables. But there is -nothing magic or primitive about these library definitions. To -illustrate this, we will explicitly recapitulate all the -definitions we need in this course, rather than just getting them -implicitly from the library. - -To see how this definition mechanism works, let's start with a -very simple example. - -### Days of the Week - -The following declaration tells Agda that we are defining -a new set of data values -- a _type_. +# Addition and its properties \begin{code} -data Day : Set where - monday : Day - tuesday : Day - wednesday : Day - thursday : Day - friday : Day - saturday : Day - sunday : Day +congruent : ∀ {m n} → m ≡ n → suc m ≡ suc n +congruent refl = refl + +injective : ∀ {m n} → suc m ≡ suc n → m ≡ n +injective refl = refl \end{code} -The type is called `day`, and its members are `monday`, -`tuesday`, etc. The second and following lines of the definition -can be read "`monday` is a `day`, `tuesday` is a `day`, etc." - -Having defined `day`, we can write functions that operate on -days. - \begin{code} -nextWeekday : Day -> Day -nextWeekday monday = tuesday -nextWeekday tuesday = wednesday -nextWeekday wednesday = thursday -nextWeekday thursday = friday -nextWeekday friday = monday -nextWeekday saturday = monday -nextWeekday sunday = monday +_+_ : ℕ → ℕ → ℕ +zero + n = n +suc m + n = suc (m + n) \end{code} -One thing to note is that the argument and return types of -this function are explicitly declared. Like most functional -programming languages, Agda can often figure out these types for -itself when they are not given explicitly -- i.e., it performs -_type inference_ -- but we'll include them to make reading -easier. - -Having defined a function, we should check that it works on -some examples. There are actually three different ways to do this -in Agda. - -First, we can use the Emacs command `C-c C-n` to evaluate a -compound expression involving `nextWeekday`. For instance, `nextWeekday -friday` should evaluate to `monday`. If you have a computer handy, this -would be an excellent moment to fire up Agda and try this for yourself. -Load this file, `Basics.lagda`, load it using `C-c C-l`, submit the -above example to Agda, and observe the result. - -Second, we can record what we _expect_ the result to be in the -form of an Agda type: - \begin{code} -test-nextWeekday : nextWeekday (nextWeekday saturday) ≡ tuesday ++-assoc : ∀ m n p → (m + n) + p ≡ m + (n + p) ++-assoc zero n p = refl ++-assoc (suc m) n p rewrite +-assoc m n p = refl + ++-zero : ∀ m → m + zero ≡ m ++-zero zero = refl ++-zero (suc m) rewrite +-zero m = refl + ++-suc : ∀ m n → m + (suc n) ≡ suc (m + n) ++-suc zero n = refl ++-suc (suc m) n rewrite +-suc m n = refl + ++-comm : ∀ m n → m + n ≡ n + m ++-comm m zero = +-zero m ++-comm m (suc n) rewrite +-suc m n | +-comm m n = refl \end{code} -This declaration does two things: it makes an assertion (that the second -weekday after `saturday` is `tuesday`), and it gives the assertion a name -that can be used to refer to it later. +# Equality and decidable equality for naturals -Having made the assertion, we must also verify it. We do this by giving -a term of the above type: + + + +# Showing `double` injective \begin{code} -test-nextWeekday = refl +double : ℕ → ℕ +double zero = zero +double (suc n) = suc (suc (double n)) \end{code} -There is no essential difference between the definition for -`test-nextWeekday` here and the definition for `nextWeekday` above, -except for the new symbol for equality `≡` and the constructor `refl`. -The details of these are not important for now (we'll come back to them in -a bit), but essentially `refl` can be read as "The assertion we've made -can be proved by observing that both sides of the equality evaluate to the -same thing, after some simplification." +\begin{code} +double-injective : ∀ m n → double m ≡ double n → m ≡ n +double-injective zero zero refl = refl +double-injective zero (suc n) () +double-injective (suc m) zero () +double-injective (suc m) (suc n) r = + congruent (double-injective m n (injective (injective r))) +\end{code} -Third, we can ask Agda to _compile_ some program involving our definition, -This facility is very interesting, since it gives us a way to construct -_fully certified_ programs. We'll come back to this topic in later chapters. +In Coq, the inductive proof for `double-injective` +is sensitive to how one inducts on `m` and `n`. In Agda, that aspect +is straightforward. However, Agda requires helper functions for +injection and congruence which are not required in Coq. + +I can remove the use of `congruent` by rewriting with its argument. +Is there an easy way to remove the two uses of `injective`?