rwa using

Stream: general

[Kenny Lau]

Can we have rwa [foo, bar] using (baz h1 h2) just like simpa using?

[Kenny Lau]

Because I find myself using by { rw [foo, bar], exact baz h1 h2 } a lot

[Kenny Lau]

After the ban of semicolons I feel like this is the correct approach

[Anne Baanen]

Barely tested because I need to recompile core Lean, but this seems to work:

meta def rwa' (q : parse rw_rules) (l : parse location)
  (tgt : parse (tk "using" *> texpr)?) (cfg : rewrite_cfg := {}) : tactic unit :=
let try_rw := λ (ls : list (option name)), ls.mmap (λ n, try (rewrite q (loc.ns [n]) cfg)) in
match tgt with
| none := rewrite q l cfg >> try assumption
| some e := do
  e ← i_to_expr e <|> do {
    ty ← target,
    e ← i_to_expr_strict ``(%%e : %%ty), -- for positional error messages, don't care about the result
    pty ← pp ty, ptgt ← pp e,
    -- fail deliberately, to advise regarding `rw; exact` usage
    fail ("rwa failed, 'using' expression type not directly " ++
      "inferrable. try:\n\nrwa ... using\nshow " ++
      to_fmt pty ++ ",\nfrom " ++ ptgt : format) },
  match e with
  | local_const _ lc _ _ := try_rw [some lc, none] >> get_local lc >>= tactic.exact
  | e := do
    t ← infer_type e,
    assertv `this t e >> try_rw [some `this, none] >> get_local `this >>= tactic.exact
  end
end

[Anne Baanen]

(This is essentially the code for simpa but with simp renamed to rw everywhere)

[Anne Baanen]

Thinking about it some more, a better generalization would be to let convert accept a tactic for the equalities that it generates. Then we wouldn't need ringa, abela, etc.