simple_nat_tactic.lean

namespace nat.tactic

open nat
open tactic

meta def match_le (e : expr) : tactic (expr × expr) :=
match expr.is_le e with
| (some r) := return r
| none     := tactic.fail "expression is not a leq"
end

lemma le_eq_left  {x y z : ℕ} (q : x = y) (p : x ≤ z) : y ≤ z := eq.subst q p
lemma le_eq_right {x y z : ℕ} (q : y = z) (p : x ≤ y) : x ≤ z := eq.subst q p

-- Give a base and a bound, this generates a proof that base <= bound if one exists.
meta def nat_lit_le_core (base bound : ℕ) : tactic unit := do
  base_e ← to_expr base,
  diff_e ← to_expr (bound - base),
  sum_e  ← to_expr `(%%base_e + %%diff_e),
  (diff_norm, diff_pr) ← tactic.norm_num sum_e,
  pr ← tactic.to_expr `(@aim.nat.tactic.le_eq_right _ _ _ %%diff_pr (nat.le_add_right %%base_e %%diff_e)),
  tactic.exact pr

-- This evaluates resolves a goal of the form a <= b where a and b are literals.
meta def nat_lit_le : tactic unit := do
  (base_e, bound_e) ← tactic.target >>= match_le,
  base  ← tactic.eval_expr ℕ base_e,
  bound ← tactic.eval_expr ℕ bound_e,
  nat_lit_le_core base bound

-- loosen_upperbound (x <= l) u discharges a goal of the form (x <= u)
meta def loosen_upperbound (pp : pexpr) (bound : ℕ) : tactic unit := do
  p_expr ← tactic.to_expr pp,
  proof_type_expr ← infer_type p_expr,

  (base_expr, tight_bound_expr) ← match_le proof_type_expr,
  tight_bound ← tactic.eval_expr ℕ tight_bound_expr,

  transitivity,
  exact p_expr,
  nat_lit_le_core tight_bound bound

end nat.tactic