Using grind for nonlinear arithmetic

Stream: general

[Alexander Bentkamp]

How can I use grind for simple nonlinear arithmetic? In particular, I'd like to solve goals like:

example (x : Nat) : x ≤ 4 → y ≤ 4 → x * y ≤ 2000 := by grind

My best idea so far is to add these grind annotations:

grind_pattern Nat.mul_le_mul_left => n ≤ m, k * n
grind_pattern Nat.mul_le_mul_right => n ≤ m, n * k
grind_pattern Nat.mul_le_mul_left => n ≤ m, k * m
grind_pattern Nat.mul_le_mul_right => n ≤ m, m * k

Is this a good idea?

[Kim Morrison]

No, we need to / plan to add special support for handling nonlinear arithmetic in grind. We're not very far along, however!

[Alexander Bentkamp]

So do you think grind patterns like these will slow down grind?