Code review for small tactic

Stream: metaprogramming / tactics

[Heather Macbeth]

I wrote my first small tactic, basically a wrapper for fin_cases, which case splits according to the remainder of a variable n modulo a variable p. I'd be really glad to get feedback on doing things more efficiently, or more according to convention.

import tactic.interactive
import tactic.fin_cases
import tactic.norm_cast
import data.int.modeq

lemma int.exists_unique_modeq_mem_range (a : ℤ) (b : ℕ) (hb : 0 < b) :
  ∃ z ∈ finset.range b, a ≡ z [ZMOD b] :=
begin
  obtain ⟨a₀, ha₀, ha₀n⟩ := int.exists_unique_equiv_nat a (by exact_mod_cast hb : (0:ℤ) < b),
  norm_cast at ha₀,
  refine ⟨a₀, finset.mem_range.mpr ha₀, _⟩,
  apply int.modeq.symm,
  exact ha₀n
end

namespace tactic

meta def mod_cases (n p : expr) : tactic unit :=
do z ← mk_app `nat.zero [],
   pos ← mk_app `has_lt.lt [z, p],
   assert `h_pos pos, tactic.exact_dec_trivial, -- make a proof that `p` is positive
   hh ← get_local `h_pos,
   w ← mk_app `int.exists_unique_modeq_mem_range [n, p, hh],
   [(p, [w_name, hw_aux₂])] ← tactic.cases w [`k, `hk_aux],
   [(p', [hk_name, H_name])] ← tactic.cases hw_aux₂ [`hk, `H],
   tactic.fin_cases_at none none hk_name,
   all_goals (do H' ← get_local `H,
                  junk ← replace_at norm_cast.derive [H'] ff,
                  pure ()),
   pure ()


namespace interactive
setup_tactic_parser

meta def mod_cases (n p : parse parser.pexpr) : tactic unit :=
do p' ← to_expr p,
   n' ← to_expr n,
   tactic.mod_cases n' p'

end interactive
end tactic

example (n : ℤ) :  ¬ (4 ∣ n ^ 2 - 3) :=
begin
  mod_cases n 4,

end

[Heather Macbeth]

Some questions:

• how can I make the syntax mod_cases n 4 using hn, to name the hypothesis produced?
• how can I protect against bad variable inputs (n not an integer, p not a nat, p not positive)?
• can I do the tactic.cases application more efficiently?

[Mario Carneiro]

Since p needs to be a numeral known to the tactic, you can use small_nat to parse it instead of parse pexpr

[Mario Carneiro]

that will restrict users of the tactic to write numerals, i.e. 4 not 2+2 and certainly not k, but that should be fine for this application

[Mario Carneiro]

n on the other hand can be a non-numeral expression, so you want to use parse pexpr there. If you put some kind of punctuation or keyword between n and p then you can parse n at low precedence which is probably nicer if n is a composite expression like a + b

[Mario Carneiro]

The call to mk_app `int.exists_unique_modeq_mem_range will automatically check that n is an integer, but another way to do it is to use i_to_expr ``(%%p : int) instead of to_expr p

[Mario Carneiro]

To parse an optional using hn, you can use parse (tk "using" *> ident)?

[Heather Macbeth]

Thanks Mario! What should I do to protect against the ugly fail if p = 0?

exact tactic failed, type mismatch, given expression has type
  true
but is expected to have type
  as_true (0 < 0)

[Mario Carneiro]

altogether it looks like this:

namespace tactic

meta def mod_cases (n : expr) (p' : ℕ) (H : name) : tactic unit :=
do z ← mk_app `nat.zero [],
  p ← expr.of_nat `(ℕ) p',
  pos ← mk_app `has_lt.lt [z, p],
  assert `h_pos pos, tactic.exact_dec_trivial, -- make a proof that `p` is positive
  hh ← get_local `h_pos,
  w ← mk_app `int.exists_unique_modeq_mem_range [n, p, hh],
  [(p, [w_name, hw_aux₂])] ← tactic.cases w [`k, `hk_aux],
  [(p', [hk_name, H_name])] ← tactic.cases hw_aux₂ [`hk, H],
  tactic.fin_cases_at none none hk_name,
  () <$ all_goals (do
    H' ← get_local H,
    () <$ replace_at norm_cast.derive [H'] ff)


namespace interactive
setup_tactic_parser

meta def mod_cases
  (n : parse parser.pexpr)
  (p : parse small_nat)
  (h : parse (tk "using" *> ident)?) : tactic unit :=
do n' ← to_expr ``(%%n : ℤ),
   tactic.mod_cases n' p (h.get_or_else `H)

end interactive
end tactic

example (n : ℤ) :  ¬ (4 ∣ n ^ 2 - 3) :=
begin
  mod_cases n 4 using a,
end

[Mario Carneiro]

The tactic also puts an unnecessary h_pos in the context; here you only need that expression in order to construct w so there is no need to have it

[Mario Carneiro]

You should use norm_num (or rather norm_num.prove_pos) instead of exact_dec_trivial to prove p is positive

[Mario Carneiro]

Since p' is just a nat here, you can provide a nicer error message with e.g. when (p = 0) (fail "nope")

[Mario Carneiro]

you can even make it a parse error with parse (do n <- small_nat, guard (n != 0), pure n) for the p parameter

[Mario Carneiro]

Here's how you would use norm_num to prove 0 < p:

meta def mod_cases (n : expr) (p' : ℕ) (H : name) : tactic unit :=
do z ← mk_app `nat.zero [],
  p ← expr.of_nat `(ℕ) p',
  pos ← mk_app `has_lt.lt [z, p],
  ic ← mk_instance_cache `(ℕ),
  (_, hh) ← norm_num.prove_pos_nat ic p,
  w ← mk_app `int.exists_unique_modeq_mem_range [n, p, hh],
  [(p, [w_name, hw_aux₂])] ← tactic.cases w [`k, `hk_aux],
  [(p', [hk_name, H_name])] ← tactic.cases hw_aux₂ [`hk, H],
  tactic.fin_cases_at none none hk_name,
  () <$ all_goals (do
    H' ← get_local H,
    () <$ replace_at norm_cast.derive [H'] ff)

[Heather Macbeth]

Thank you! That _ trick is nice, I see I can do

  [(_, [_, hw_aux₂])] ← tactic.cases w [`k, `hk_aux],
  [(_, [hk_name, _])] ← tactic.cases hw_aux₂ [`hk, H],

later as well. I also didn't know how about norm_num.prove_pos_nat to extract a proof of positivity.

Is there a way to get (0:ℕ) faster than z ← mk_app nat.zero []`?

Is there a way to combine the two tactic.cases?

[Heather Macbeth]

And I also couldn't see where to slot in the

parse (do n <- small_nat, guard (n != 0), pure n)

[Mario Carneiro]

For (0:nat) specifically (i.e. you know the type in advance so no typeclass search is needed), you can just use let zero := `(0:nat)

[Mario Carneiro]

Re: combining cases, not really, although you can craft your lemma as an induction principle so that you don't need the cases

[Heather Macbeth]

Also, do I understand correctly that I ought to use get_unused_name to ensure that the cases don't accidentally receive names that already exist in context?

  A₁ ← get_unused_name,
  A₂ ← get_unused_name,
  [(_, [_, hw])] ← tactic.cases w,
  [(_, [hk, _])] ← tactic.cases hw [A₁, A₂],

[Mario Carneiro]

rcases just calls cases repeatedly

[Mario Carneiro]

You usually shouldn't have to worry about that. You only need to provide names if you are routing some names provided by the user

[Mario Carneiro]

you can just use `_ for everything you don't want to name

[Mario Carneiro]

It's a shame that fin_cases doesn't have a lower level interface to save some computation here. I didn't take a deep look at what fin_cases is doing, but here's a version that performs significantly better and skips cases and such:

import tactic.interactive
import tactic.fin_cases
import tactic.norm_cast
import data.int.modeq

namespace int

-- these should exist in data.int.modeq (in preference to the exists version?)
def sigma_unique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) : {z : ℤ // 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]} :=
⟨ a % b, mod_nonneg _ (ne_of_gt hb),
  have a % b < |b|, from mod_lt _ (ne_of_gt hb),
  by rwa abs_of_pos hb at this,
  by simp [modeq] ⟩

def sigma_unique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : {z : ℕ // ↑z < b ∧ ↑z ≡ a [ZMOD b]} :=
let ⟨z, hz1, hz2, hz3⟩ := sigma_unique_equiv a hb in
⟨z.nat_abs, by split; rw [←of_nat_eq_coe, of_nat_nat_abs_eq_of_nonneg hz1]; assumption⟩

end int

namespace tactic

def on_mod_cases (n : ℕ) (a lb : ℤ) (p : Sort*) :=
∀ z, lb ≤ z → z < n → a ≡ z [ZMOD n] → p

lemma on_mod_cases_start (p : Sort*) (a : ℤ) (n : ℕ) (hn : 0 < n)
  (H : on_mod_cases n a 0 p) : p :=
begin
  obtain ⟨a₀, ha₀, ha₀n⟩ := int.sigma_unique_equiv_nat a (by exact_mod_cast hn : (0:ℤ) < n),
  exact H a₀ (by simp) (by simp [ha₀]) ha₀n.symm
end

lemma on_mod_cases_stop {p : Sort*} {n : ℕ} {a n' : ℤ} (h : n' = n) :
  on_mod_cases n a n' p :=
λ z h₁ h₂, (not_lt_of_le h₁ $ h.symm ▸ h₂).elim

lemma on_mod_cases_succ {p : Sort*} {n : ℕ} {a b c : ℤ} (bc : b + 1 = c)
  (h : a ≡ b [ZMOD n] → p) (H : on_mod_cases n a c p) :
  on_mod_cases n a b p :=
λ z h₁ h₂ hm, if he : b = z then h (he.symm ▸ hm) else
  H z (bc ▸ lt_of_le_of_ne h₁ he) h₂ hm

meta def prove_mod_cases (u : level) (p n a : expr) (nn : ℕ) :
  instance_cache → instance_cache → expr → ℕ → tactic (list expr × expr)
| zc nc b nb := if nn ≤ nb then do
    (_, _, _, pr) ← norm_num.prove_nat_uncast zc nc b,
    pure ([], pr)
  else do
    (zc, c, bc) ← norm_num.prove_succ' zc b,
    g ← to_expr_strict ``(%%a ≡ %%b [ZMOD (%%n : ℕ)] → %%p) >>= mk_meta_var,
    (gs, pr) ← prove_mod_cases zc nc c (nb+1),
    pure (g::gs, (expr.const ``on_mod_cases_succ [u]).mk_app [p, n, a, b, c, bc, g, pr])

meta def mod_cases (a : expr) (nn : ℕ) (H : name) : tactic unit :=
focus1 $ do
  p ← target,
  zc ← mk_instance_cache `(ℤ),
  nc ← mk_instance_cache `(ℕ),
  (nc, n) ← nc.of_nat nn,
  (nc, hn) ← norm_num.prove_pos_nat nc n,
  refine ``(on_mod_cases_start _ %%a %%n %%hn _),
  expr.sort u ← infer_type p | failure,
  (gs, pr) ← try_for 1000 (prove_mod_cases u p n a nn zc nc `(0:ℤ) 0),
  exact pr,
  set_goals gs,
  () <$ all_goals (intro H)

namespace interactive
setup_tactic_parser

meta def mod_cases
  (n : parse parser.pexpr)
  (p : parse (do n ← small_nat, guard (n ≠ 0), pure n))
  (h : parse (tk "using" *> ident)?) : tactic unit :=
do n' ← to_expr ``(%%n : ℤ),
   tactic.mod_cases n' p (h.get_or_else `H)

end interactive
end tactic

example (n : ℤ) :  ¬ (4 ∣ n ^ 2 - 3) :=
begin
  mod_cases n 100 using a,
end

[Mario Carneiro]

@Heather Macbeth

[Heather Macbeth]

@Mario Carneiro This is very interesting, I will study it! But also, perhaps you could PR it? :). Much better than I came up with.

[Mario Carneiro]

Also, I was going to mention that using h is not a conventional way to ask for a name in a tactic; I would suggest h : instead, or perhaps with h

[Mario Carneiro]

there aren't too many tactics using using, but those that do expect an expression after it

[Heather Macbeth]

Mario Carneiro said:

there aren't too many tactics using using, but those that do expect an expression after it

Indeed, I realised later and changed to with in my local version!