[Coq-Club] [Agda] Re: [HoTT] newbie questions about homotopy theory & advantage of UF/Coq

[Frédéric Blanqui]

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 <mailto: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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140109/745daeac/attachment.html