symm tactic

This implements the symm tactic, which can apply symmetry theorems to either the goal or a hypothesis.

def Lean.Meta.Symm.symmExt.config : Lean.Meta.WhnfCoreConfig

Discrimation tree settings for the symm extension.

Equations

• Lean.Meta.Symm.symmExt.config = { iota := true, beta := true, proj := Lean.Meta.ProjReductionKind.yesWithDelta, zeta := true, zetaDelta := true }

opaque Lean.Meta.Symm.symmExt : Lean.SimpleScopedEnvExtension (Lake.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lake.Name)

Environment extensions for symm lemmas

def Lean.Expr.getSymmLems (tgt : Lean.Expr) : Lean.MetaM (Array Lake.Name)

Return the symmetry lemmas that match the target type.

Equations

• ((rel.app arg).app arg_1).getSymmLems = do let __do_lift ← Lean.getEnv (Lean.ScopedEnvExtension.getState Lean.Meta.Symm.symmExt __do_lift).getMatch rel Lean.Meta.Symm.symmExt.config
• tgt.getSymmLems = Lean.throwError (Lean.toMessageData "symmetry lemmas only apply to binary relations, not" ++ Lean.toMessageData (Lean.indentExpr tgt) ++ Lean.toMessageData "")

def Lean.Expr.applySymm (e : Lean.Expr) : Lean.MetaM Lean.Expr

Given a term e : a ~ b, construct a term in b ~ a using @[symm] lemmas.

Equations

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

def Lean.MVarId.applySymm (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Apply a symmetry lemma (i.e. marked with @[symm]) to a metavariable.

The type of g should be of the form a ~ b, and is used to index the symm lemmas.

Equations

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

def Lean.MVarId.applySymmAt (h : Lean.FVarId) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Use a symmetry lemma (i.e. marked with @[symm]) to replace a hypothesis in a goal.

Equations

• Lean.MVarId.applySymmAt h g = do let h' ← (Lean.Expr.fvar h).applySymm let __do_lift ← g.replace h h' pure __do_lift.mvarId

def Lean.MVarId.symmSaturate (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

For every hypothesis h : a ~ b where a @[symm] lemma is available, add a hypothesis h_symm : b ~ a.

Equations

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