package coq-waterproof
Install
Dune Dependency
Authors
Maintainers
Sources
md5=cd4867e94e20eba727bd6deea06130cd
sha512=1205227101bb30f3e8c4ec05217920dcda1e3631ecd0428f2ac820c9a2811f91526d68623aaf01dd9aa1e81e8adfc083af01152d7f7a6e48894caa829bc3f440
README.md.html
README.md
The Waterproof plugin for the Coq proof assistant
The Waterproof plugin for the Coq proof assistant (coq-waterproof
) 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. Mathematicians unfamiliar with the Coq syntax are able to read the resulting proof scripts. The plugin can be used directly in combination with the Coq proof assistant, but it may be worth checking out the related vscode extension as well.
Installation
Through the vscode extension
The easiest way to start using the coq-waterproof
plugin is to install it through the vscode extension.
Basic installation with opam
If you prefer to use the plugin directly with the Coq theorem prover without the vscode extension for Waterproof, for instance, one can install the coq-waterproof
plugin in the following way.
First one needs a working opam
installation (in Linux, WSL or on MacOS).
Then, one can install the coq-waterproof
plugin by:
$ opam install coq-waterproof
This will install the latest release of coq-waterproof.
Example
The following snippet from gives a taste of a proof written using coq-waterproof.
Goal 2 is the infimum of [2, 5).
Proof.
We need to show that (2 is a _lower bound_ for [2, 5)
∧ (∀ l ∈ ℝ, l is a _lower bound_ for [2, 5) ⇨ l ≤ 2)).
We show both statements.
- We need to show that (2 is a lower bound for [2, 5)).
We need to show that (∀ c ∈ [2, 5), 2 ≤ c).
Take c ∈ [2, 5).
We conclude that (2 ≤ c).
- We need to show that
(∀ l ∈ ℝ, l is a lower bound for [2, 5) ⇒ l ≤ 2).
Take l ∈ ℝ. Assume that (l is a lower bound for [2, 5)).
We conclude that (l ≤ 2).
Qed.
Features
Less cryptic, controlled natural language formulations for built-in Coq tactics.
Commonplace mathematical notation such as
ℝ
orA is closed
.Enforced signposting: after a case distinction, for example, one has to state which case is to be shown.
Allows for reasoning with chains of (in)equalities.
Automation to hide details not used in written proofs.
Help messages and more elaborate error messages.
Runtime-configurable presets of hint databases used by the automation.
Usage
To use the tactics in a .v
file, use the import:
Require Import Waterproof.Waterproof.
To use the automation system, add:
Require Import Waterproof.Automation.
To use the tactics system, add:
Require Import Waterproof.Tactics.
To use the notations defined, add:
Require Import Waterproof.Notations.
Automation
The more advanced tactics rely on automation. The automation function is called waterprove
, which employs wp_auto
and wp_eauto
, together with a customizable set of hint-databases.
wp_auto
and wp_eauto
are rewrite of auto
and eauto
with better backtracking support, which can be use to retrieve the full backtrace during the execution of those functions, which allows to have a better control on the execution flow of the hints. For example, it can be used to reject a complete proof if certain lemmas are not used and continue to search for a new one.
Configuration
The behavior of the automation tactics can be configured by importing specific files.
Adding a Database: Example:
Require Import Waterproof.Automation. Waterproof Enable Automation RealsAndIntegers.
Removing a Database: Example:
Require Import Waterproof.Automation. Waterproof Enable Automation RealsAndIntegers. Waterproof Disable Automation RealsAndIntegers.
Clearing every Databases: Example:
Require Import Waterproof.Automation. Waterproof Enable Automation RealsAndIntegers. Waterproof Enable Automation Intuition. Waterproof Clear Automation.
Declaring a new automation dataset: Example:
Require Import Waterproof.Automation. Waterproof Declare Automation Foo. Waterproof Set Main Databases Foo core, wp_core. Waterproof Set Decidability Databases Foo wp_decidability_classical. Waterproof Set Shorten Databases Foo core.
Turn debugging of automation on: Example:
Waterproof Enable Debug Automation.
Turn debugging of automation off: Example:
Waterproof Disable Debug Automation.
Chains of (in)equalities
In written proofs, one often uses a chain of (in)equalities to explain why more complicated (in)equalities hold. Waterproof allows you to use a similar notation in Coq. For example
We conclude that (& -r < -r/2 = 1 - r/2 - 1 ≤ Rmax(1/2, 1 - r/2) - 1 = x - 1).
The chain of inequalities is used to show that -r < x - 1
.
Library documentation
Autogenerated documentation for the coq-waterproof library can be found here.
Background
The coq-waterproof library is developed as part of the educational Waterproof editor for Coq. The tactics are designed to be used by first-year mathematics students who are unfamiliar with Coq. This is also why the tactics require the user to be explicit: the students have to learn to write readable proofs.
The library was originally written by Jim Portegies in Ltac1. It was extended and ported to Ltac2 by Cosmin Manea, Lulof Pirée, Adrian Vrămuleţ and Tudor Voicu as part of the 'Waterfowl' bachelor Software Engineering Project at the Eindhoven University of Technology (in May-June 2021). Since then it has been under further development by Jelle Wemmenhove and Jim Portegies. In April-June 2023, Balthazar Patiachvili improved the automation, and converted parts of the library to an OCaml plugin.
Please also note that a very nice project with many similarities exists for the Lean theorem prover as well: lean-verbose.
Developer instructions
Developers of the coq-waterproof
library might find useful in formation in the developer instructions