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: Provide suggestions to users on how to use forall- and exists-statements. #69

Closed jellooo038 closed 1 month ago

jellooo038 commented 1 month ago

Help. tactic

input:

Goal (forall n : nat, n = n) -> (exists m : nat, m = 0) -> (0 = 1).    (* difficult goal *)
  intros.
  Help.
Abort.

results in printed message:

No direct hint available.
Does the goal contain a definition that can be expanded?

To use one of the ‘for all’-statements (∀)
    (forall n : nat, n = n)
use
    Use ... := (...) in (...).

To use one of the ‘there exists’-statements (∃)
    (exists m : nat, m = 0)
use
    Obtain ... according to (...).

Suggestion for new hypothesis

It holds that (forall n : nat, n = n).

results in printed message

To use (forall n : nat, n = n), use
    Use ... := (...) in (...).

Note: these suggestions do result in a lot of printed messages during library compilation.

jellooo038 commented 1 month ago

Looks great, added one small test

jim-portegies commented 1 month ago

Thanks a lot! Maybe we should make some thoughts on whether the messages are visible enough to students.