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

[=?GB2312?B?TWF4aW1lIESopm6oqHM=?=]

I am very sorry, I should have explicitly mentioned that I was porting
Cristobal's example. These things are so interesting that I got
distracted :) Anyway, the original examples are archived on Coq-club.
Thanks Bruno!

Maxime.


On 01/08/2014 09:03 AM, Bruno Barras wrote:
> 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.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda