Can simp find useful equations automatically?

Stream: lean4

[Ching-Tsun Chou]

I encountered the following situation again and again: I have a goal in which a term of the form n - m + m appears, where n and m are terms of type ℕ, (Note that n and m are not always simple variables but may be expressions themselves.). In general, n - m + m cannot be simplified to n. But In the context I have the hypothesis m ≤ n, so indeed n - m + m = n in this context. Right now I have to manually tell Lean this fact by adding show n - m + m = n by omega to the list of equations given to simp. Would it be possible for simp to find such equations by itself?

[Aaron Liu]

If h : m ≤ n then try simp [h]?

[Ching-Tsun Chou]

One more example: I may have m < n among the hypotheses and the goal contains an if-then-else whose condition is m < n + 1. Then "obviously" the condition is false and the ITE should simply to its ELSE clause. But now I have to explicitly supply show ¬ m < n + 1 by omega to simp.

[Kyle Miller]

It's possible to tell simp to use omega as a discharger as well, via simp (disch := omega).

example (m n : Nat) (h : m ≤ n) : n - m + m = 2 := by
  simp (disch := omega)
  -- `n = 2`

Aaron's suggestion of simp [h] (or simp [*]) works here too because this supplies the hypothesis to the simp lemma.

[Kyle Miller]

I'm not sure why if_pos needs to be given explicitly here, but the discharger works for if as well:

example {p q : Prop} (m n : Nat) (h : m < n) : if m < n + 1 then p else q := by
  simp (disch := omega) [if_pos]
  -- ⊢ p

[Ching-Tsun Chou]

How about this?

example (k n : ℕ) (h : k + 1 > n) (f : ℕ → ℕ) : f (k + 1 - n) = f (k - n + 1) := by sorry

Here f represent some complex expression in which the ℕ terms are embedded.

[Ching-Tsun Chou]

Another situation: The goal is:
ss (k + 1 + φ m) ∈ Automaton.next (ss (k + φ m)) (as (k + φ m))
while there is this hypothesis:
ss (k + φ m + 1) ∈ Automaton.next (ss (k + φ m)) (as (k + φ m))
It would be really nice if some like "assumption" would just work.

[Ching-Tsun Chou]

Sorry, I made a typo above, which I just corrected.

[Kyle Miller]

Ching-Tsun Chou said:

How about this?

example (k n : ℕ) (h : k + 1 > n) (f : ℕ → ℕ) : f (k + 1 - n) = f (k - n + 1) := by sorry

Here f represent some complex expression in which the ℕ terms are embedded.

Have you been able to try grind yet? It's good at that sort of goal.

I'm not sure simp will ever have significant symbolic arithmetic normalization integrated into it. Note that users can write simprocs to extend simp's capabilities, and one can write some kind of symbolic normalizer.

I'll mention that there's some limited arithmetic normalization with simp +arith.

[Kyle Miller]

Ching-Tsun Chou said:

It would be really nice if some like "assumption" would just work.

I agree that it would be nice if there were better ways to do "conversion modulo arithmetic".

With our current tactics, all I can really think of for that particular case is doing convert h using n where n is some number to limit congruence, and then omega.

grind probably works here; might be worth testing.

[Ching-Tsun Chou]

Indeed grind works for that example! Thanks for pointing that out.
I don't necessarily have to use simp. It's just the first thing I reach for, so many of my show ... by omega lemmas appear as equations given to simp.