Conjunctive preconditions

isConjunctiveInPosts classifies the @[spec] theorems whose precondition specPre Q is conjunctive in the schematic postcondition Q: specPre a ⊓ specPre b ⊑ specPre (a ⊓ b). vcgen applies such a spec directly and skips frame inference. The classification is an optimization: a frameproc can recognize the same situations and decline to frame.

Why no frame is needed

Apply the spec specPre Q ⊑ wp x Q to the goal P ⊑ wp x Q. The direct application emits the single VC (h₁) P ⊑ specPre Q. A framed application with frame F needs (h₂) P ⊑ F and (h₃) P ⊓ F ⊑ specPre (fun _ => F), the spec-level WP.Frames obligation under the guard P. Its conclusion follows from h₁, h₂ and h₃:

P ⊑ specPre Q ⊓ specPre (fun _ => F)    -- h₁, and h₂ with h₃
  ⊑ specPre (fun v => Q v ⊓ F)          -- conjunctivity
  ⊑ wp x (fun v => Q v ⊓ F)             -- the spec

So the direct application carries every admissible F. WP.frames_of_conjunctive is this derivation with specPre := wp x.

Syntactic detection

Every occurrence of Q/E in specPre must lie in a conjunctive context: the body of a λ or ∀ with a Q-free binder type, an application Q a⋯ with Q-free arguments, or a conjunctive argument of a head in conjunctiveArgs?. A context applied to further Q-free arguments stays conjunctive, because (f ⊓ g) a = f a ⊓ g a. For example:

get       ↦  fun s => Q s s
bind      ↦  wp x (fun a => wp (f a) Q E) E
tryCatch  ↦  wp x Q (fun e => wp (h e) Q E, E.snd)

The wp arm assumes that the wp of the sub-program is conjunctive (WPConjunctive).

conjunctiveArgs? is a fixed table. An attribute on lemmas such as ite c a₁ b₁ ⊓ ite c a₂ b₂ ⊑ ite c (a₁ ⊓ a₂) (b₁ ⊓ b₂) could extend it to user-defined heads, reading the varying arguments as conjunctive and the shared ones as Q-free. Such a lemma would have to state conjunctivity jointly in all varying arguments: Or is conjunctive in each argument separately, but not jointly. There is no such attribute because the classification only saves time: a spec with an unknown head goes through frame inference, and the frameproc can decline to frame it, which yields the same VCs. An attribute pays off only once a user-defined head makes frame inference measurably slow.

Premises

A spec with a premise that mentions Q/E is not considered conjunctive, because its direct application does not auto-frame. vcgen applies a spec at the current state s of the goal, and the frame (· = s) for that state argument reaches the conclusion but not the premises. In

(ht : P₁ ⊑ wp t Q) → (he : P₂ ⊑ wp e Q) → (if c then P₁ else P₂) ⊑ wp (ite c t e) Q

all facts about s must be guessed into P₁ and P₂. The premise-free form (if c then wp t Q else wp e Q) ⊑ wp (ite c t e) Q keeps both branches at s. A premise Q = Q opts a spec out of the direct application.

def Lean.Elab.Tactic.VCGen.SpecAttr.isConjunctiveInPosts (concl : Expr) (binders : Array Expr) : MetaM Bool

Whether the precondition of the spec ∀ binders, concl is conjunctive in its schematic postconditions.

Equations

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