7.2. Interactive mode tactic language
7.2.1. Usual tactic language
A lot of the features of Lean's tactic language also work in the interactive mode.
For example all_goals, <;> and have can be used a expected (where the latter doesn't usually need a proof as we have seen). You can find more examples in the Lean 4.25.0 release notes
7.2.2. grind-specific tactics
There are a few tactics that are specific to the interactive mode or behave differently as in the usual Lean tactic language.
Examples here are the satellite solvers which you can manually instruct grind to use by writing their name, so ring, linarith and so on. Again, in the grind interactive mode these don't refer to the Mathlib tactic under the same name.
Another tactic that behaves slightly differently is cases. In interactive mode, this expects an anchor. You can have the possible anchors displayed with cases?.
Here is an example:
@[simp] lemma forall_mem_not_eq {α : Type*} {s : Finset α}
{a : α} : (∀ b ∈ s, ¬ a = b) ↔ a ∉ s := α:Type u_1s:Finset αa:α⊢ (∀ b ∈ s, ¬a = b) ↔ a ∉ s
grind =>
α:Type u_1s:Finset αa:αh✝:(∀ b ∈ s, ¬a = b) = (a ∈ s)⊢ False
All goals completed! 🐙
which gives the output:
that shows us the only possible case that we could split on here.
Another tactic that we already saw is finish. This basically instructs grind to use all the tools at its disposal (you can imagine grind to do the same thing as grind => finish). In the proof at the beginning of this section we used have to provide a hint and then finish to tell grind to do the rest itself. We also briefly saw finish? at the beginning of this document. This provides you with a more detailed proof. Here is an example:
lemma two_mul_ediv_two_of_even' {n : ℤ} :
Even n → 2 * (n / 2) = n := n:ℤ⊢ Even n → 2 * (n / 2) = n
grind =>
All goals completed! 🐙
which gives the output
Here we can see another command: instantiate tells grind to use e-matching to apply theorems. Additionally one can specify additional theorems to be tried even if they are not tagged with grind or have no matching pattern.
In the following example, Mathlib uses the proof := by grind [SimpleGraph.adjMatrix_apply] as we saw in a previous section. But we could also prove it like this:
theorem isAdjMatrix_adjMatrix''' (α : Type*) {V : Type*}
(G : SimpleGraph V) [DecidableRel G.Adj] [Zero α]
[One α] : (G.adjMatrix α).IsAdjMatrix where
zero_or_one := α:Type u_1V:Type u_2G:SimpleGraph Vinst✝²:DecidableRel G.Adjinst✝¹:Zero αinst✝:One α⊢ ∀ (i j : V), SimpleGraph.adjMatrix α G i j = 0 ∨ SimpleGraph.adjMatrix α G i j = 1
grind =>
α:Type u_1V:Type u_2G:SimpleGraph Vinst✝²:DecidableRel G.Adjinst✝¹:Zero αinst✝:One αi✝:Vj✝:Vleft✝:¬SimpleGraph.adjMatrix α G i✝ j✝ = 0right✝:¬SimpleGraph.adjMatrix α G i✝ j✝ = 1⊢ False
All goals completed! 🐙
7.2.3. Query commands
Interactive mode also provides a few commands that let you query the state of grind.
These will basically output specific parts of the typical error messages.
These commands are: show_splits, show_state, show_true, show_false, show_asserted and show_eqcs.
We could use these in our example from above:
theorem exists_subset_or_subset_of_two_mul_lt_card''''
{α : Type*} [DecidableEq α] {X Y : Finset α} {n : ℕ}
(hXY : 2 * n < #(X ∪ Y)) :
∃ C : Finset α, n < #C ∧ (C ⊆ X ∨ C ⊆ Y) := α:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)⊢ ∃ C, n < #C ∧ (C ⊆ X ∨ C ⊆ Y)
grind =>
α:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h✝:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Ythis:#(X ∪ Y) = #X + #(Y \ X)⊢ False
α:Type u_1inst✝:DecidableEq αX:Finset αY:Finset αn:ℕhXY:2 * n < #(X ∪ Y)h✝:∀ (a : Finset α), #a ≤ n ∨ ¬a ⊆ X ∧ ¬a ⊆ Ythis:#(X ∪ Y) = #X + #(Y \ X)⊢ False
All goals completed! 🐙
which shows us the following: