16.1. Error Messages🔗

When grind fails, it prints the subgoal that it could not solve. This is typically not enough information to diagnose why grind failed, however. Enabling the verbose flag causes the error message to additionally include all the information returned by grind's subsystems—the contents of the “shared whiteboard.” In particular, it presents equivalence classes of terms that it has determined to be equal. The two largest classes are shown as True propositions and False propositions, listing every literal currently known to be provable or refutable. Inspect these lists to spot missing facts or contradictory assumptions.

Verbose Failure Messages

This example uses grind in a situation where there is not sufficient information for it to prove the theorem.

example (f : Nat → Nat) (h : f 0 = 1) : f 1 = 1 := byf:Nat → Nath:f 0 = 1⊢ f 1 = 1
  `grind` failed
grindf:Nat → Nath:f 0 = 1h_1:¬f 1 = 1⊢ False
use `+verbose` to obtain diagnostic informationgrindAll goals completed! 🐙

The resulting error message shows only the goal that could not be proved:

`grind` failed
grindf:Nat → Nath:f 0 = 1h_1:¬f 1 = 1⊢ False
use `+verbose` to obtain diagnostic information

Enabling the verbose flag makes the error message much more informative:

example (f : Nat → Nat) (h : f 0 = 1) : f 1 = 1 := byf:Nat → Nath:f 0 = 1⊢ f 1 = 1
  `grind` failed
grindf:Nat → Nath:f 0 = 1h_1:¬f 1 = 1⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] f 0 = 1
[prop] ¬f 1 = 1
[eqc] False propositions
[prop] f 1 = 1
[eqc] Equivalence classes
[eqc] {f 0, 1}
[cutsat] Assignment satisfying linear constraints
[assign] f 0 := 1
[assign] f 1 := 2grind +verboseAll goals completed! 🐙

`grind` failed
grindf:Nat → Nath:f 0 = 1h_1:¬f 1 = 1⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] f 0 = 1
[prop] ¬f 1 = 1
[eqc] False propositions
[prop] f 1 = 1
[eqc] Equivalence classes
[eqc] {f 0, 1}
[cutsat] Assignment satisfying linear constraints
[assign] f 0 := 1
[assign] f 1 := 2