# package coq-waterproof

## Install

## Dune Dependency

## Authors

## Maintainers

## Sources

`md5=a7d2922fb4ed7f0b8fe38074319890fe`

`sha512=3c511d066ba324cf19fc5620ae89ad09796f3a04576012739783100487dd8d50214edab9bdfc85d581d6538e601511f4563b90ad1dc3041e60a9702f4875e31d`

## Description

The coq-waterproof library allows you to write Coq proofs in a style that resembles non-mechanized mathematical proofs. Mathematicians unfamiliar with the Coq syntax are able to read the resulting proof scripts.

## Tags

keyword:mathematics education category:Mathematics/Education date:2023-11-04 logpath:Waterproof## Published: 10 Jan 2024

## README

## README.md

## coq-waterproof

The coq-waterproof plugin allows you to write Coq proofs in **a style that resembles non-mechanized mathematical proofs**. Mathematicians unfamiliar with the Coq syntax are able to read the resulting proof scripts.

### Installation

#### Linux

##### With Opam

Firstly you should install `opam`

.

Then, you can create a new switch and install the requirements by running :

```
$ opam switch create waterproof --packages coq.8.17.0
$ eval $(opam env --switch=waterproof)
```

Then, you can clone this repository and install the library by running :

```
$ git clone https://github.com/impermeable/coq-waterproof.git && cd coq-waterproof
$ opam install .
```

Once this is done, you can use coq-waterproof in any file of your system by switching to the `waterproof`

switch on opam.

##### Manually

You can also install coq-waterproof without using opam (though it is greatly recommended for Coq) by compiling it by hand with :

```
$ git clone https://github.com/impermeable/coq-waterproof.git && cd coq-waterproof
$ autoreconf -i -s
$ ./configure
$ dune build
$ make && make install # It is needed to compile and install with both `dune` and `make`
$ dune install
```

### 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.
```

### Example

The following snippet from `sample_proof.v`

gives a taste of a proof written using coq-waterproof.

```
Goal (¬ [0,1) is closed).
Proof.
Expand the definition of closed.
That is, write the goal as (¬ ℝ\[0,1) is open).
Expand the definition of open.
That is, write the goal as
(¬ ∀ a : ℝ, a : ℝ\[0,1) ⇒ a is an interior point of ℝ\[0,1)).
It suffices to show that
(∃ a : ℝ, a : ℝ\[0,1) ∧ ¬ a is an interior point of ℝ\[0,1)).
Choose a := 1.
We show both statements.
- We conclude that (1 : ℝ\[0,1)).
- We need to show that (¬ 1 is an interior point of ℝ\[0,1)).
Expand the definition of interior point.
That is, write the goal as
(¬ ∃ r : ℝ, r > 0 ∧ (∀ x : ℝ, x : B(1,r) ⇒ x : ℝ\[0,1))).
It suffices to show that
(∀ r : ℝ, r > 0 ⇒ (∃ x : ℝ, x : B(1,r) ∧ x : [0,1))).
Take r : ℝ. Assume that (r > 0).
Choose x := (Rmax(1/2, 1 - r/2)).
We show both (x : B(1,r)) and (x : [0,1)).
+ We need to show that (| x - 1 | < r).
It suffices to show that (-r < x - 1 < r).
We show both (-r < x - 1) and (x - 1 < r).
* It holds that (1 - r/2 ≤ Rmax(1/2, 1 - r/2)).
We conclude that (& -r < -r/2 = 1 - r/2 - 1 ≤ Rmax(1/2, 1 - r/2) - 1 = x - 1).
* We conclude that (& x - 1 = Rmax(1/2, 1 - r/2) - 1 < 0 < r).
+ We need to show that (x : [0,1)).
We need to show that (0 ≤ x ∧ x < 1).
We show both (0 ≤ x) and (x < 1).
* We conclude that (& 0 ≤ 1/2 ≤ Rmax(1/2, 1 - r/2) = x).
* We conclude that (& x = Rmax(1/2, 1 - r/2) < 1).
Qed.
```

### Features

Less cryptic,

**controlled natural language formulations for build-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.

### 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, `sample_proof.v`

contains the statement

```
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`

.

### TODO

[ ] Split total statements in Ltac2 before calling

`waterprove`

to have more precise error locations[ ] Add a restricted version of

`wp_autorewrite`

then change the`restricted_automation_routine`

in`src/waterprove.ml`

[ ] Flatten the search tree during

`wp_auto`

and`wp_eauto`

not to make restricted versions skip branches

### 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.