structure Lean.Elab.Tactic.VCGen.LatticeOp : Type

How to decompose a lattice operator head … s⃗ on the RHS of an entailment: the distribution and unfolding rewrites that saturate it, and the terminal ⊑-introduction terminals that close the reduced form. head keys the split in the latticeOps table.

• head : Name

  Head constant of the operator this split decomposes. Keys the latticeOps table.

• numConst : Nat

  The number of leading arguments held constant during rule construction: the operator's carrier type and its typeclass instances. The operands and excess state arguments after them become the rule's schematic parameters. 2 for a connective over a CompleteLattice carrier; 0 for a monomorphic operator.

• rewrites : Array Name

  Distribution and unfolding equalities that saturate the operator applied to state arguments.

• terminal? : Option Name

  The operator's terminal ⊑-introduction rule, or none when it saturates to another operator's terminal.

• applies? : Expr → Bool

  Whether the split applies to this RHS. Ops without a terminal decline shapes their rewrites cannot reduce.

Lattice split rules

Backward rules that decompose a lattice operator on the RHS of an entailment pre ⊑ op … s⃗. The operator is saturated with distribution and unfolding rewrites, a terminal ⊑-introduction rule fires on the reduced form, and any state arguments the terminal leaves over-applied are point-framed onto the precondition.

The built-in splits cover the lattice connectives ⊓/⇨/⌜·⌝/⊤/iInf and the magic-wand residual upperAdjoint.

def Lean.Elab.Tactic.VCGen.LatticeOp.meet : LatticeOp

The lattice meet ⊓: distributes via meet_apply, closes with le_meet.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.meet = { head := `Lean.Order.meet, rewrites := #[`Lean.Order.meet_apply], terminal? := some `Lean.Order.le_meet }

def Lean.Elab.Tactic.VCGen.LatticeOp.himp : LatticeOp

Heyting implication ⇨: distributes via himp_apply, closes with le_himp.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.himp = { head := `Lean.Order.himp, rewrites := #[`Lean.Order.himp_apply], terminal? := some `Lean.Order.le_himp }

def Lean.Elab.Tactic.VCGen.LatticeOp.ofProp : LatticeOp

The pure assertion ⌜·⌝: distributes via ofProp_apply, closes with the ⊤-fixed top_le_ofProp.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.ofProp = { head := `Lean.Order.CompleteLattice.ofProp, rewrites := #[`Lean.Order.CompleteLattice.ofProp_apply], terminal? := some `Lean.Order.top_le_ofProp }

def Lean.Elab.Tactic.VCGen.LatticeOp.top : LatticeOp

The lattice top ⊤: distributes via top_apply, closes with le_top.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.top = { head := `Lean.Order.top, rewrites := #[`Lean.Order.top_apply], terminal? := some `Lean.Order.le_top }

def Lean.Elab.Tactic.VCGen.LatticeOp.upperAdjoint : LatticeOp

The magic-wand residual upperAdjoint f b: point-framed, closes with le_upperAdjoint.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.upperAdjoint = { head := `Lean.Order.PreservesSup.upperAdjoint, terminal? := some `Lean.Order.PreservesSup.le_upperAdjoint }

def Lean.Elab.Tactic.VCGen.LatticeOp.iInf : LatticeOp

Indexed infimum iInf/⨅: distributes via iInf_apply, closes with le_iInf.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.iInf = { head := `Lean.Order.iInf, numConst := 3, rewrites := #[`Lean.Order.iInf_apply], terminal? := some `Lean.Order.le_iInf }

def Lean.Elab.Tactic.VCGen.LatticeOp.fst : LatticeOp

The projection (⊥/⊤ : _ × _).fst of an exception-postcondition tuple: reduces to the bare ⊥/⊤ via Prod.fst_bot/Prod.fst_top and the pointwise bot_apply/top_apply. numConst := 3 holds the tuple operand concrete, since which rewrite fires depends on it; only the excess state arguments go schematic. No terminal: the ⊥ residual becomes the subgoal, the ⊤ residual closes with le_top. applies? declines every other operand, whose projection the rewrites cannot reduce.

Equations

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

def Lean.Elab.Tactic.VCGen.LatticeOp.snd : LatticeOp

The projection (⊥/⊤ : _ × _).fst of an exception-postcondition tuple: reduces to the bare ⊥/⊤ via Prod.fst_bot/Prod.fst_top and the pointwise bot_apply/top_apply. numConst := 3 holds the tuple operand concrete, since which rewrite fires depends on it; only the excess state arguments go schematic. No terminal: the ⊥ residual becomes the subgoal, the ⊤ residual closes with le_top. applies? declines every other operand, whose projection the rewrites cannot reduce.

Equations

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

def Lean.Elab.Tactic.VCGen.builtinLatticeOps : Array LatticeOp

The built-in connective splits, whose rewrites and terminals seed every saturation.

Equations

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

def Lean.Elab.Tactic.VCGen.latticeOps : Std.HashMap Name LatticeOp

Lattice splits of the built-in connectives, keyed by operator head. splitLatticeOp? looks a head up here.

Equations

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

def Lean.Elab.Tactic.VCGen.mkLatticeOpRule (rhs : Expr) (op : LatticeOp) : Meta.Sym.SymM Meta.Sym.BackwardRule

Build a reusable backward rule decomposing pre ⊑ op … s⃗ for a lattice operator. The operator's value arguments are made schematic; rewrites saturate the operator through its distribution and unfolding equalities, the terminal keyed by the reduced head fires, and any state arguments left over-applied by the terminal are point-framed onto the precondition. When the reduced head has no registered terminal, the saturated pre ⊑ reduced is handed back as the sole subgoal. Throws when the operator neither reduces nor has a terminal, since its rule would be the identity; the operator's applies? filter keeps such shapes away from rule construction.

For ⊓, produces ∀ a b s⃗ pre, pre ⊑ a s⃗ → pre ⊑ b s⃗ → pre ⊑ (a ⊓ b) s⃗. For the opaque residual upperAdjoint f b, produces ∀ f b s⃗ pre, f (fun u⃗ => ⌜u⃗ = s⃗⌝ ⊓ pre) ⊑ b → pre ⊑ upperAdjoint f b s⃗.

Equations

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