The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hello Vladimir,

Indeed it seems that due to a bug in Coq's termination checker 
(uncovered by Daniel Schepler's example), the negation of (False -> 
False) = True is provable. My original message was simply emphasizing 
that since it is a consequence of the propositional extensionality 
axiom, this axiom was inconsistent with the current implementation of 
Coq. It is probably also the case with univalence (without considering 
other sources of inconsistency with the current Coq implementation).

This can be problematic since some developments rely on this axiom. 
However, it is unlikely that they exploit the bug.

Anyway, some tentative fixes have been described by Christine Paulin and 
Bruno Barras, so the bug is acknowledged and we will provide a patch as 
soon as possible. The technical challenge is to restore the correctness 
of the checker, while not ruling out legitimate and useful examples.

Maxime.

On 12/18/2013 04:52 PM, Vladimir Voevodsky wrote:
> 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.