The reduction command

Given a problem p : Minimization D R and fresh identifiers red and q, a user can use the reduction command as follows:

reduction red/q : p := by ...

Placing the cursor on after the by keyword opens up a tactic environment where the goal is to prove p ≼ ?q. After applying a sequence of tactics that transform the goal into, say r ≼ ?q, the user can leave the reduction environment and two new definitions will be added to the environment:

• q := r,
• red : p ≼ q.

Writing reduction* instead of reduction will also generate a backward solution map at the level of floats.

It is essentially the same as CvxLean/Command/Equivalence.lean, except that the goal is to prove a reduction instead of an equivalence. We note that proving that two problems are equivalent is usually preferred.

def CvxLean.runReductionTactic (mvarId : Lean.MVarId) (stx : Lean.Syntax) : Lean.Elab.TermElabM Unit

Run a transformation tactic indicating that a reduction is expected.

Equations

• CvxLean.runReductionTactic mvarId stx = CvxLean.Meta.runTransformationTactic CvxLean.Meta.TransformationGoal.Reduction mvarId stx

def CvxLean.elabReductionProof (lhs : Lean.Expr) (rhsName : Lean.Name) (stx : Lean.Syntax) : Lean.Elab.TermElabM (Lean.Expr × Lean.Expr)

Run reduction tactic and return both the right-hand term (q) and the reduction proof, of type Reduction p q.

Equations

• CvxLean.elabReductionProof lhs rhsName stx = CvxLean.Meta.elabTransformationProof CvxLean.Meta.TransformationGoal.Reduction lhs rhsName stx

def CvxLean.reduction : Lean.ParserDescr

Open a reduction environment.

Equations

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

def CvxLean.reductionAndBwdMap : Lean.ParserDescr

Open a reduction environment and try to generate a computable backward map.

Equations

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

def CvxLean.evalReductionAux (probIdStx : Lean.TSyntax `ident) (redIdStx : Lean.TSyntax `ident) (xs : Array (Lean.Syntax × Lean.Expr)) (lhsStx : Lean.Syntax) (proofStx : Lean.TSyntax `Lean.Parser.Term.byTactic) (bwdMap : Bool) : Lean.Elab.TermElabM Unit

Open a reduction environment with a given left-hand-side problem (lhsStx) and perhaps some parameters (xs). From this, a reduction goal is set to a target problem which is represented by a metavariable. The proof (proofStx) is evaluated to produce the desired reduction. The metavariable is then instantiated and the resulting problem is stored using the identifier probIdStx. The reduction witness is stored according to the identifier redIdStx. Optionally, a floating-point backward solution map is created. See evalReduction and evalReductionAndBwdMap.

Equations

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

def CvxLean.evalReduction : Lean.Elab.Command.CommandElab

Create reduction command. It is similar to the equivalence command, but requires a Reduction instead of an Equivalence.

Equations

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

def CvxLean.evalReductionAndBwdMap : Lean.Elab.Command.CommandElab

Same as reduction but also adds the backward map to the environment.

Equations

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