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

[gallais at ensl.org]

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].

--
guillaume



On 8 April 2011 09:46, Jason Dusek <jason.dusek at gmail.com> wrote:
> On Fri, Apr 8, 2011 at 07:09, gallais @ ensl.org
> <guillaume.allais at ens-lyon.org> wrote:
>> Have you tried to destruct the proofs of [x == y] and [xs == ys] ?
>
>  To destruct them?
>
> --
> Jason Dusek
> ()  ascii ribbon campaign - against html e-mail
> /\  www.asciiribbon.org   - against proprietary attachments
>