The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

I can say that it did affect some of my libraries which have a fair amount of dependent types, but they are relatively easy to fix.

On Wed, Sep 9, 2015 at 6:21 AM, Christian Doczkal <doczkal AT ps.uni-saarland.de> wrote:

Hello,

The CHANGES file for Coq 8.5beta2 states the following:

- The guard condition for fixpoints is now a bit stricter. Propagation
  of subterm value through pattern matching is restricted according to
  the return predicate. Restores compatibility of Coq's logic with the
  propositional extensionality axiom. May create incompatibilities in
  recursive programs heavily using dependent types.

I am wondering how frequent the mentioned "incompatibilities" turned up
in existing developments. That is, how may proofs from projects such as
the Standard Library or Contribs had to be adapted following the change
in the guard condition.

My working hypothesis is that (relative) soundness bugs are rarely
exploited unintentionally and that fixing them should affect very few
proofs. Certainly, the changed guard condition did not cause any
problems in my own developments, but I don't use dependently typed
recursive definitions on a regular basis.

I apologize if this has been asked before, but a quick search did not
turn up anything.


--
Cheers
Christian

--

gregory malecha