The Waterproof plugin for the Coq proof assistant allows you to write Coq proofs in a style that resembles handwritten mathematical proofs, designed to help university students with learning how to prove mathematical statements.
Allow for choosing blanks in specialize statements. For example:
Goal (forall a b c : nat, a + b + c = 0) -> False.
Proof.
intro H.
Use a := _, b := _, c := _ in (H).
It holds that (?a + ?b + ?c = 0).
When a user provides a blank for postponing the choice of a variable, the tactic automatically creates a variable (an evar) with a name based on the binder name that was selected.
The PR includes renaming of evars also for the choose tactic.
Allow for choosing blanks in specialize statements. For example:
When a user provides a blank for postponing the choice of a variable, the tactic automatically creates a variable (an evar) with a name based on the binder name that was selected.
The PR includes renaming of evars also for the choose tactic.