param_guard — descent through guarded squares

param_guard closes a goal Related enc t t', an equation enc t = t' (or an equation bridged to Related id), or an equivalence r a b ↔ br a' b' by descending through the registered squares, total and guarded (Transfer.Base.RelatedOn). At each node it applies rcongrBinOpOn, rcongrUnOpOn or rcongrRelOn; the total squares take part through the instances RelatedBinOp.toOn and RelatedUnOp.toOn with guard True.

The guard of each node is a proposition about the abstract operands of that node, for example b ≤ a at a - b or (a - b) < 2 ^ 64 ∧ s < 64 at (a - b) >>> s. The discharger runs on it: transfer_guard_disch by default, or the tactic given as param_guard (disch := tac). A guard the discharger does not close is left as a goal, so param_guard returns exactly the side conditions it could not prove.

When a Related subgoal has no registered square and no leaf closes it, param_guard fails with an error that names that subgoal, its abstract and encoded heads, and the encoding. The error is raised at the leaf, not at the root of the op-tree.

param_solve runs the same guarded descent with the default discharger and fails over to its closure leaf when a guard is not closed.

def Transfer.paramGuardLeafError (g : Lean.MVarId) : Lean.MetaM Lean.MessageData

The error for a Related goal that no registered square and no leaf closes: it names the goal, the heads of its abstract and encoded sides, and the encoding.

Equations

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

def Transfer.paramGuardCloses (tac : Lean.Syntax) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM Bool

Run tac on g; return true and keep the result when it closes g, else restore the state and return false.

Equations

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

def Transfer.paramGuardApply (rule : Lean.Syntax) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM (Option (List Lean.MVarId))

Apply the rule rule to g; return its new goals, or none (state restored) when the rule does not apply.

Equations

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

def Transfer.paramGuardReshape (g : Lean.MVarId) : Lean.MetaM Lean.MVarId

Reshape an equation enc t = t' whose sides have a type other than that of t into the goal Related enc t t', and return that goal. Metadata around the left-hand side is removed first.

Equations

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

partial def Transfer.paramGuardCore (disch : Lean.Syntax) (g : Lean.MVarId) : Lean.Elab.Tactic.TacticM (List Lean.MVarId)

The param_guard recursion on one goal. Returns the goals left open: the guards the discharger disch did not close. Throws the leaf error of paramGuardLeafError on a Related subgoal that no rule closes.

def Transfer.paramGuardMain (disch : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Run paramGuardCore on the main goal and replace it by the open guards.

Equations

• Transfer.paramGuardMain disch = do let g ← Lean.Elab.Tactic.getMainGoal let rest ← Transfer.paramGuardCore disch g Lean.Elab.Tactic.replaceMainGoal rest

def Transfer.tacticParam_guard : Lean.ParserDescr

param_guard descends through the registered total and guarded squares (RelatedBinOpOn, RelatedUnOpOn, RelatedRelOn), discharges each guard by transfer_guard_disch, and leaves the guards it does not close as goals.

Equations

• Transfer.tacticParam_guard = Lean.ParserDescr.node `Transfer.tacticParam_guard 1024 (Lean.ParserDescr.nonReservedSymbol "param_guard" false)

def Transfer.«tacticParam_guard(Disch:=_)» : Lean.ParserDescr

param_guard (disch := tac) is param_guard with the guard discharger tac.

Equations

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