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

[Bruno Barras]

On 08/01/2014 11:05, Altenkirch Thorsten wrote:
> P.S. An attempt at a summary:
>
> We already knew that pattern matching is incompatible with univalence
> because we can prove K.
>
> Now, due to the example by Maxime (and Conor) there is another
> incompatibilty which arises from pattern matching making things appear
> structurally recursive which shouldn't be.

Credits should go to Daniel Schepler and Thomas Braibant who gave the
first alarming example on Coq-Club. Maxime has ported to Agda an example
given by Cristobal Camarero.

> This one is not covered by K and it is another example where pattern
> matching is non-conservative over the standard eliminators (I guess we
> could invent a version of combinators which allow us to use propositional
> equality of types during recursion).
>
> As a consequence it also affects Coq, which always ruled out K but not
> this one.
>
> This is clearly a bug (has anybody filed a bug report) which should be
> fixed as a matter of urgency. Any proposals?

Yes sir. Maxime has implemented a fix that is almost ready to be pushed
to the dev version of Coq. It is still a bit restrictive and rejects a
couple of examples of the standard library but it is not too complicated
to reformulate those examples to comply with the new rules.

The idea is that subst (or any dependent pattern-matching) preserves the
size, but only according to the form of the "return type". Using
Jesper's notations:

On 08/01/2014 11:35, Jesper Cockx wrote:
>
> <->-elim : (X : Set) (P : (Y : Set) -> X <-> Y -> Set) ->
> (m : P X Refl) ->
> (Y : Set) (E : X <-> Y) -> P Y E
> <->-elim X P m .X Refl = m

The size of m can be preserved only when P is sufficiently specialized.
Let me just give illustrative examples:
- if P is of the form (\ Y e -> list Y) then only the size of the list
is known to be preserved. The size of the elements is unknown.
- If P is of the form (\ Y e -> list tree) then both the size of the
list and its elements are preserved.
- If the body of P does not start with an inductive type, then the size
of m is lost.
I conjecture this is also compatible with HoTT.

I have no idea how easy it is to adapt this to Agda. The main issue is
that it is not at the time you define <->-elim that you know how size is
preserved, but only when you use it.

Regarding evidences for safer pattern-matching, it seems that the only
information you need is the "return type" (argument P of <->-elim).
If you don't have it, then it's hard to avoid K from sneaking in, and
you're lacking information relating what comes in and out of a dependent
eliminator.

So,

On 06/01/2014 14:49, Altenkirch Thorsten wrote:
> Hope I haven't started a flame war.
>
>

On 07/01/2014 10:28, Altenkirch Thorsten wrote:
> Very good. Agda is right and Coq got it wrong.

After all, you might in a better situation using Coq ;)

Bruno.