3. Understanding error messages🔗

We now want to understand how to read the error messages of grind. This is the error message from before:

`grind` failed
grind.2α:Type u_1inst:DecidableEq αX Y:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Yleft:¬X ∪ Y ⊆ Xright:¬X ∪ Y ⊆ Yw:αh_3:¬(w ∈ X ∪ Y → w ∈ X)w_1:αh_5:¬(w_1 ∈ X ∪ Y → w_1 ∈ Y)⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] 2 * n + 1 ≤ #(X ∪ Y)
[prop] ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
[prop] #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] (X ∪ Y ⊆ Y) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] (X ∪ Y ⊆ X) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] ¬X ∪ Y ⊆ X
[prop] ¬X ∪ Y ⊆ Y
[prop] ¬(w ∈ X ∪ Y → w ∈ X)
[prop] ¬(w_1 ∈ X ∪ Y → w_1 ∈ Y)
[prop] w_1 ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] w ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] (w_1 ∈ X ∪ Y) = (w_1 ∈ X ∨ w_1 ∈ Y)
[prop] (w ∈ X ∪ Y) = (w ∈ X ∨ w ∈ Y)
[eqc] True propositions
[prop] 2 * n + 1 ≤ #(X ∪ Y)
[prop] ∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Y
[prop] ¬X ∪ Y ⊆ X
[prop] ¬X ∪ Y ⊆ Y
[prop] ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[prop] (X ∪ Y ⊆ X) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] (X ∪ Y ⊆ Y) = ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] w ∈ X ∪ Y
[prop] w_1 ∈ X ∪ Y
[prop] ¬#(X ∪ Y) = 0
[prop] w ∈ X ∨ w ∈ Y
[prop] w_1 ∈ X ∨ w_1 ∈ Y
[prop] (w ∈ X ∪ Y) = (w ∈ X ∨ w ∈ Y)
[prop] (w_1 ∈ X ∪ Y) = (w_1 ∈ X ∨ w_1 ∈ Y)
[prop] w_1 ∈ X
[prop] w ∈ Y
[prop] w ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[prop] w_1 ∈ X ∪ Y → ¬#(X ∪ Y) = 0
[eqc] False propositions
[prop] X ∪ Y ⊆ X
[prop] X ∪ Y ⊆ Y
[prop] w ∈ X
[prop] w_1 ∈ Y
[prop] ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ X
[prop] ∀ ⦃x : α⦄, x ∈ X ∪ Y → x ∈ Y
[prop] w ∈ X ∪ Y → w ∈ X
[prop] w_1 ∈ X ∪ Y → w_1 ∈ Y
[prop] #(X ∪ Y) = 0
[cases] Case analyses
[cases] [2/2]: #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y
[cases] source: E-matching `h`
[ematch] E-matching patterns
[thm] card_union_add_card_inter: [@card #3 (@Union.union (Finset _) _ #1 #0), @card _ #0]
[thm] card_union_add_card_inter: [@card #3 (@Union.union (Finset _) _ #1 #0), @card _ #1]
[thm] h: [@LE.le `[ℕ] `[instLENat] (@card `[α] #0) `[n]]
[thm] h: [@card `[α] #0]
[thm] h: [@Subset `[Finset α] `[instHasSubset] #0 `[X]]
[thm] h: [@Subset `[Finset α] `[instHasSubset] #0 `[Y]]
[thm] subset_iff: [@Subset (Finset #2) _ #1 #0]
[thm] Set.subset_def: [@Subset _ _ #1 #0]
[thm] card_ne_zero_of_mem: [@Membership.mem #3 (Finset _) _ #2 #1, @card _ #2]
[thm] mem_union: [@Membership.mem #4 (Finset _) _ (@Union.union (Finset _) _ #2 #1) #0]
[thm] Multiset.mem_add: [@Membership.mem #3 _ _ (@HAdd.hAdd _ _ _ _ #1 #0) #2]
[thm] Set.mem_union: [@Membership.mem #3 _ _ (@Union.union _ _ #1 #0) #2]
[thm] HtmlFeatures.mem_union: [@Membership.mem `[HtmlFeature] `[HtmlFeatures] `[HtmlFeatures.instMembershipHtmlFeature] (@Union.union `[HtmlFeatures] `[HtmlFeatures.instUnion] #1 #0) #2]
[thm] HtmlFeatures.mem_iff_contains: [@Membership.mem `[HtmlFeature] `[HtmlFeatures] `[HtmlFeatures.instMembershipHtmlFeature] #1 #0]
[cutsat] Assignment satisfying linear constraints
[assign] n := 0
[assign] #(X ∪ Y) := 1

[grind] Diagnostics
[thm] E-Matching instances
[thm] card_ne_zero_of_mem ↦ 2
[thm] mem_union ↦ 2
[thm] subset_iff ↦ 2
[thm] h ↦ 1

At the top you can see the goal state that grind got stuck on. If there are several open goals, it only displays the first one. You can see here that we are in a case generated by a case split somewhere. To see how we got there we can set the option trace.grind.split to true to get

[grind.split] #(X ∪ Y) ≤ n ∨ ¬X ∪ Y ⊆ X ∧ ¬X ∪ Y ⊆ Y, generation: 1

Here we can see the statement grind has split on, which is h applied to X ∪ Y.

Question: What does the asserted facts section actually do?

The next thing to understand is that grind doesn't work by rewriting with terms that it considers to be equal. Instead, it maintains equivalence classes. This is also a way to discover contradictions. If two different constructors of the same type (e.g. True and False or some a and none) are put in the same equivalence class, grind has found a contradiction and finishes the proof.

The two main equivalence classes are those of true and false propositions which you can see as output in the error message. It can also show other equivalence classes. That isn't the case in our example but it is here:

Of course this statement is clearly false but it shows us some different possible parts of the error message:

`grind` failed
grindn k:ℕh1:2 * n = kh:¬k = 5⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] 2 * n = k
[prop] ¬k = 5
[eqc] False propositions
[prop] k = 5
[eqc] Equivalence classes
[eqc] {k, 2 * n}
[cutsat] Assignment satisfying linear constraints
[assign] n := 0
[assign] k := 0
[ring] Ring `Lean.Grind.Ring.OfSemiring.Q ℕ`
[diseqs] Disequalities
[_] ¬2 * ↑n + -5 = 0

You can see that here we have more equivalence classes than just those of true and false propositions.

Next, our error message from the beginning of this section has a section on cases. Here you can see on which terms case splits were performed. We will get into case splits in the next section.

Afterwards there is a section called "ematch". E-matching is how grind uses tagged lemmas. We will discuss this in detail in a later section.

Then both error messages feature sections called cutsat and the later error message in this section has a section about ring. These are two examples of satellite solvers that grind employs to solve problems of specific types. They are different from the Mathlib tactics of the same names because grind is supposed to work Mathlib-free. You can however imagine them to work similarly.