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: 'Expand definition' tactic unfolds definition in all statements #66

Closed jellooo038 closed 1 month ago

jellooo038 commented 1 month ago

Example usage:

Definition foo : nat := 0.

Goal (foo = 0) -> (foo = 2) -> (foo = 1).
Proof.
  intros.
  Expand the definition of foo.
Abort.

outputs the message

Expanded definition in statements where applicable.
To include these statements, use (one of):

  We need to show that (0 = 1).

  It holds that (0 = 0).
  It holds that (0 = 2).

and throws an error stating that the Expand definition line needs to be removed in the final proof.

jellooo038 commented 1 month ago

Looks good. Added some tests and removed the period from the output

result:
    (0 = 1).

to make copying easier