The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 09/01/2014 01:14, Jesper Cockx a écrit :

On Wed, Jan 8, 2014 at 9:41 PM, Conor McBride <conor AT strictlypositive.org> wrote:

One reason why my brief career as a singer-songwriter was curtailed is that
I could never remember the words, but I think it highly unlikely that the
paper we wrote back then made any kind of assurance about mutual definitions
like moo and noo. If I did, then perhaps I join the good company in error,
for which I apologize.

I'm sorry, I meant the version of noo I gave in my previous mail. I'd better call it something else:

woo : (X : Set) -> (WOne <-> X) -> X -> Zero

woo .WOne Refl (wrap f) = woo (Zero -> WOne) myIso f

bad : Zero

bad = woo WOne Refl (wrap \ ())

The definition of woo falls within the framework of EDPM. Moreover, it is structurally recursive on its third argument. It is still incompatible with univalence (as shown by 'bad'), and it cannot be translated to eliminators.

 

I quite agree that the definition of "structurally smaller" we gave does say
that

  f < wrap f

where f amounts to a collections of (no) things, all of which are smaller
than (wrap f). NOWHERE is it said that transporting f with respect to an
equation on types respects structural ordering relations, and ESPECIALLY
IN THE PRESENCE OF UNIVALENCE that is OBVIOUS NONSENSE.

Of course, transporting a term along an equation should not preserve structural ordering. Yet we should still be able to pattern match on equality proofs (in the --without-K sense), as long as the definition can be translated to eliminators.

 

Eliminators are ok because they fix the "view" of the datatype for the
whole of the recursion. They don't allow you to make up spurious,
allegedly smaller, elements of the type by shipping stuff across
isomorphisms.

I agree, and I think neither should pattern matching let us do this (at least not with --without-K enabled). But wasn't the whole point of EDPM to show that it *is* safe to use pattern matching? What Daniel and Thomas on the Coq list showed, is that we need an additional criterion for pattern matching to be safe. My proposal is to require that the type of the argument on which the function is structurally recursive, should be a data type. A different (and probably much more sophisticated) proposal was given on the Coq list. Do you have another proposal?

Hello.

Note that this condition does not seem to appear in Thierry's original paper on pattern-matching in MLTT (1992). However, and sorry for having to cite myself, but I always required such a condition on my works on the termination of rewriting (which generalizes pattern-matching) in the calculus of constructions (with or without sized types). See for instance Def 24 in "Definitions par rewriting in the calculus of constructions" (Math. Structures in Comp. Science 15(1), 2005).

Best regards,

Frédéric.

On the long term, I think the best way to go would be to actually perform the translation of pattern matching to eliminators in Agda, similar to Matthieu's Equations plugin for Coq. There are just too many subtleties to pattern matching to get everything correct otherwise, especially when univalence and higher inductives are involved.

Jesper