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

[gallais at ensl.org]

My guess is that you must begin by pattern matching on [n] because
if n = 0 then [Fin n] has no inhabitant.

--
gallais



On 11 April 2011 08:58, Jason Dusek <jason.dusek at gmail.com> 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.
>>
>> 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
>