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.

A frame operator contributes its own rewrites and terminals through its @[frameproc]; the built-in seeds cover the lattice connectives ⊓/⇨/⌜·⌝/⊤ and the magic-wand residual upperAdjoint.

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

def Lean.Elab.Tactic.Do.Internal.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.Do.Internal.VCGen.mkLatticeOpTable (frameSplits : Std.HashMap Name LatticeOp) : Std.HashMap Name LatticeOp

The lattice-split table keyed by operator head, merging the built-in connectives with the registered frame operators' splits.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkLatticeOpRule (rhs : Expr) (op : LatticeOp) : MetaM 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.

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.