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):
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
Youtube vidya: https://www.youtube.com/watch?v=wRLybFnjazk&index=3&list=PLWU5W_m7Gj8-CRDXAzQThCf8MSq7wYdff
