Checking if a goal is *definitely wrong* by testing it against random examples in Coq

Question

I'm currently poking around in a medium-sized Coq codebase that I didn't write and am not very familiar with ... and I'm trying off and on to make progress on some lemmas where the proof attempt was Aborted.

One thing that I'm struggling with is learning the framework for this project and where the currently open proofs got stuck simultaneously.

My usual approach in files I've written from scratch is to write very small named lemmas, usually extracted from a more ambitious theorem that I'm not yet able to prove.

However, I'm a project that I'm not familiar with this is harder because I don't have a strong sense of how to "weaken" a proof that I can't currently solve productively.

I'm wondering if there's a tactic (perhaps called quickcheck or something) that generates and tests a bunch of random examples. The goal in this case would not be to close the proof (unless it's like an existential proof or something, which isn't most proofs in my experience), but rather to see whether the current goal is hopeless and fail informatively with a nice message to the user. The motivating use case for this would be help people explore Coq codebases they aren't familiar with by testing conjectures or subgoals to see if the current line of attack is promising.

I have heard of, but haven't used, the creatively named quickchick library.

It's possible that QuickChick already does what I want, but the Readme only described some new custom Vernacular Toplevel definitions defined by the library, and not any tactics.

Answer 1

QuickChick recently got a tactic that you can call in the middle of a proof.

From QuickChick Require Import QuickChick.
From Coq Require Import Nat Arith.

Lemma test (n : nat) : n + n = n.
Proof.
  revert n.    (* the context must be emptied back into the goal (in the future this could be done for you) *)
               (* goal: forall n, n + n = n *)
  quickchick.  (* Counterexample: 1 *)

The QuickChick documentation is a volume of the Software Foundations series. It doesn't yet mention the tactic, but once you know how the QuickChick command works, the tactic is the same, just in the middle of a proof.

The test suite gives more examples of usage of this tactic.

Good places to ask questions about QuickChick are the Github Issues of the QuickChick repository and the Coq Zulip.