[Agda] Help with proofs

[Tristan Wibberley]

On Sun, 2008-05-04 at 19:02 +0100, Nils Anders Danielsson wrote:
> On Sun, May 4, 2008 at 5:10 PM, Tristan Wibberley <tristan at wibberley.org> wrote:
> >
> >  [...] This is in preference from
> >  allowing the proof objects to be the same sometimes and not others
> >  because the rule for when it is allowed and when it isn't is difficult
> >  to grok.
> 
> If the rule is difficult to grok, then maybe we have not explained it
> properly:
> 
> * A function can only be applied to an argument if the type of the
>   argument is equivalent to that expected by the function.
> * Two types are equivalent iff they have the same normal form.
> 
> To understand when two terms have the same normal form you need to
> know how functions defined using pattern matching are evaluated.


I think what I'm saying is that this is the problem. It seems that the
type of a proof object differs depending on the definitions of the
functions used to define its type rather than the direct written form of
the type (and relationships between proof objects used in that written
form as proved in any lemmas). There should be a much stricter rule for
type equivalence and require proofs of (aka transformations for) more
complex type equivalences.

It would be nice if said equivalence proofs could be declarative and
merely imported or given as lemmas, or somesuch.

-- 
Tristan Wibberley

Any opinion expressed is mine (or else I'm playing devils advocate for
the sake of a good argument). My employer had nothing to do with this
communication.