There is a hierarchy on the possible transformations between two problems. Most crucially, a tactic that builds an Equivalence should also build a Reduction. And both equivalence and reduction-preserving tactics should build backward maps.

This file avoid unnecessary code duplication by providing a common interface for all transformation-preserving tactics. When building a tactic, a user must define an EquivalenceBuilder, a ReductionBuilder or a RelaxationBuilder. These builders can then be turned into tactics using the toTactic method.

inductive CvxLean.Meta.TransformationGoal : Type

• Solution: CvxLean.Meta.TransformationGoal
• Equivalence: CvxLean.Meta.TransformationGoal
• Reduction: CvxLean.Meta.TransformationGoal
• Relaxation: CvxLean.Meta.TransformationGoal

def CvxLean.Meta.TransformationGoal.isTransitive : CvxLean.Meta.TransformationGoal → Bool

Equations

• x.isTransitive = match x with | CvxLean.Meta.TransformationGoal.Solution => false | x => true

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

Equations

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

def CvxLean.Meta.TransformationGoal.applyTransitivity (transf : CvxLean.Meta.TransformationGoal) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM (Lean.MVarId × Lean.MVarId)

Applies appropriate transitivity tactic to the goal.

Equations

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

def CvxLean.Meta.RelaxationBuilder (α : Type) : Type

Given a relaxation goal in the form of a RelaxationExpr and the MVarId of the current goal, provide a tactic to close it.

Equations

• CvxLean.Meta.RelaxationBuilder α = (CvxLean.Meta.RelaxationExpr → Lean.MVarId → Lean.Elab.Tactic.TacticM α)

def CvxLean.Meta.RelaxationBuilder.toTactic {α : Type} (builder : CvxLean.Meta.RelaxationBuilder α) : Lean.Elab.Tactic.TacticM α

Equations

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

def CvxLean.Meta.ReductionBuilder (α : Type) : Type

Given a reduction goal in the form of a ReductionExpr and the MVarId of the current goal, provide a tactic to close it.

Equations

• CvxLean.Meta.ReductionBuilder α = (CvxLean.Meta.ReductionExpr → Lean.MVarId → Lean.Elab.Tactic.TacticM α)

def CvxLean.Meta.ReductionBuilder.toTactic {α : Type} (builder : CvxLean.Meta.ReductionBuilder α) : Lean.Elab.Tactic.TacticM α

Equations

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

def CvxLean.Meta.EquivalenceBuilder (α : Type) : Type

Given an equivalence goal in the form of a EquivalenceExpr and the MVarId of the current goal, provide a tactic to close it.

Equations

• CvxLean.Meta.EquivalenceBuilder α = (CvxLean.Meta.EquivalenceExpr → Lean.MVarId → Lean.Elab.Tactic.TacticM α)

def CvxLean.Meta.EquivalenceBuilder.toTactic {α : Type} (builder : CvxLean.Meta.EquivalenceBuilder α) : Lean.Elab.Tactic.TacticM α

Equations

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

def CvxLean.Meta.runTransformationTactic (transf : CvxLean.Meta.TransformationGoal) (mvarId : Lean.MVarId) (stx : Lean.Syntax) : Lean.Elab.TermElabM Unit

Equations

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

def CvxLean.Meta.elabTransformationProof (transf : CvxLean.Meta.TransformationGoal) (lhs : Lean.Expr) (rhsName : Lean.Name) (stx : Lean.Syntax) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Wraper that works for all defined transformations, elaborating syntax into the RHS expression and a proof of the relation with the LHS. The RHS can be named so that the metavariable displayed in the infoview corresponds to a user-defined name.

Equations

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