Awesome

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) ∧
     (for all 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 (for all c : ℝ, c : [2, 5) ⇒ 2 ≤ c).
  Take c : ℝ. Assume that (c : [2, 5)).
  We conclude that (2 ≤ c).
- We need to show that
    (for all 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 ℝ or A 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