Linter for simplification lemmas

This files defines several linters that prevent common mistakes when declaring simp lemmas:

• simpNF checks that the left-hand side of a simp lemma is not simplified by a different lemma.
• simpVarHead checks that the head symbol of the left-hand side is not a variable.
• simpComm checks that commutativity lemmas are not marked as simplification lemmas.

structure Batteries.Tactic.Lint.SimpTheoremInfo : Type

The data associated to a simp theorem.

• hyps : Array Lean.Expr

  The hypotheses of the theorem

• lhs : Lean.Expr

  The thing to replace

• rhs : Lean.Expr

  The result of replacement

def Batteries.Tactic.Lint.isCondition (h : Lean.Expr) : Lean.MetaM Bool

Is this hypothesis a condition that might turn into a simp side-goal? i.e. is it a proposition that isn't marked as instance implicit?

Equations

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

def Batteries.Tactic.Lint.withSimpTheoremInfos {α : Type} (ty : Lean.Expr) (k : SimpTheoremInfo → Lean.MetaM α) : Lean.MetaM (Array α)

Runs the continuation on all the simp theorems encoded in the given type.

Equations

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

def Batteries.Tactic.Lint.isSimpEq (a b : Lean.Expr) (whnfFirst : Bool := true) : Lean.MetaM Bool

Checks whether two expressions are equal for the simplifier. That is, they are reducibly-definitional equal, and they have the same head symbol.

Equations

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

def Batteries.Tactic.Lint.checkAllSimpTheoremInfos (ty : Lean.Expr) (k : SimpTheoremInfo → Lean.MetaM (Option Lean.MessageData)) : Lean.MetaM (Option Lean.MessageData)

Constructs a message from all the simp theorems encoded in the given type.

Equations

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

def Batteries.Tactic.Lint.isSimpTheorem (declName : Lean.Name) : Lean.MetaM Bool

Returns true if this is a @[simp] declaration.

Equations

• Batteries.Tactic.Lint.isSimpTheorem declName = do let __do_lift ← liftM Lean.Meta.getSimpTheorems pure (Lean.PersistentHashSet.contains __do_lift.lemmaNames (Lean.Meta.Origin.decl declName))

def Lean.Meta.DiscrTree.elements {α : Type} (d : DiscrTree α) : Array α

Returns the list of elements in the discrimination tree.

Equations

• d.elements = d.root.foldl (fun (arr : Array α) (x : Lean.Meta.DiscrTree.Key) => Lean.Meta.DiscrTree.elements.trieElements✝ arr) #[]

def Batteries.Tactic.Lint.decorateError {α : Type} (msg : Lean.MessageData) (k : Lean.MetaM α) : Lean.MetaM α

Add message msg to any errors thrown inside k.

Equations

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

def Batteries.Tactic.Lint.formatLemmas (usedSimps : Lean.Meta.Simp.UsedSimps) (simpName : String) (higherOrder : Option Bool) : Lean.MetaM Lean.MessageData

Render the list of simp lemmas.

Equations

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

def Batteries.Tactic.Lint.simpNF : Linter

A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.

Equations

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

def LibraryNote.«simp-normal form» : Batteries.Util.LibraryNote

This note gives you some tips to debug any errors that the simp-normal form linter raises.

The reason that a lemma was considered faulty is because its left-hand side is not in simp-normal form. These lemmas are hence never used by the simplifier.

This linter gives you a list of other simp lemmas: look at them!

Here are some tips depending on the error raised by the linter:

1. 'the left-hand side reduces to XYZ': you should probably use XYZ as the left-hand side.

2. 'simp can prove this': This typically means that lemma is a duplicate, or is shadowed by another lemma:

   2a. Always put more general lemmas after specific ones:

   @[simp] lemma zero_add_zero : 0 + 0 = 0 := rfl
   @[simp] lemma add_zero : x + 0 = x := rfl
   

   And not the other way around! The simplifier always picks the last matching lemma.

   2b. You can also use @[priority] instead of moving simp-lemmas around in the file.

   Tip: the default priority is 1000. Use @[priority 1100] instead of moving a lemma down, and @[priority 900] instead of moving a lemma up.

   2c. Conditional simp lemmas are tried last. If they are shadowed just remove the simp attribute.

   2d. If two lemmas are duplicates, the linter will complain about the first one. Try to fix the second one instead! (You can find it among the other simp lemmas the linter prints out!)

3. 'try_for tactic failed, timeout': This typically means that there is a loop of simp lemmas. Try to apply squeeze_simp to the right-hand side (removing this lemma from the simp set) to see what lemmas might be causing the loop.

   Another trick is to set_option trace.simplify.rewrite true and then apply try_for 10000 { simp } to the right-hand side. You will see a periodic sequence of lemma applications in the trace message.

Equations

• LibraryNote.«simp-normal form» = default

def Batteries.Tactic.Lint.simpVarHead : Linter

A linter for simp lemmas whose lhs has a variable as head symbol, and which hence never fire.

Equations

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

def Batteries.Tactic.Lint.simpComm : Linter

A linter for commutativity lemmas that are marked simp.

Equations

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