[Agda] Proving _!_ is inverse of tabulate...

[Jason Dusek]

On Mon, Apr 11, 2011 at 09:31, Conor McBride <conor at strictlypositive.org> wrote:
> Guillaume is correct to point out that pattern matching on
> equality proofs identifies both sides. There's a handy
> mechanism which packages this fact neatly for a common
> use-case: rewrite. Here's how you use it
>
> myLemma : ... (xs : Vec X n) -> rhubarb xs == custard xs
> myLemma [] = refl  -- hopefully
> myLemma (x :: xs) rewrite myLemma xs = ?

  Rewrite proved to be handy, indeed: the Agda system prompted
  me to replace the ? with a proof that x ∷ xs ≡ x ∷ xs so I end
  up with refl. This is almost too good to be true.

> ...the rewrite mechanism takes a proof of an equation,
> abstracts all occurrences of the lhs, then matches on the
> proof, causing the lhs to be replaced by the rhs.

  So to do this out "longhand", I could have included something
  in a `where', perhaps? There I would have explicitly matched
  on [myLemma xs] and called the inner worker recursively?

--
Jason Dusek
()  ascii ribbon campaign - against html e-mail
/\  www.asciiribbon.org   - against proprietary attachments