symm tactic

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

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

Environment extensions for symm lemmas

def Lean.Expr.symmAux {α : Type} (tgt : Lean.Expr) (k : Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MetaM α) : Lean.MetaM α

Internal implementation of Lean.Expr.symm, Lean.MVarId.symm, 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.symm this result will be a new Expr, and in Lean.MVarId.symm and Lean.MVarId.symmAt this result will be a new goal.

Equations

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

def Lean.Expr.symm (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.symmAux (tgt : Lean.Expr) (k : Lean.Expr → Array Lean.Expr → Lean.Expr → Lean.MVarId → Lean.MetaM Lean.MVarId) (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Internal implementation of Lean.MVarId.symm 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

• Lean.MVarId.symmAux tgt k g = Lean.Expr.symmAux tgt fun lem args body => do let g' ← k lem args body g let __do_lift ← Lean.MVarId.getTag g Lean.MVarId.setTag g' __do_lift pure g'

def Lean.MVarId.symm (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.symmAt (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.symmAt h g = do let h' ← Lean.Expr.symm (Lean.Expr.fvar h) let __do_lift ← Lean.MVarId.replace g h h' none 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.

def Mathlib.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.

def Mathlib.Tactic.tacticSymm_saturate : Lean.ParserDescr

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

Equations

• Mathlib.Tactic.tacticSymm_saturate = Lean.ParserDescr.node `Mathlib.Tactic.tacticSymm_saturate 1024 (Lean.ParserDescr.nonReservedSymbol "symm_saturate" false)