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

[Jason Dusek]

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.
>
> Let's say that I want to prove that the equality is commutative:
>
> eq-comm : {A : Set} (x y : A) -> x == y -> y == x
> eq-comm x y H = ?
>
> Then I can pattern-match on [H] (I said « destruct » in the previous
> message) and I get the term:
>
> eq-comm x .x refl = ?
>
> The [y] is now a [.x] (the dotted patterns are the one where the value
> is forced by the context)
> and I can prove my goal (which is now [x == x]) using [refl].

  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 already have a proof that [tabulate f ! i ≡ f i]
  so I could use this to show that the heads of the vectors are
  equal, I think; but I'm not sure how to bring it in to scope.
  To bring it in scope with a `with' seems not to work at all:

    lem-tab-! xs with xs | tabulate (_!_ xs) | lem-!-tab (_!_ xs) zero
    ...

  This fails with:

    (suc (_102 xs)) != .n of type ℕ
    when checking that the expression zero has type Fin .n

  I hate to simply reprint the exercize and a solution here; the
  tutorial does not seem to offer much guidance here, though.

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