The `#defeq_abuse` tactic and command combinators #

WARNING: #defeq_abuse is an experimental tool intended to assist with breaking changes to transparency handling (associated with backward.isDefEq.respectTransparency). Its syntax may change at any time, and it may not behave as expected. Please report unexpected behavior on Zulip.

#defeq_abuse in tac runs tac with backward.isDefEq.respectTransparency both true and false. If the tactic succeeds with false but fails with true, it identifies the specific isDefEq checks that fail with the stricter setting, helping to diagnose where Mathlib relies on definitional equality that isn't available at instance transparency.

#defeq_abuse in cmd does the same for commands (e.g. instance declarations), where type class synthesis failures may occur during elaboration rather than during a tactic. It additionally traces Meta.synthInstance to group isDefEq failures by the synthesis application that triggered them.

Usage #

Tactic mode #

#defeq_abuse in rw [Set.disjoint_singleton_right]

will report something like:

Tactic fails with `backward.isDefEq.respectTransparency true` but succeeds with `false`.
The following isDefEq checks are the root causes of the failure:
  (i : ℕ) → (fun a ↦ Prop) i =?= Set ℕ

Command mode #

#defeq_abuse in
instance {V : Type} [AddCommGroup V] [Module ℝ V] {l : Submodule ℝ V} :
    Module.Free ℝ l := Module.Free.of_divisionRing ℝ l

will report the synthesis failures grouped by instance application.

source

def Mathlib.Tactic.DefEqAbuse.defeqAbuse :

Lean.ParserDescr

WARNING: #defeq_abuse is an experimental tool intended to assist with breaking changes to transparency handling. Its syntax may change at any time, and it may not behave as expected. Please report unexpected behavior on Zulip.

The tactic still executes (using the permissive setting if needed), so proofs remain valid during debugging.

Equations

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

Instances For

source

def Mathlib.Tactic.DefEqAbuse.defeqAbuseCmd :

Lean.ParserDescr

WARNING: #defeq_abuse is an experimental tool intended to assist with breaking changes to transparency handling. Its syntax may change at any time, and it may not behave as expected. Please report unexpected behavior on Zulip.

#defeq_abuse in cmd runs cmd with backward.isDefEq.respectTransparency both true and false. If the command succeeds with false but fails with true, it identifies the specific synthesis applications and isDefEq checks that fail with the stricter setting.

This is useful for diagnosing instance declarations or other commands where type class synthesis failures occur during elaboration rather than within a tactic.

The command is re-executed with the permissive setting so that it actually takes effect.