Rewriting at specified locations

Many metaprograms have the following general structure: the input is an expression e and the output is a new expression e', together with a proof that e = e'.

This file provides convenience functions to turn such a metaprogram into a variety of tactics: using the metaprogram to modify the goal, a specified hypothesis, or (via Tactic.Location) a combination of these.

def Lean.Elab.Tactic.withNondepPropLocation (loc : Location) (atLocal : FVarId → TacticM Unit) (atTarget : TacticM Unit) (failed : MVarId → TacticM Unit) : TacticM Unit

Runs the given atLocal and atTarget methods on each of the locations selected by the given loc.

• If loc is a list of locations, runs at each specified hypothesis (and finally the goal if ⊢ is included), and fails if any of the tactic applications fail.
• If loc is *, runs at the target and at the nondependent Prop hypotheses in reversed order (those produced by Lean.MVarId.getNondepPropHyps), calling failed if no location succeeds.

The implementation adapts Lean.Elab.Tactic.withLocation with a restricted wildcard.

Equations

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

def Lean.Elab.Tactic.mapNondepPropLocation {α : Type} (loc : Location) (atLocal : FVarId → TacticM α) (atTarget : TacticM α) : TacticM (Array α)

Collect the values from running the atLocal and atTarget methods on each of the locations selected by the given loc.

• If loc is a list of locations, collects the results of running at each specified hypothesis (and finally the goal if ⊢ is included), and fails if any of the applications fail.
• If loc is *, collects the results of running at the target and at the nondependent Prop hypotheses (those produced by Lean.MVarId.getNondepPropHyps). Locations where the application fails are skipped, so the result can be empty.

Equations

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

inductive Mathlib.Tactic.BehaviorIfUnchanged : Type

Different settings of communicating about a tactic which made no progress: do nothing (keep silent), print a warning or throw an error.

• silent : BehaviorIfUnchanged

  Stay silent if this action has no effect.

• warning : BehaviorIfUnchanged

  Log a warning if this action has no effect.

• error : BehaviorIfUnchanged

  Throw an error if this action has no effect.

@[instance_reducible]

instance Mathlib.Tactic.instBEqBehaviorIfUnchanged : BEq BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instBEqBehaviorIfUnchanged = { beq := Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq }

def Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq : BehaviorIfUnchanged → BehaviorIfUnchanged → Bool

Equations

• Mathlib.Tactic.instBEqBehaviorIfUnchanged.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[instance_reducible]

instance Mathlib.Tactic.instInhabitedBehaviorIfUnchanged : Inhabited BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instInhabitedBehaviorIfUnchanged = { default := Mathlib.Tactic.instInhabitedBehaviorIfUnchanged.default }

@[instance_reducible]

instance Mathlib.Tactic.instReprBehaviorIfUnchanged : Repr BehaviorIfUnchanged

Equations

• Mathlib.Tactic.instReprBehaviorIfUnchanged = { reprPrec := Mathlib.Tactic.instReprBehaviorIfUnchanged.repr }

def Mathlib.Tactic.instReprBehaviorIfUnchanged.repr : BehaviorIfUnchanged → Nat → Std.Format

Equations

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

def Mathlib.Tactic.transformAtTarget (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (ifUnchanged : BehaviorIfUnchanged) (goal : Lean.MVarId) : ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)

Use the procedure m to rewrite the provided goal.

Assumes proc is not surrounded by backticks.

Equations

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

def Mathlib.Tactic.transformAtLocalDecl (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (ifUnchanged : BehaviorIfUnchanged) (mayCloseGoal : Bool) (fvarId : Lean.FVarId) (goal : Lean.MVarId) : ReaderT Lean.Meta.Simp.Context Lean.MetaM (Option Lean.MVarId)

Use the procedure m to rewrite hypothesis fvarId.

The simpTheorems of the simp-context carried with m will be modified to remove fvarId; this ensures that if the procedure m involves rewriting by this SimpTheoremsArray, then, e.g., h : x = y is not transformed (by rewriting h) to True.

Assumes proc is not surrounded by backticks.

Equations

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

def Mathlib.Tactic.transformAtLocation (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (loc : Lean.Elab.Tactic.Location) (ifUnchanged : BehaviorIfUnchanged := BehaviorIfUnchanged.error) (mayCloseGoalFromHyp : Bool := false) (ctx : Lean.Meta.Simp.Context := default) : Lean.Elab.Tactic.TacticM Unit

Use the procedure m to transform at specified locations (hypotheses and/or goal).

Assumes proc is not surrounded by backticks.

Equations

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

def Mathlib.Tactic.transformAtNondepPropLocation (m : Lean.Expr → ReaderT Lean.Meta.Simp.Context Lean.MetaM Lean.Meta.Simp.Result) (proc : String) (loc : Lean.Elab.Tactic.Location) (ifUnchanged : BehaviorIfUnchanged := BehaviorIfUnchanged.error) (mayCloseGoalFromHyp : Bool := false) (ctx : Lean.Meta.Simp.Context := default) : Lean.Elab.Tactic.TacticM Unit

Use the procedure m to transform at specified locations (hypotheses and/or goal).

In the wildcard case (*), filter out all dependent and/or non-Prop hypotheses.

Assumes proc is not surrounded by backticks.

Equations

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