grind proofs involving Fin subtraction comm/assoc

Stream: lean4

[Gavin Zhao]

I have several lemmas of the form that I'd like to prove using grind:

x y z : Nat
hx : x ≥ 4

|- (x - 4) + y + z + 4 = x + y + z

|- (x - 4) + y + z + 5 = x + y + z + 1

|- (x - 4) + y + z + 6 = x + y + z + 1

ring can't solve this because I need theorems like Nat.sub_add_comm and Nat.add_sub_assoc in the process. See this playground link for example.

Can I use grind to automate the proofs of these lemmas? Thanks a lot!

[Robin Arnez]

Yes? Except for the one that is impossible of course:

example (x y z : Nat) (hx : x ≥ 4) : (x - 4) + y + z + 4 = x + y + z := by grind
example (x y z : Nat) (hx : x ≥ 4) : (x - 4) + y + z + 5 = x + y + z + 1 := by grind
example (x y z : Nat) (hx : x ≥ 4) : (x - 4) + y + z + 6 = x + y + z + 1 := by grind -- fails

example : ¬ ∀ (x y z : Nat) (_hx : x ≥ 4), (x - 4) + y + z + 6 = x + y + z + 1 := by
  simp only [ge_iff_le, Nat.reduceEqDiff, not_imp, Classical.not_forall, exists_and_left]
  exists 4, by decide, 1, 1

[Gavin Zhao]

Oh my bad, sorry for the typo. I guess this mwe is too simple because in my actual code grind taps into some completely unrelated variable in context and then gets stuck. Is there a way to tell grind to ignore some variable in the context?

[Aaron Liu]

clear?

[Gavin Zhao]

Ok sorry I really should've just gave the full example using Fin instead of simplifying it in Nat:

import Mathlib

abbrev BB : ℕ := 2013265921

variable
  {x y z : Fin BB}
  {hx : x ≥ 4}

include x y z hx

example : (x - 4).val + y.val + z.val + 4 = x.val + y.val + z.val :=
  by
    simp [Fin.sub_val_of_le hx]
    convert_to x.val ≥ 4 at hx
    grind

example : (x - 4).val + y.val + z.val + 5 = x.val + y.val + z.val + 1 := sorry

example : (x - 2 - 2).val + y.val + z.val + 4 = x.val + y.val + z.val := sorry

The normal process is to use Fin.sub_val_of_le. I think the pattern should be simple enough for grind to detect and handle?

[Kim Morrison]

These three all work on the latest nightly release. (Which will arrive in a release candidate approximately next Thursday.)