Provably Sorted Lists: Instance Search (1)

   Programming with dependent types allows you to create data structures and functions that are guaranteed to maintain correctness invariants. This helps to prevent you (or users of your library) from logic or run-time errors, such as an out of bounds index on an array, reading from a file before it has been opened, or inserting an element into a sorted list in the wrong place.

   This post is the first of three that give an example of how to use DTP in Agda to enforce correctness using sorted lists. This post will focus on designing a data structure to capture the idea of "sortedness" that is also easy for other programmers to use, i.e. helps them avoid writing out proofs in simple cases. To follow along, you will need a version of Agda >= 2.4.2, as the technique we will use requires recursive instance search (discussed below).

   So enough of the preamble - let's dig in! To keep things simple, let's decide to make our lists contain only numbers. We can always go back and parameterize our list over any element type with an ordering relation, but I think that might be too much overhead to start with for an introductory example.

   With that out of the way, a simple representation of a list of sorted numbers would be a list in which, when you add an element to it, you also provide a proof that the element is "in order" relative to the rest of the list. We keep our list sorted in increasing order, which means that we will have a "snoc" list (cons to the right) whose last element is the upper bound of the list. When we snoc a new element, we also show that this new element is larger or equal to this list's upper bound to produce a new list with a new upper bound. The code for this is shown below.

   We have a list of numbers, indexed by its upper bound. The upper bound of the empty list is 0; given xs a sorted list bounded by m and n a number, we can create a new sorted list bounded by n if m ≤ n.

   So far so good, but we run into a problem fast when we try to create a SortList.

   Ugh! Who wants to write code that looks like that? It's hard to see that this is a simple list of 1 2 3 with all those proof terms lying about. Here I used Agsy (C-c C-a) to fill in the proof terms for me, so it didn't require much writing, but it is still painful to read or use.

   The fact that Agda could easily find these proof terms should lead you to think we can get Agda to do this automatically, invisible to the user. And you're right! Let's have our proof as an instance argument; this will have Agda search for constructors that match our proof obligation, as well as any functions declared in an instance block.

   If we attempt to write out a very simple SortList, one containing only the element 3, we have no problems. That's because the constructor z≤n :  ∀ {n} → 0 ≤ n can be found lying around in scope, and it will match the goal 0 ≤ 3.

   However, we run into a problem when we try to use the same list as before.

   Remember what I said before? Instance search looks for constructors that are lying around and (possibly recursive) functions declared in instance blocks. We know that z≤n doesn't apply here, because 1 != 0. But what about the other constructor, s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc n ? Unfortunately, it is not an instance recursive constructor. What we'd like to see is this:

1. Agda needs to find a term that will match 1 ≤ 2
2. Agda looks at the two constructors for _≤_ and sees that s≤s will apply
3. Agda applies s≤s, and searches for a suitable (m≤n : m ≤ n) (found in the constructor argument) that will satisfy the goal.
4. Agda concludes that m≤n must have type 0 ≤ 1.
5. Agda searches the constructors and sees that z≤n will apply, finishing the proof.

Unfortunately, Agda gets stumped at 3; since m≤n is not declared as an instance argument, Agda will search no further. But take heart - we can remedy this! We need simply to declare a function in an instance block to do the trick for us.

   And because we can, let's finish up by prettying up our constructors, which we can now do because our proof obligation is invisible.

   Doesn't that just give you the warm fuzzies? :)

