Automatic proof for nat-sub

Stream: general

[Damiano Testa]

Dear All,

have you ever been annoyed by nat-subtraction?

This post is in the intersection of Proofs that should be automatic and linarith failure.

I tried writing a simple-minded tactic that would split nat-subtractions in a goal into the two obvious cases and continue until all nat-subtractions have been removed.

Below is the experimental tactic and the example showing that it works in the case that @Michael Stoll mentioned in his post.

Feel free to experiment and give comments! If you like it, I can polish it and make a PR.

import tactic.linarith

lemma nat.le_cases (a b : ℕ) : a - b = 0 ∨ ∃ c, a = b + c :=
begin
  by_cases ab : a ≤ b,
  { exact or.inl (tsub_eq_zero_of_le ab) },
  { refine or.inr _,
    rcases nat.exists_eq_add_of_le ((not_le.mp ab).le) with ⟨c, rfl⟩,
    exact ⟨_, rfl⟩ },
end

namespace tactic

/--  `get_sub e` extracts a list of pairs `(a, b)` from the expression `e`, where `a - b` is a
subexpression of `e`. -/
meta def get_sub : expr → tactic (list (expr × expr))
| `(%%a - %%b) := do [ga, gb] ← [a, b].mmap get_sub,
                      return ((a, b) :: (ga ++ gb))
| (expr.app f a) := do [gf, ga] ← [f, a].mmap get_sub,
                      return (gf ++ ga)
| _ := pure []

/--  `remove_one_sub e` scans the expression `e` and selects the last occurrence of a
subtractiion `a - b`.  It splits two cases:
*  `a ≤ b`, in which case it replaces `a - b` with `0`, introduces the inequality `a ≤ b` into
   the local context and continues from there;
*  writes `a = b + c`, for some `c`, tries to substitute this equality and continues from there.
-/
meta def remove_one_sub (e : expr) : tactic unit :=
do l ← get_sub e,
  match l.last' with
  | none := fail"no subtractions"
  | some (a, b) := do
    -- introduce names with the following meanings:
    -- `eq0 : a - b = 0`, `exis : ∃ c, b + c = a`, `var = c`, `ide : b + c = a`
    [eq0, exis, var, ide] ← ["h", "k", "x", "hx"].mmap (λ y, get_unused_name y),
    -- either `a ≤ b` or `a = b + c`
    cases `(nat.le_cases %%a %%b) [eq0, exis],
    -- on the branch where `a ≤ b`...
      prf ← get_local eq0,
      rewrite_target prf,
      preq ← to_expr ``(nat.sub_eq_zero_iff_le),
      rewrite_hyp preq prf,
      try `[ simp ],
    -- on the branch where `b < a`...
      swap,
      prf ← get_local exis,
      cases prf [var, ide],
      prf ← get_local ide,
      -- either substitute or rewrite
      subst prf <|> rewrite_target prf,
      `[ rw nat.add_sub_cancel_left ] <|> fail"could not rewrite: something went wrong",
      try `[ simp ]
  end

namespace interactive

/--  Iterate replacing a subtraction with two cases.  Once this is done, try `linarith` on
all remaining goals. -/
meta def remove_subs : tactic unit :=
do iterate_at_most' 10 $ target >>= remove_one_sub,
  any_goals' $ try $ `[ linarith ]

end interactive

end tactic

example {i l : ℕ} : 1 ≤ i → i + 1 ≤ l → i - 1 + (l - i - 1 + 1) + 1 = l :=
begin
  intros,
  remove_subs,
end

[Damiano Testa]

Of course, I would be happy to know situations where this tactic works, but it would probably be more useful to have examples where it does not work!

[Michael Stoll]

You could remove the spurious d in the example :smile:

[Damiano Testa]

Done! I edited the code above.

[Andrew Yang]

I think it would be useful to have a version without simps and linariths, so that it could be used mid-proof without introducing non-terminal simps.

[Damiano Testa]

Andrew, good point! If I end up making a PR, I'll definitely make sure not to introduce non-terminal simps!

[Damiano Testa]

Btw, the simp there is mostly a lazy way of dealing with subtractions of the form 0 - x.

[Damiano Testa]

I created #16422.

The tactic no longer uses simp and will only use linarith if it is called via remove_subs!.

[Damiano Testa]

Dear All,

I realize that merging a tactic this close to the transition to Lean4 is not anyone's priority.

Still, if someone could take a look at #16443 and give me some comments, I would be very grateful! My main motivation is that I have been trying to do some Lean4 programming, but I still find it easier to go via Lean3 code.

Thus, even if this tactic does not get merged, I could use a Lean3-mergeable version as a canvas to port it to Lean4.

Thanks!

[Damiano Testa]

Following up on the discussion here, I made the small changes to make remove_subs to work with tsub.

However, while the tactic does work, linarith seems to be much less developed for canonically_ordered... than for nat.

[Damiano Testa]

Here are explicit examples highlighting the difference in behaviour of linarith:

import data.real.nnreal
open_locale nnreal

example {a : ℕ} (h : a = 0) : a = 0 :=
by linarith  -- succeeds

example {R} [canonically_linear_ordered_semifield R] {a : R} (h : a = 0) : a = 0 :=
by linarith  -- fails

example {a : ℝ≥0} (h : a = 0) : a = 0 :=
by linarith  -- fails

Thus, if the truncated subtractions that remove_subs is going to eliminate are not in nat, then calling remove_subs! may be equivalent (but slower) to calling remove_subs.