The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Sorry I came to this discussion a bit late so I might have missed something. The following (adapted from https://sympa.inria.fr/sympa/arc/coq-club/2013-12/msg00119.html ) works:

****

Variable Heq : (False -> False) = True.

Fixpoint contradiction (u : True) : False :=

contradiction (

match Heq in (_ = T) return T with

| eq_refl => fun f:False => match f with end

end

).

 

Definition c : False := contradiction ( I ) . 

****

Is it acknowledged that this is a bug? 

V.

On Dec 18, 2013, at 12:24 PM, Bruno Barras wrote:

Dear Andrej,

On 17/12/2013 23:32, Andrej Bauer wrote:

Several people have commented on the univalence and the present

trouble. I would just like to clarify the situation a bit more.

It is indeed the case that univalence implies that (False -> False) =

True. However:

1) in HoTT we do not use Prop, so that should really be (Empty_set ->

Empty_set) = unit.

Yes, but this is inconsistent as well with the current implementation. Naughty Prop has nothing to do with the current issue.

2) In HoTT we do not use match statements but rather the eliminators.

I do not see how to reproduce the problem using False_rect.

True. As long as you're using the generated recursors, you are safe. None of the nice examples given by Cristobal Camarero do translate to the language of recursors.

3) There are numerous other incompatibilities between Coq and HoTT,

which is why HoTT uses a patched Coq and abstains from using certain

parts of Coq.

We'll have to apply the patch to HoTT-coq when we have it. I think I have a fix that rules out all of the counter-examples given on this list, but we need to be sure it is OK. And I'm not sure it'll be implemented before Christmas.

Anyway, people should not worry too much. The fix will probably change nothing for most people. Maybe Daniel Schepler will have to re-work on the last examples he submitted...

On a more personal note, I think the present situation shows the value

of having some semantics around to curb hasty adoption of rules that

"look OK".

You need *formal* semantics ;-). Informal semantics did not save us here.

Bruno.