with: intro(in)spection (Pt. 3)

   This is the third in a series of posts about using "with" in programs / proofs in Agda, and it will focus on the "inspect" idiom. I recommend reading the first and second posts before this one, but they aren't absolutely necessary for understanding the material here.

   In the second post, when we encountered the red text of death, the problem was we had used "with" to rewrite all naked occurrences of an expression, but the function we were trying to prove a property about (i.e., swap is involutive) had a hidden use of the original expression, and it wasn't obvious to Agda after the term had been rewritten that the new term was equal to the original.

   As this situation happens quite a lot, the Agda standard library provides an idiom function called inspect that lives in Relation.Binary.PropositionalEquality. inspect takes a function and an argument and returns a structure that "remembers" that the with-expression was originally the function applied to its argument.

   OK, enough of the vagaries. Let's look at a specific example: we have a filter function, and we wish to prove that all elements in the resulting list satisfy the property they were originally filtered by. Below is the classic example of filter on lists.

   In order to prove that, for any list xs and predicate p, p holds true for all elements of filter xs, we will need to look at two things. First, how do we represent "something holds true for all elements of a list"? In my opinion, the most direct way is to use the Agda standard library's Data.List.All, which defines a data structure representing exactly this. Let's copy the definition down below in our buffer and study it a bit (modulo the universe-level boilerplate).

   (Note that in Agda you can have overloaded constructor names. Therefore, the [] and _∷_ for All are distinct from the ones for List).

   The second thing we will have to do arises immediately from studying the definition of All. Our filter function uses booleans, but traditionally in type theory we use indexed types to represent properties about data. Fortunately, this is easy to address - Data.Bool defines a type family T : Bool → Set that maps true to  ⊤ (the trivially inhabited type, not to be confused with, nor spelled with the same symbol, as the T in question) and false to ⊥ (the uninhabited type). With this, we can bridge the gap between booleans and types and write the type signature of our proof:

   I added function composition to clean up the type signature. We are saying here that the predicate type for All is the boolean predicate p elevated to types. There can be no elements x in filter xs where p x is false, as this would mean we would have to produce an inhabitant of the uninhabited type.

   As before, in order to proceed with our proof we will need to follow the same steps as our original program. We first pattern match on our list xs, and fill in the obvious case where it is [].

   We are now looking at the Goal + Context for our inductive case. We cannot analyze our function further without doing some analysis on p x, as this is what is holding up normalization on the function if_then_else_. Let's do that with "with" (we are now actually getting to the issue this blog addresses!). I will both bring in a with term for p x and do pattern matching on it.

   The case where p x = true is the tricky one, so lets deal with the easier false case first. We merely need to notice that our goal type is exactly the return type of a (structurally smaller) recursive call to our proof.

 

    We now need that p is true for all elements in x ∷ filter p xs. There is only one constructor for All that mentions a List cons, so we can have Agda automatically fill that in for us (C-c C-r).

   And fill in the obvious recursive case for the right argument of cons.

   And so now we're left with an interesting goal of T (p x). Because we did pattern matching, we know that in this branch p x must be equal to true. However, once Agda has finished rewriting the obvious occurrences of the expression you used with on, it forgets about the rewriting process entirely. In order to use this fact again, we are going to need a data structure that "remembers" what the original expression was. Enter inspect:

 

   Note that I did a few things here: I added an import, changed the original line using with to include inspect, and passed down the new term to the lines below (we don't need the inspect term in the false case, so I chose not to name it there).

   Now, the type of insp may be a bit confusing. The important thing to understand is that inspect is using a helper function hide to keep from evaluating p x too soon. If it didn't, the type of insp would be Reveal true is true, which would not be very helpful.

   Let's break open insp and see what's inside!

 

   I've used aggressive normalization to make the type of eq more readable, and commented out the RHS before doing the case analysis. Now, we have one final snag. What we have available to us is eq : p x ≡ true, but what we want is a T (p x). You may be tempted to reach for rewrite here, but it won't work! The reason is, rewrite and with happen before anything you put on the RHS of an equation. rewrite will have absolutely no effect, because the new goal of T (p x) isn't visible to it (that goal was introduced as an argument to the  _∷_ constructor for Any). Fortunately, we can use the next best thing - subst.

   subst works a lot like rewrite, but is a proper function and is used on the RHS of an equation. Its type is (again, minus level boilerplate):

subst : ∀ {A : Set} {x y} (P : A → Set) → x ≡ y → P x → P y

   So, we're just going to substitute in an inhabitant of T true where we need one of T (p x).

   One thing to note about subst is that when you haven't specified the type family P you are substituting under, Agda usually has a hard time figuring out the types for the other goals. We know our family is T, and the equation we want to use is eq (or more specifically, sym eq, since we want the equation to run the other way). So how to we provide an element of T true ?

   Let Agda figure that out :)


Youtube vidya: https://www.youtube.com/watch?v=wRLybFnjazk&index=3&list=PLWU5W_m7Gj8-CRDXAzQThCf8MSq7wYdff

`with': hold computation from those to whom it is due (Pt. 2)

   In the post prior, I showed how to pattern match on a rewritten term by manually de-sugaring to `with'. This post will discuss a "gotcha" when writing a proof about a function that uses `with': holding up the computation. And in this case, it will reveal just why the version of swap I defined earlier is a particularly poorly written function.

   Let's get back to speed with where we were:

   We now want to write a simple proof - that swap is involutive, i.e. that it is its own inverse. Our type signature for swap-involutive:

   As a general rule, in order to prove something about a function, you will frequently have to follow the same decision tree as the function, e.g. if the function you're interested in does case analysis on a term, you probably will too. We started with n before, so

   Hmm, what's this? Why doesn't it normalize to [] ≡ [] in the first case? Even thought that's the only case that can come of this, Agda will not do any normalization unless its arguments exactly match a decision tree - in this case, we need to analyse xs, just like we did in our original function.

   If you type the special Emacs agda-mode command C-u C-, you will see the goal pre-normalization - swap zero (swap zero []) ≡ [] . Anyway, it's easy to see where to go on from here, so now let's fill the first goal, pattern match on our tail in the second case, and see what awaits!

   Woah! What are those bars doing in my goal? You can think of this as Agda's way of explicitly telling you what's holding up the computation. In our case, it's the term we rewrote and the equation we rewrote it by. In these situations I proceed in the following way: bring in each "with-held" term one at a time interactively (but all at once programmatically, e.g. all in the same use of `with'). Like so - first our equation:

