simp@

Stream: general

[Kyle Miller]

Sometimes simp lemmas need local assumptions for applicability, and what I've usually done is add them to the simp set manually. I remembered today that there's also the discharger option, which you can supply with a tactic that's run to deal with extra goals that crop up.

-- fails
example (n m m' : ℚ) (h : n ≠ 0) : m * n / n = m := by simp

-- succeeds
example (n m m' : ℚ) (h : n ≠ 0) : m * n / n = m := by simp [h]
example (n m m' : ℚ) (h : n ≠ 0) : m * n / n = m := by simp { discharger := tactic.assumption }

@Scott Kovach and I thought it might be interesting if this were more accessible, so we added a @ flag to join ! and ?:

-- succeeds
example (n m m' : ℚ) (h : n ≠ 0) : m * n / n = m := by mysimp@

In addition to setting the discharger, it also sets contextual := tt, since these are sort of like additional assumptions.

Is this a good idea to have in simp? Or is it just a step down the road of inscrutability?

[Kyle Miller]

Implementation:

namespace tactic
namespace interactive
setup_tactic_parser

@[derive [has_reflect, decidable_eq]]
inductive mysimp_flags
| use_iota_eqn
| discharge_assumptions
| trace_lemmas

meta def mysimp_flags.apply : mysimp_flags → simp_config_ext → simp_config_ext
| mysimp_flags.use_iota_eqn cfg :=
  { iota_eqn := tt, ..cfg }
| mysimp_flags.discharge_assumptions cfg :=
  { contextual := tt, discharger := tactic.assumption <|> cfg.discharger, ..cfg }
| mysimp_flags.trace_lemmas cfg :=
  { trace_lemmas := tt, ..cfg }

meta def mysimp
  (flags : parse $
    ((with_desc "!" $ tk "!" >> pure mysimp_flags.use_iota_eqn)
    <|> (with_desc "@" $ tk "@" >> pure mysimp_flags.discharge_assumptions)
    <|> (with_desc "?" $ tk "?" >> pure mysimp_flags.trace_lemmas))*)
  (no_dflt : parse only_flag) (hs : parse simp_arg_list) (attr_names : parse with_ident_list)
              (locat : parse location) (cfg : simp_config_ext := {}) : tactic unit :=
let cfg := flags.foldr mysimp_flags.apply cfg in
propagate_tags $
do lms ← simp_core cfg.to_simp_config cfg.discharger no_dflt hs attr_names locat,
  if cfg.trace_lemmas then
    let a := if flags.mem mysimp_flags.discharge_assumptions then "@" else ""
    in trace (↑("Try this: mysimp" ++ a ++ " only ") ++ to_fmt lms.to_list) else skip

end interactive
end tactic

[Eric Wieser]

Is simp { discharger := tactic.assumption } different to simp [*]?

[Kyle Miller]

@Eric Wieser Good point, I didn't realize [*] and simp only interacted correctly. (Or rather, I think I might have forgotten about [*].)

[Kyle Miller]

I'm not sure what the differences between simp {discharger := tactic.assumption} and simp [*] might be, if any.

[Gabriel Ebner]

IIRC simp uses simp as the default discharger, so simp [*] will usually prove a bit more than simp {discharger:=assumption}.

[Kyle Miller]

@Gabriel Ebner As I understand it, simp effectively uses discharger <|> simp to discharge goals, and since the default value for discharger is tactic.fail it generally works the way you describe, though simp [*] {discharger := tactic.assumption} should prove at least as much as simp [*] (and possibly exactly as much).