symm tactic

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

def Std.Tactic.symmExt.config : Lean.Meta.WhnfCoreConfig

Discrimation tree settings for the symm extension.

Equations

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

opaque Std.Tactic.symmExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)

Environment extensions for symm lemmas

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.Expr.applySymm.go (tgt : Lean.Expr) {α : Type} (k : Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM α) : Lean.MetaM α

Internal implementation of Lean.Expr.applySymm, Lean.MVarId.applySymm, and the user-facing tactic.

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

k lem args body should calculate a result, given a candidate symm lemma lem, which will have type ∀ args, body.

In Lean.Expr.applySymm this result will be a new Expr, and in Lean.MVarId.applySymm and Lean.MVarId.applySymmAt this result will be a new goal.

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.

Equations

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

def Lean.MVarId.applySymm.go (tgt : Lean.Expr) (g : Lean.MVarId) (k : Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MVarId → Lean.MetaM Lean.MVarId) : Lean.MetaM Lean.MVarId

Internal implementation of Lean.MVarId.applySymm and the user-facing tactic.

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

k lem args body goal should transform goal into a new goal, given a candidate symm lemma lem, which will have type ∀ args, body. Depending on whether we are working on a hypothesis or a goal, k will internally use either replace or assign.

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.applySymm (Lean.Expr.fvar h) let __do_lift ← Lean.MVarId.replace g h h' none pure __do_lift.mvarId

def Std.Tactic.tacticSymm_ : Lean.ParserDescr

• symm applies to a goal whose target has the form t ~ u where ~ is a symmetric relation, that is, a relation which has a symmetry lemma tagged with the attribute [symm]. It replaces the target with u ~ t.
• symm at h will rewrite a hypothesis h : t ~ u to h : u ~ t.

Equations

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