The Coq mailing list

[Conor McBride <conor AT strictlypositive.org>]

Hi

Late to the party, I know....

On 4 Aug 2009, at 22:24, Benjamin Pierce wrote:

>  Inductive Dir : Set := R | L.
>  Definition swap (d:Dir) := match d with R => L | L => R end.
>
>  Module Type Iso.
>    Parameter S : Dir -> Set.
>    Parameter f : forall d, S d -> S (swap d).
>    Axiom isoAx : forall d x, f (swap d) (f d x) = x.
>  End Iso.
>
> Unfortunately, this definition doesn't typecheck: the term
>
>   f (swap d) (f d x)
>
> has type S (swap (swap d)), not S d, which is the type of x.  Of  
> course, swap (swap d) is provably equal to d for every d, but not  
> convertible.
>
> What to do?  We've seen the discussion of John Major equality in  
> CoqArt... is this our only hope, or is there a lighter way?

In the light of the fiendish schemes proposed so far, I
invite you to consider what is so heavy about John Major
equality. It was introduced to solve exactly the problem
of comparing values in types which are provably, but not
definitionally equal. This problem is inevitable in
decidable type theories once the /sets/ you reason about
become dependent: it would be astonishingly fortunate if
the only equations one needed on such sets held in the
necessarily illiberal definitional equality. Nothing
less than a heterogeneous propositional equality will
ultimately prove adequate to the task. Individual
examples may have individual workarounds, of course.

Moreover, the JMeq I implemented in LEGO last century
had the property that its homogeneous special cases
behaved just like the usual homogeneous inductive
equality. There were no losers. The JMeq implemented
in Coq does not have this property: it relies on a
K-like axiom "homogeneous JMeq implies equality" rather
than a *definition* with appropriate computational
behaviour. This omission can, I accept, make JMeq
heavy to work with in Coq.

Definitional "proof irrelevance" (DPI) is one way to
tackle this problem: wasn't there a plan to have this
in Coq? How's it going? Of course, DPI is incompatible
with case analysis on proofs, as happens in the
computational behaviour of equality elimination, so it
makes things more complex, requiring computation and
definitional equality to be defined mutually. Just
adding K in some (computational) form is much cheaper!
I know there were some other proposals which would
effectively repair the computational behaviour of JMeq:
it would be good to know the state of play.

All the best

Conor