Infrastructure to work with Equivalence types as expressions. We also define some basic tactics that work on equivalence goals:

• equivalence_rfl closes a goal by reflexivity.
• equivalence_symm applies symmetry.
• equivalence_trans applies transitivity.
• equivalence_step => ... allows users to apply one equivalence step in the equivalence command by first applying transitivity as otherwise the goal would be closed immediately.

structure CvxLean.Meta.EquivalenceExpr : Type

Equivalence type components as expressions.

• domainLHS : Lean.Expr
• domainRHS : Lean.Expr
• codomain : Lean.Expr
• codomainPreorder : Lean.Expr
• lhs : Lean.Expr
• rhs : Lean.Expr

def CvxLean.Meta.EquivalenceExpr.toMinimizationExprLHS (eqvExpr : CvxLean.Meta.EquivalenceExpr) : Lean.MetaM CvxLean.Meta.MinimizationExpr

Equations

• eqvExpr.toMinimizationExprLHS = do let __do_lift ← Lean.Meta.whnf eqvExpr.lhs CvxLean.Meta.MinimizationExpr.fromExpr __do_lift

def CvxLean.Meta.EquivalenceExpr.toMinimizationExprRHS (eqvExpr : CvxLean.Meta.EquivalenceExpr) : Lean.MetaM CvxLean.Meta.MinimizationExpr

Equations

• eqvExpr.toMinimizationExprRHS = do let __do_lift ← Lean.Meta.whnf eqvExpr.rhs CvxLean.Meta.MinimizationExpr.fromExpr __do_lift

def CvxLean.Meta.EquivalenceExpr.toExpr (eqvExpr : CvxLean.Meta.EquivalenceExpr) : Lean.Expr

Equations

• eqvExpr.toExpr = Lean.mkApp6 (Lean.mkConst `Minimization.Equivalence) eqvExpr.domainLHS eqvExpr.domainRHS eqvExpr.codomain eqvExpr.codomainPreorder eqvExpr.lhs eqvExpr.rhs

def CvxLean.Meta.EquivalenceExpr.fromExpr (e : Lean.Expr) : Lean.MetaM CvxLean.Meta.EquivalenceExpr

Equations

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

def CvxLean.Meta.EquivalenceExpr.fromGoal (goal : Lean.MVarId) : Lean.MetaM CvxLean.Meta.EquivalenceExpr

Equations

• CvxLean.Meta.EquivalenceExpr.fromGoal goal = do let __do_lift ← goal.getDecl let goalType ← Lean.Meta.whnf __do_lift.type CvxLean.Meta.EquivalenceExpr.fromExpr goalType

def CvxLean.Meta.tacticEquivalence_rfl : Lean.ParserDescr

Equations

• CvxLean.Meta.tacticEquivalence_rfl = Lean.ParserDescr.node `CvxLean.Meta.tacticEquivalence_rfl 1024 (Lean.ParserDescr.nonReservedSymbol "equivalence_rfl" false)

def CvxLean.Meta.tacticEquivalence_symm : Lean.ParserDescr

Equations

• CvxLean.Meta.tacticEquivalence_symm = Lean.ParserDescr.node `CvxLean.Meta.tacticEquivalence_symm 1024 (Lean.ParserDescr.nonReservedSymbol "equivalence_symm" false)

def CvxLean.Meta.tacticEquivalence_trans : Lean.ParserDescr

Equations

• CvxLean.Meta.tacticEquivalence_trans = Lean.ParserDescr.node `CvxLean.Meta.tacticEquivalence_trans 1024 (Lean.ParserDescr.nonReservedSymbol "equivalence_trans" false)

def CvxLean.Meta.tacticEquivalence_step__ : Lean.ParserDescr

Equations

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