Bas Spitters (Jun 21 2020 at 19:49): Bas Spitters (Jun 21 2020 at 19:49):@Samuel Gruetter wrote a nice overview about counterexample generators.
https://popl19.sigplan.org/details/CoqPL-2019/7/Counterexamples-for-Coq-Conjectures
It would be nice to keep track of any updates. Although, there may not have been much progress since then.
Samuel Gruetter (Jun 21 2020 at 22:21):The update from my side is that I've learnt, in the meantime, that Coq already provides most of what I need to find counterexamples. In fact, one can split counterexample finding into two steps:
1) Guess a few "interesting" values for which your conjecture might not hold.
2) Evaluate your conjecture on these values, if it's true, go back to 1) else done.
When I was working on the writeup linked above, I was assuming that both 1) and 2) need to be done manually in Coq, and that therefore, a tool is needed. But since then, I learnt that 2) can be done almost automatically in Coq: For instance, if my goal contains two nats aand b, I can achieve 2) by assert (a = 42) by admit; assert (b = 43) by admit; subst a b; simpl, and then my goal is most likely something obviously true or something obviously false. So we only need to do 1) manually, which is not that much of a problem, because since I'm planning to eventually prove the conjecture, I usually already have a good intuition on what "interesting" values to try. And moreover, the choices in 1) can be informed by case splits made during the proof: Once I'm far enough down a tree of case splits and stuck in a particularly hard case, most of the values are already constrained to an interesting subset, and picking a concrete value can quickly reveal a counterexample.
Karl Palmskog (Jun 21 2020 at 22:42):I don't disagree that one can do some counterexample exploration as part of regular Coq proofs, but the kind of uses of Nitpick highlighted by Jasmin here, e.g., finding minimal models for use in in papers, seem very remote from this. If the Nunchaku connection to Coq was finished, it might be possible to get something similar to Nitpick.
Last updated: Sep 23 2023 at 14:01 UTC