Notice how +-suc n n got rewritten to eq after the bar in the goal? And now we'll try n + suc n ...

   Oh no! The red text of death! What did we do wrong? Well, reading this error is a bit of a pain - Agda wasn't able to get through type-checking the file before it reached an error, and as a consequence didn't rebind it's internal w₁ (the second with pattern, n + suc n) to our nicer name, n+sn.

   Well ok. But then it's saying w₁, which is the term we bound to n + suc n, is not n + suc n? W₁TF? Is Agda completely out of its mind? Well... no. It's hard to spot, but look at the given type signature of xs. It's Vec A w₁. We have rewritten all of the naked occurrences of n + suc n, but swap still relies on that expression (via its argument n) for its vector argument and return type. Therefore, when we rewrite xs and try to put it back where we found it, Agda complains because now swap isn't being fed an argument that (syntactically) conforms to its type. We need some way to rewrite the type of swap itself!

   I wish I could show you a solution now, but unfortunately, though I have tried many ways to skin this type, I have not had success. I'm hoping someone on #agda can help me out here when I get around to asking them (basically, when I swallow my pride and give up trying to do it myself).

   Instead, I leave with a closing thought - in my previous blog-post, I mentioned Conor McBride had a bit of difficulty defining this version of swap. I felt pretty smug about myself (althought hopefully it didn't show) that I had managed to succeed here. But after all my efforts in trying to show this swap is involutive, it occurs to me that Conor's wisdom was in avoiding a bad program as early as possible. If I may paraphrase: "Only fools code boldly where Conor McBride fears to tread."

`with': great power, great intractibility (Pt. 1)

   This post is in response to an email chain on the Agda mailing list concerning the behaviour of with. For anyone interested, the issue in question (that eventually became a bugfix in Agda 2.4.2.1) has an entry on the Google code page here: https://code.google.com/p/agda/issues/detail?id=1342. I have noticed that newbies like myself (and experts like Conor McBride, even!) sometimes have difficulty with the behavior of with and its cousin rewrite, and thought it might be a good idea to describe some of the pitfalls I've come across and techniques for addressing them. So without further ado...

rewrite

 rewrite is a spiffy pseudo-tactic in Agda that allows you to leverage dependent pattern matching on equality types to "rewrite" sub-terms in your goal. It can be very useful when a solution to the rewritten goal is obvious, but fails spectacularly if you want to do further analysis on the terms in scope. Let's look at an example - a very dumb "swap" function that takes a Vector with an even length and swaps the position of every two elements. I say "dumb" for two reasons: 1) if you want to swap pairs of adjacent elements, you really should be working on a list of pairs; 2) the way we will be expressing "even length" is by using n + n, which does not match the structure we will be working on (this length would work better if we were splitting the vector up and putting the second half in front of the first, like cutting a deck of cards).

   The first thing we have to deal with isn't related to with or rewrite - Agda won't in general try to deconstruct an arbitrary expression with functions inside of it when it isn't obvious which constructor to apply. In this case it's not a big deal - we just pattern match on n instead.

   Ok, so we've delt with the empty case. We know that our input list has an even number of items in it, so if it's not 0, then it has at least 2 elements in it. That means we should be able to pattern match on xs further to get the next item. Right?

   Now, we know that a vector of length n + suc n is non-empty, and thus we should be able to pattern match on the tail of our original list xs because there's only one constructor that applies, but again this is not obvious to Agda. So now we get to rewrite - we want to use the lemma that says suc distributes left over addition.

Groovy! And now to pattern match on xs to get our second element (after importing Propositional equality, which is what the function +-suc returns.)

   Oh no! What's happened? The answer comes from reading the Agda wiki entry on rewrite and putting 2 and 2 together (or in this case, n and n). Essentially, all rewrite does is provide sugar for saying with a | eq when a b : A and eq : a ≡ b.

   In this situation, when you want to pattern match on a term in scope whose type has been rewritten in this way, the only path forward is to manually de-sugar and use with.

   And pattern match on eq...

   And now finally we can pattern match on xs, since it's now in the right form.

   After getting through all that, I realized that Agda won't in general infer the n of a Vector of length n + n, and thus I should not have made it implicit. Oh well.

   Writing this blog makes me think I should make YouTube videos of me programming in Agda live. Might be a better format for things like this than screenshots of my editor window.

Update: OK, so I do have a YouTube video now. Please forgive the poor quality: https://www.youtube.com/watch?v=g_s5G5vqjQc

Whitespace in Programming Languages

    Disclaimer: This post is just my way of getting back into the habit of writing blog posts. You might find it somewhat interesting but it is off-topic as far as the blog's statement of purpose goes.

    I have had some exposure to different kinds of programming languages, and it occurred to me recently that one (crude) way to see what is part of a language's core design philosophy is to see how it uses white-space. White-space is one of the easiest parts of a language's syntactical terms to both write and read. It's reasonable to assume that whatever idea a language allows you to express with minimal syntactic overhead is close to the heart of the language's philosophy.

    Now, no discussion of white-space in programming languages can fail to mention Python. Python is a modern, multi-paradigm programming (scripting) language that is somewhat controversial for it's insistence on using indentation as its code structure. In most languages, it's considered "good form" to indent wherever you have control structures (functions, conditionals, loops). Python requires it. Let's take a look.

#! python

# break operator
# prime numbers

for n in range(2, 1000):
    for x in range(2, n):
        if n % x == 0:
            print n, 'equals', x, '*', n/x
            break
    else:
        # loop fell through without finding a factor
        print n, 'is a prime number'

    What is the effect? The same as what "good coding style" tries to promote, of course: readability and modularity. If your code has too many levels of nested control structures, you really feel it. Python forces you to maintain the same indentation throughout - if you use 4 spaces once, you use it everywhere or the interpreter complains. There's probably more to say here, but like I said, this is a warm up and I have other languages to cover.

   Another important language to discuss is the pathological case - the language "Whitespace" itself. This is a joke language developed by Edwin Brady (who also wrote Idris, which me may see more of in future blog posts...) in which the language commands are all different types of white-space - space, tab, newline, etc. The reason this is a joke language is very much related to the thesis of this post - white-space should be about removing noise from the program or organizing it to be more readable. But if everything is white-space, it's totally unreadable! You're best bet in programming "Whitespace" is to use a hex-editor.

    Now for an even more obscure programming language - J, a descendent of APL. J uses white-space in the creation of arrays, which makes sense - J is one of the few "array oriented" programming languages. Consider the following declaration of a 2 x 3 matrix:

mat = 2 3 $ 0 1 2 3 4 5

and consider the equivalent C code:

int mat[2][3] = { {0, 1, 2} , {3, 4, 5}};

    J uses spaces to delimit the elements of an array, presumably because arrays are the core data structure in the language and it would be excruciating to type them out in the C style.

    Haskell does something similar, as well. If you noticed, J functions (the dollar sign) also use white-space to receive their arguments. Haskell does this for functions of any arity (J only supports up to 2 arguments - if you want more, you guessed it, use an array). Consider a function that takes 3 integers and tests whether they could be the lengths of a right triangle (assuming the 3rd is the hypotenuse).


is_pythag :: Int -> Int -> Int -> Bool
is_pythag a b c = a*a + b*b == c*c

temp = is_pythag 3 4 5

    Like with J and arrays, in Haskell functions are a core data structure so the syntax for defining and using them is trimmed down (I could have omitted the type signature for the function I defined). Though a pure functional language, Haskell also tries to support the idiomatic line-by-line imperative programming. Programmers of imperative languages take using a line to separate commands for granted (whether its required or merely good style), but in Haskell a special form called "do notation" is used to achieve the same.

nameDo :: IO ()
nameDo = do putStr "What is your first name? "
            first <- getLine
            putStr "And your last name? "
            last <- getLine
            let full = first ++ " " ++ last
            putStrLn ("Pleased to meet you, " ++ full ++ "!")

    I'll wrap this up with a discussion of Scala, another multi-paradigm programming language. Scala runs on the Java Virtual Machine and shares some syntax in common with Java itself. One complaint many have about Java that Scala tries to fix, is Java's excruciating verbosity. Consider adding a number to a "BigInt":

BitInteger myBig = big1.add(big2);

    You can see how this would get out of hand with larger arithmetical expressions, especially ones using operators with different precedents from each other (whereas method invocation always has the same precedence). In Scala, you can write:

val myBig = big1 add big2

or even

val myBig = big1 + big2

    Part of this brevity comes from allowing symbolic method names, but allowing methods to sometimes be used as if they were infix operators really helps. Scala also has good type inference, saving you the need to explicitly declare the types (in exchange for having to type val, var, and def instead). Additionally, Scala has a few "magic methods" which can be omitted, such as "apply". Thus, the following two lines of code are equivalent.

myApplyObj.apply(mySubj)
myApplyObj mySubj

    Hope this wasn't too disappointing - you were warned. My future posts will be more ambitious, as I am currently working on a MIPS simulator in Agda and was able to prove a few neat things about representing numbers in binary!

Propositions as Types, and the Universal and Existential Quantifiers

    I have noticed that individuals new to dependent type theory (myself included) initially have a hard time understanding the new paradigm of types-as-propositions required for understating dependent type theory. Personally, before I had any (informal) learning about type theory I considered types to be analogous to sets, and that the Liskov substitution principle reflected the notion that propositions that held true of any set A should hold true of a set B ⊆ A. This idea of a set as a collection of objects defined (usually) by some propositions held in common describing how the objects behaved seems very intuitive to me, and probably anyone who has ever taken a discrete mathematics course. But it is exactly this intuition that gets in the way of understanding what occurs when we identify types as propositions.

    Here's the problem: to my mind, one of the reasons the distinction between sets of objects and descriptions of the object's properties remain separate is that classical mathematics, especially pure set theory, do not require that these objects have any describable properties at all! The axiom of choice in set theory guarantees that certain sets of objects exist, even when it's provable that descriptions of the objects are impossible. But for most of us, our intuition does not know how to deal with unknowable sets. The Banach-Tarski paradox is a good example - it's not a paradox in the sense that it leads to a contradiction, but that the result goes against our intuition about geometric figures. Most of us prefer to reason about objects with known or knowable properties. Dependent type theory gives us this - in fact, the guarantee is so strong, that the very distinction between objects and their properties is collapsed.

    In order to avoid much confusion, let me give some definitions and terms. I will henceforth talk about objects in type theory as constructions (in homage to constructive mathematics), and refer to sets and propositions as interpretations of these constructions, in order help the reader make the leap between set theory and type theory. When we consider type A as a proposition, we also say that the term a : A is a proof of A. There are additionally two special types. We define top, which is a trivially inhabited type. In contrast, the empty type (sometimes just empty, or absurd, bottom, or false) is the type that has no inhabitant, and proving that a proposition is false is done by showing that if we assume the proposition, we can derive an inhabitant of empty (i.e. a contradiction).

    One of my professors asked me, if types are supposed to represent propositions, what proposition does the type of natural numbers represent? Indeed, nothing much - the natural numbers are trivially inhabited by 0, making them no more informative as propositions as top (i.e. trivial truth) is. The natural numbers are much more naturally understood as constructions belonging to a set, or as the subjects of propositions. In order to fully realize constructions that are propositions, we need to use dependent types.

    Consider the following definition:

data _≤_ : Rel ℕ Level.zero where
  z≤n : ∀ {n}                 → zero  ≤ n
  s≤s : ∀ {m n} (m≤n : m ≤ n) → suc m ≤ suc 

    This says, "Less-or-equal is a relation on natural numbers (a level zero type) that is created one of two ways - for two numbers m and n, we have m ≤ n either we have that m is 0, or m and n are successors to two numbers who are also less than or equal to each other. Given this definition, ≤ isn't merely inhabited or uninhabited - it isn't true or false - until you have two numbers m and n to consider. What makes, for example, the type 3 ≤ 5 a proposition is the restricted nature of how an element of such a type can be constructed.

example : 3 ≤ 5
example = s≤s (s≤s (s≤s (z≤n {2})))

    This example works by taking a base case, a proof that 0 is less than 2, and using it to construct inhabitants of 1 ≤ 3, 2 ≤ 4, and finally  3 ≤ 5. In general, types that are indexed over other types (like inequality of numbers) can serve as propositions when constructing elements of said type imposes some sort of restriction or structure on the indexed type.

    Consider another example, a definition describing "evenness" for natural numbers:

data Even : ℕ → Set where
  even-0 : Even 0
  even-s : ∀ {n} → Even n → Even (2 + n)

    This says, "there are two ways a number can be even - either it is 0 or it is 2 + another even number." If I get a construction of type Even n, I know that n has to have been made this way, and so I know that n is an even number. However, it gets much more interesting - what if I wanted to express the idea that, for every number n, double n is an even number (as I have defined Even above)? It should suffice to produce a rule, transforming any input n into a proof / inhabitant of Even (double n)

double : ℕ → ℕ
double n = n * 2

double-is-even : (n : ℕ) → Even (double n)
double-is-even 0 = even-0
double-is-even (suc n') with double-is-even n'
...                     | evn = even-s evn

 This says, "In the case that n is 0, we know that 0 is even; in the case that n is a successor of another number, say n', use recursion to show that double n' is even, and then adding two to double n' is the same as double (suc n'), so we have Even (double (suc n')). So, to express universal quantification over natural numbers, we need only to write a function that takes a natural number and return a construction of some type family whose index is that number (or an expression in which the number occurs).

    In fact, recognizing the correspondence between universal quantification and dependent function types, Agda has a nifty syntax for just this type of situation. For the type signature of double-is-even, we could have equivalently written:

double-is-even : ∀ n → Even (double n)

    Feel free to read this as "for all n, the double of n is even."

    Universal quantification seems straightforward enough - what about for the existential quantifier? In constructive mathematics, it does not suffice merely to show that a particular x exists, satisfying some proposition - we must produce the x satisfying the proposition itself. How might we do this? A particularly elegant solution is to use the dependent product type - a tuple whose first element is the x satisfying some proposition P, and whose second element is the proof that x satisfies P (with P itself as the type of this second (proof) construction).

    In order to see how this might be done, we should first take a closer look a P itself. Let us say P is a proposition about constructions of type A. Then, in Agda, we would say P : A → Set (confusing our terminology a bit, in Agda Set is the type of types, and in our case the type of propositions). So what we want from our tuple is, a first element x : A, and a second element p : P x (a proof of proposition P concerning x). In the Agda standard library, the sorts of tuples are defined as follows (modulo some book-keeping concerning universe levels, which I'll leave out for clarity):

record Σ (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

     In this definition, proj₁ corresponds to x and proj₂ to our proof of P called p. So how do we use this definition to prove a "there exists" proposition? Let us return to our example of even numbers. We had shown that the double of every n is even, and now we shall show that every even number is the double of some number, i.e. that for every even number n there exists a number m such that n ≡ double m (the symbol ≡ represents equality). The proof is given below (the form Σ[_] is just special syntax for the above definition):

even-is-double : ∀ {n} → Even n → Σ[ m ∈ ℕ ] (n ≡ double m)
even-is-double even-0 = (0 , refl)
even-is-double (even-s evn) with even-is-double evn
...                        | (m' , refl) = (1 + m' , refl)

    The type signature says: "For all n, if n is an even number, then there exists an m such that n is equal to double m". The definitions says, "In the case that our even number is 0, we know that double 0 is 0, so we say the number satisfying the equation is 0, and the proof is reflexivity - 0 ≡ 0. If our even number is 2 + another even number (unnamed above, but we'll call it e'), find the number (m') that, when doubled, is our smaller even number e'. double (1 + m') is then equal to 2 + e', which is therefor equal to the even number given to us."

    A closing remark: some time ago someone on the Idris IRC channel complained that Agda should have had a built-in definition of existential types(1) like Idris does, because existentials are "fundamental." I could not disagree more. To me, one of the most beautiful results of dependent type theory is that the "primitive" (i.e. axiomatic) notions of predicate logic for universal and existential quantification can be reduced to even more general notions of dependent function and product types.


1: Idris can of course implement existentials as dependent products, the language just also provides a built-in version as well.

Equational Reasoning vs rewrite in Agda: Equational reasoning

In my last post we explored how to use rewrite to reason about equations in Agda. We found that while rewrite can do quite a lot of the heavy lifting of manipulating equations, too much leads to unreadable code - the equalities are all tacit, meaning if a reader wants to follow along with the proof they would have to work out the types of the intermediate goals by hand. In this post we shall see that Agda's equational reasoning allows the programmer to write these intermediate goals explicitly and even use them to guide their proof.

The Agda standard library provides very useful functions and syntax for equational reasoning in module Relation.Binary.PropositionalEquality. The following import statements should bring the appropriate definitions into scope:

open import Relation.Binary.PropositionalEquality as PropEq
  using (_≡_; refl) renaming (cong to ≡-cong)
open PropEq.≡-Reasoning

Lets see how its used with the same example, proving the commutativity of addition.

 In our previous example, the second case of +-comm' only required one rewrite before finishing with refl. With equational reasoning, we will see that it is a little more verbose. We begin a block of equational reasoning with begin:

Woah! A little scary! The full goal type is given below. Fortunately, beginners such as myself don't need to worry about most of this - only the last couple
 of lines have the immediately relevant information. These lines tell us that to finish this proof we only need to show that suc (m + 0) ≡ suc m. (IsRelatedTo)

Every "chunk" of a block of equational reasoning consists of three parts: the current left hand side of the equation; a rule to apply, and the rest of the proof. These chunks can be broken up for you (and the first chunk automatically filled for you) by Agda. First type ? ≡⟨ ? ⟩ ? in the goal and use the "refine" command. Then, you can use the automatic search to fill the first goal. The result should be the following (after formatting):

Next, I provide the rule I want to use. In this case, I want to show that
suc (m + 0) ≡ suc m. I know how to show that m + 0 ≡ m, so in a sense I want to rewrite the equation under the application of suc on both sides. rewrite did that for us automatically, but when using equational reasoning we need to use  ≡-cong, specifying the structure we want to undo in a lambda as a first argument and the rule we wish to apply in the second.

And after all that, we have our proof. To finish:

This case of the proof is significantly more verbose that using rewrite and has a much steeper learning curve, and it's arguably less readable as well. However, it has the potential to scale, and additionally working on the right hand side of the equation allows us to use the information from multiple goals to write our proofs.

Lets continue with the next case in our proof.

 I can tell that I will finish the proof if, again, I just manipulate everything under the application of suc, but I am also sure that I won't be able to do it in a single step. Thankfully, there is nothing stopping me from nesting another block of equational reasoning.

So far so good. At this point, I realize that I will need a separate lemma (like last time) to finish, so I sketch out what using the lemma should look like:

And of course this proof follows much like the one from last time

Now finishing the proof using more equational reasoning:

A little verbose but very readable, I'd say, and not nearly as verbose as labeling the transformations on the equations using lemmas.

One weakness I see is that unlike rewrite, equational reasoning does not seem to easily support manipulating both sides of the equation. You need only compare the definitions +-comm'-under-sr in this and the last post - the previous post used two rewrites to deal with an intermediate goal suc m + suc n ≡ suc n + suc m before finishing, whereas in this proof it occurs in the middle. This may seem like a small complaint, but for more complicated equations I can imagine it might be conceptually easier to massage both ends of an equation to a provable goal than forcing the programmer to march left to right.

That said, it is certainly more readable and offers the programmer more guidance along the way than with using rewrites as much of the information outside of the angle brackets can be inferred by Agda. All in all I would say, use rewrite sparingly - it's a neat syntactic sugar useful in very small equational manipulations. Very complicated equational manipulations should use the features of ≡-Reasoning.