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

[Conor McBride]

Hi Jason

On 11 Apr 2011, at 07:58, Jason Dusek wrote:

> On Fri, Apr 8, 2011 at 08:00, gallais @ ensl.org
> <guillaume.allais at ens-lyon.org> wrote:
>> Well, propositional equality is an inductive type with only one
>> constructor [refl]. So you can pattern match on any term that is of
>> the shape [A == B], this will yeld [refl] but also identify the
>> corresponding terms.
>
>  Thank you for your explanation. I now see how to leverage an
>  existing refl -- it allows me to identify terms in pattern
>  matches.
>
>  Unfortunately, showing that [tabulate (_!_ xs) ≡ xs] still
>  eludes me.

I recommend induction on xs, as that will simultaneously deliver
an analysis of the vector and its length. I'd expect that
symbolic evaluation alone is enough to deliver that

   tabulate (_!_ []) = []
   tabulate (_!_ (x :: xs)) = x :: tabulate (_!_ xs)

Then, as you've noted, you need to make use of some equality
proofs. You shouldn't need

> I already have a proof that [tabulate f ! i ≡ f i]

but the inductive hypothesis (the recursive call for xs) will
surely be needed.

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 = ?

If the original step-case goal is rhubarby,

   myLemma (x :: xs) : T[rhubarb xs]

then the rewritten goal is custardy

   ? : T[custard xs]

That's to say, 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. But the hokey cokey
happens behind the scenes.

Hope this helps

Conor