Tactic for adding assumptions about every subtractions in the goal

assume_sub_nneg.lean

import tactic.norm_num

meta def expr.find_all (f : expr → list (expr × expr)) (e : expr) : list (expr × expr) :=
e.fold [] (λ x _ xs, f x ++ xs)

namespace tactic

meta def is_sub : expr → list (expr × expr)
 | `(%%x - %%y) := [(x,y)]
 | _ := []

meta def is_div : expr → list (expr × expr)
 | `(%%x / %%y) := [(x,y)]
 | _ := []

namespace interactive

meta def assume_sub_nneg (discharger : itactic) : tactic unit :=
focus1 $ do
 g ← target,
 hs ← (g.find_all is_sub).mmap (λ ⟨x,y⟩, do
   h ← get_unused_name `h,
   to_expr ``(%%y ≤ %%x) >>= assert h,
   [v₀, v₁] ← get_goals,
   set_goals [v₀],
   discharger,
   vs ← get_goals,
   set_goals [v₁],
   return vs ),
 [g'] ← get_goals,
 set_goals $ g' :: hs.join,
 return ()

end interactive
end tactic

example : 5 - (3 - 1) = (3 : ℕ) :=
begin
  assume_sub_nneg { norm_num },
    -- h : 1 ≤ 3,
    -- h_1 : 3 - 1 ≤ 5
    -- ⊢ 5 - (3 - 1) = 3
  admit,
end

example : 5 - (3 - 1) = (3 : ℕ) :=
begin
  assume_sub_nneg { },
    -- 3 goals
    -- h : 1 ≤ 3,
    -- h_1 : 3 - 1 ≤ 5
    -- ⊢ 5 - (3 - 1) = 3

    -- ⊢ 1 ≤ 3

    -- h : 1 ≤ 3
    -- ⊢ 3 - 1 ≤ 5
  repeat { admit },
end