search

impermeable / coq-waterproof

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.
https://impermeable.github.io/
GNU Lesser General Public License v3.0
30 stars 9 forks source link

Feat obtain multiple vars + warn on unexpected variable names. #81

Closed jim-portegies closed 3 weeks ago

jim-portegies commented 3 weeks ago

At first I thought this wouldn't be necessary, until I needed to obtain five variables for a lemma...

Allows for:

Goal (exists n m k l : nat, n + k + 1 = l + m)%nat -> True.
Proof.
  intro H.
  Obtain such an n, m, k, l.
Abort.

The tactic now also warns on unexpected variable names.

jim-portegies commented 3 weeks ago

In terms of merging, it is probably better to first merge #80 and then first adapt the tests here.

jim-portegies commented 3 weeks ago

TODO: improve error message when there are too many variables provided, and remove intermediate hypotheses.