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 a frame for the state arguments the terminal leaves over-applied moves them onto the precondition.

The built-in splits are the LatticeOp values in builtinLatticeOps.

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_of_meet_le_left.

Equations

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

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

The pure assertion ⌜·⌝: distributes via ofProp_apply, closes with the ⊤-fixed CompleteLattice.top_le_ofProp. It decomposes pre ⊑ ⌜p⌝ only when pre is ⊤: the subgoal p of any other pre would drop pre, and the terminal fails to apply.

Equations

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

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.and : LatticeOp

The conjunction ∧ on the Prop lattice: closes with le_and.

Equations

• Lean.Elab.Tactic.VCGen.LatticeOp.and = { head := `And, numConst := 0, terminal? := some `Lean.Order.le_and }

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

The existential ∃ h : a, b h over a proposition a: closes with le_exists_prop.

Equations

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

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

The magic-wand residual upperAdjoint f b: framed for its excess state arguments, closes with le_upperAdjoint.

Equations

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

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.iSup : LatticeOp

Indexed supremum iSup/⨆ over a proposition: distributes via iSup_apply, closes with le_iSup_prop.

Equations

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

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

Equations

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

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

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 move onto the precondition through a frame for them. 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.