bdsimp tactic

bdsimp is a backward compatibility macro for dsimp that allows dependent rewrites inside depended-on positions.

def bdsimp : Lean.ParserDescr

bdsimp definitionally simplifies the goal. This is a backward compatibility macro for dsimp. Like dsimp, it applies only theorems that hold by reflexivity, and the result is guaranteed to be definitionally equal to the input. The difference is that bdsimp allows any theorem whose proof is reflexivity, while dsimp requires the proof to hold at .instances transparency level.

This tactic is a temporary workaround. bdsimp also rewrites in depended-on positions, which means the result can fail to typecheck at the expected .instances transparency level. For example:

@[expose] def two := 2
@[defeq] lemma two_eq : two = 2 := by rfl
instance : NeZero two := inferInstanceAs (NeZero 2)

example (x : Fin two) : x * 0 = 0 := by
  bdsimp only [two_eq]
  fail_if_success rw [Fin.mul_zero] -- Fails: `x : Fin two` but `· * · : Fin 2 → Fin 2 → Fin 2`

This tactic supports all options supported by dsimp.

Equations

• One or more equations did not get rendered due to their size.