coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: croux AT andrew.cmu.edu
- To: "Vladimir Voevodsky" <vladimir AT ias.edu>
- Cc: "Ali Assaf" <ali.assaf AT inria.fr>, "Coq Club" <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Propositional extensionality is inconsistent in Coq
- Date: Thu, 19 Dec 2013 12:02:38 -0500
- Importance: Normal
As Bruno pointed out, primitive recursion is not a realistic way to write
functional programs, which happens to be one of Coq's strong points.
In general, it's quite useful to have a powerful specification language
for formalizing, as trying to formalize integer division will quickly tell
you. There was a time when Coq only had the recursors, but they moved on
to pattern matching, proving that the match rule combined with the
fixpoint structural decrease was exactly equivalent in expressiveness.
This again was found lacking, and there have been many incremental
improvements to please the users, all of which seemed reasonable at the
time they were made.
That's the problem with termination: it's undecidable, so it's very common
to come up with a case that's not handled by the current criterion, but
could be with "just a little tweaking". Limiting ourselves to extensions
we have formally proven to be sound would slow development to a crawl, in
fact, both Coq and Agda have features which are widely believed to be
correct, but whose full formal proof of soundness is still unresolved
(singleton elimination and induction recursion spring to mind).
It's unrealistic to ask to return to an older system which can't handle
functions present in the standard library. I think the pragmatic approach
is to find a reasonable fix that avoids the current problem (and obvious
variants), and try to work towards the more principled approach of Typed
Based Termination, as Andreas suggests (I'm not neutral in this affair of
course, as my phd was on a similar subject). The PhD dissertation of Jorge
Sacchini and Benjamin Gregoire have worked out the main theoretical
aspects:
http://hal.inria.fr/hal-00537104
The issue with moving to TBT is first, that it is a difficult and somewhat
thankless implementation task. The second is that there are functions
which pass with the current guard condition, but that would not pass with
the implementation described by Sacchini and Gregoire! A bit more
theoretical and practical work is therefore required.
I wouldn't worry too much about this issue though. As is usual in these
cases, the inconsistency requires a "trick" and it is very likely that
there is a fix which does not break any existing code. I for one, enjoy
these moments where practice meets theory and we have motivation to
address practical problems in a more theoretic way.
In addition, I would humbly contend that the trust in any mathematical
proof formalized in Coq to be several orders of magnitude higher than any
"paper" proof.
Best,
Cody
> 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.
>>
>>
>>
>>
>
>
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, (continued)
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Christine Paulin, 12/16/2013
- RE: [Coq-Club] Propositional extensionality is inconsistent in Coq, Cristóbal Camarero Coterillo, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Christine Paulin, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Andrej Bauer, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Vladimir Voevodsky, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Maxime Dénès, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ali Assaf, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Vladimir Voevodsky, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/19/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ali Assaf, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Ramana Kumar, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Matthieu Sozeau, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Matthieu Sozeau, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, croux, 12/20/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Bruno Barras, 12/18/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Andrej Bauer, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Christine Paulin, 12/17/2013
- RE: [Coq-Club] Propositional extensionality is inconsistent in Coq, Cristóbal Camarero Coterillo, 12/17/2013
- Re: [Coq-Club] Propositional extensionality is inconsistent in Coq, Christine Paulin, 12/16/2013
Archive powered by MHonArc 2.6.18.