The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Yes, it would be great if Coq reformulated everything in terms of eliminators (which is what you call "primitive recursion" right?). It would remove one of the shaky points in convincing mathematicians that they can trust Coq proofs.

Vladimir.

On Dec 19, 2013, at 6:18 AM, Ali Assaf wrote:

Out of curiosity, is there a specific reason why the Coq kernel does not use primitive recursion internally, as in [1]? That is, allow the user to write pattern matching and fixpoints as usual, but transform everything to only use primitive recursion. That ought to fix the problems of code complexity (simpler rules) and correctness (any error in the transformation is detected by the kernel).

Ali

[1]  Eduardo Giménez: Codifying Guarded Definitions with Recursive Schemes. TYPES 1994: 39-59

---

De: "Vladimir Voevodsky" <vladimir AT ias.edu>
À: "Bruno Barras" <bruno.barras AT inria.fr>, "Daniel R. Grayson" <danielrichardgrayson AT gmail.com>
Cc: "Vladimir Voevodsky" <vladimir AT ias.edu>, coq-club AT inria.fr
Envoyé: Mercredi 18 Décembre 2013 22:52:45
Objet: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq

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.