The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

On 20 déc. 2013, at 14:00, 
croux AT andrew.cmu.edu
 wrote:

> I don't think there are any counter-examples, for the simple reason that
> you can implement any provably total function using induction over the Acc
> predicate (well_founded in the prelude).
> 
> The issue is not definability, the issue is ease of use. If the user wants
> to prove things about her function defined by pattern-matching, then
> either something really clever happens, or the user has to face a scary
> and hard to use function written with dozens of recursors. Efficiency
> becomes an issue as well at this point.

About ease of use, one can derive the elimination principle associated
to the pattern-matching and recursion (in the original, user written 
form, Equations does that automagically). It’s actually easier to work
with and you get shorter proof terms than redoing the same case analysis 
you did in the function definition.

Best,
— Matthieu

> 
>> The point is precisely to not use primitive recursion for formalization.
>> You keep using pattern matching and recursion to formalize what you want,
>> e.g. integer division. Behind the curtain, there is a complex algorithm
>> that uses intelligent heuristics that tranforms internally the user's
>> functions into equivalent ones using only primitive recursion (a.k.a.
>> eliminators), but that is invisible to the user (unless he activates some
>> low-level feature, like the one for universes, or implicit arguments,
>> etc.).
>> 
>> If that algorithm is not satisfying enough then you keep extending it to
>> accept more and more user functions (just like what is currently done with
>> the kernel code). This time however, the kernel will not be compromised
>> since any mistake in the algorithm will be rejected by the kernel.
>> 
>> On the other hand, if there are functions which simply CANNOT be expressed
>> in terms of (Coq's) primitive recursion, then you have certainly defeated
>> my point. Do you have examples of such functions that occur in practice,
>> e.g. in the standard library? As far as I know, all the usual arithmetic
>> functions (even the Ackermann function) can be transformed into
>> (higher-order) primitive recursive functions.
>> 
>> Ali
>> 
>> ----- Mail original -----
>>> De: 
>>> croux AT andrew.cmu.edu
>>> À: "Vladimir Voevodsky" 
>>> <vladimir AT ias.edu>
>>> Cc: "Ali Assaf" 
>>> <ali.assaf AT inria.fr>,
>>>  "Coq Club" 
>>> <coq-club AT inria.fr>
>>> Envoyé: Jeudi 19 Décembre 2013 18:02:38
>>> Objet: Re: [Coq-Club] Propositional extensionality is inconsistent in
>>> Coq
>>> 
>>> 
>>> 
>>> 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.
>>>>> 
>>>>> 
>>>>> 
>>>>> 
>>>> 
>>>> 
>>> 
>>> 
>>> 
>> 
> 
>