5.3. Custom Patterns🔗

Sometimes the default algorithms from above do not give you the desired pattern. Then you can use grind_pattern to specify a pattern yourself.

Here is a basic example from Mathlib:

theorem mul_left_iff {M : Type*} [Monoid M] {a b : M}
    (ha : IsUnit a) : IsUnit (a * b) ↔ IsUnit b :=
  show IsUnit (ha.unit * b) ↔ _ byAll goals completed! 🐙 simp [-IsUnit.unit_spec]All goals completed! 🐙

grind_pattern mul_left_iff => IsUnit a, IsUnit (a * b)

You can see that this is specifying a multi-pattern. This theorem is only used by grind if it finds terms of the shape IsUnit a and IsUnit (a * b) on the whiteboard.

If you want to specify multiple patterns you can do that like this:

@[simp]
theorem count_false_add_count_true' (l : List Bool) :
    count false l + count true l = length l :=
  count_not_add_count l true

grind_pattern count_false_add_count_true' => count false l
grind_pattern count_false_add_count_true' => count true l

So this theorem is used by grind if it find either count false l or count true l on the whiteboard.