Zulip Chat Archive

Stream: general

Topic: rwa using


Kenny Lau (Jun 26 2020 at 06:05):

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

Kenny Lau (Jun 26 2020 at 06:06):

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

Kenny Lau (Jun 26 2020 at 06:06):

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

Anne Baanen (Jun 26 2020 at 08:27):

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 (Jun 26 2020 at 08:28):

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

Anne Baanen (Jun 26 2020 at 08:33):

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.


Last updated: Dec 20 2023 at 11:08 UTC