Construction of BackwardRules from SpecTheoremNews and split info. Pure SymM — no knowledge of VCGenM. The VCGenM cache wrappers live in VCGen.RuleCache.

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleFromSpec (specThm : SpecAttr.SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : Meta.Sym.SymM Meta.Sym.BackwardRule

Create a backward rule for the SpecTheoremNew that was looked up in the database. In order for the backward rule to apply, we need to instantiate both m and ps with the ones given by the use site, and perhaps emit verification conditions for spec lemmas that would not apply everywhere.

General idea

Consider the spec theorem Spec.bind:

Spec.bind : ∀ {m : Type u → Type v} {ps : PostShape} [inst : Monad m] [inst_1 : WPMonad m ps]
  {α β : Type u} {x : m α} {f : α → m β} {Q : PostCond β ps},
  ⦃wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.snd)⦄ (x >>= f) ⦃Q⦄

This theorem is already in "WP-form", so its postcondition Q is schematic (i.e., a ∀-bound var). However, its precondition wp⟦x⟧ ... is not. Hence we must emit a VC for the precondition:

prf : ∀ {m : Type u → Type v} {ps : PostShape} [inst : Monad m] [inst_1 : WPMonad m ps]
  {α β : Type u} {x : m α} {f : α → m β} {Q : PostCond β ps}
  (P : Assertion ps) (hpre : P ⊢ₛ wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.snd)),
  P ⊢ₛ wp⟦x >>= f⟧ Q

(Note that P ⊢ₛ wp⟦x >>= f⟧ Q is the definition of ⦃P⦄ (x >>= f) ⦃Q⦄.) Where prf is constructed by doing SPred.entails.trans hpre spec under the forall telescope. The conclusion of this rule applies to any situation where bind is the top-level symbol in the program.

Postcondition VCs

Similarly, a VC hpost is generated for the postcondition if it isn't schematic. The details here are more complicated because we need to make available the pure facts in P to prove Q' ⊢ₚ Q, so the hpost obligation becomes P ⊢ₛ ⌜Q' ⊢ₚ Q⌝. For example, a hypothetical restrictive spec for pure in Id would be:

myPure.spec (n : Nat) : ⦃fun x => ⌜True⌝⦄ myPure n ⦃⇓ r x => ⌜r = n⌝⦄

This yields the following backward rule:

prf : ∀ (n : Nat) (P : Assertion .pure) (hpre : P ⊢ₛ ⌜True⌝)
  (Q : PostCond Nat .pure) (hpost : P ⊢ₛ ⌜(⇓ r => ⌜r = n⌝) ⊢ₚ Q⌝),
  P ⊢ₛ wp⟦myPure n⟧ Q

The prf term in this (most general) case is

fun n P hpre Q hpost =>
  SPred.pure_elim hpost fun h =>
    SPred.entails.trans (SPred.entails.trans hpre (myPure.spec n))
      (PredTrans.mono (wp (myPure n)) (⇓ r => ⌜r = n⌝) Q h)

Excess state arguments

Furthermore, when there are excess state arguments [s₁, ..., sₙ] involved, we rather need to specialize the backward rule for that:

... : ∀ {m : Type u → Type v} {ps : PostShape} [inst : Monad m] [inst_1 : WPMonad m ps]
  {α β : Type u} {x : m α} {f : α → m β} {Q : PostCond β ps}
  (P : Assertion ...) (hpre : P ⊢ₛ wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.snd) s₁ ... sₙ),
  P ⊢ₛ wp⟦x >>= f⟧ Q s₁ ... sₙ

Caching

It turns out we can cache backward rules for the cache key (specThm, m, excessArgs.size). This is very important for performance and helps getting rid of the overhead imposed by the generality of Std.Do. We do that in the VCGenM wrapper mkBackwardRuleFromSpecCached. Furthermore, in order to avoid re-checking the same proof in the kernel, we generate an auxiliary lemma for the backward rule.

Specialization and unfolding of Std.Do abbreviations and defs

It is unnecessary to use the bind rule in full generality. It is much more efficient to specialize it for the particular monad, postshape and WP instance. In doing so we can also unfold many Std.Do abbreviations, such as Assertion ps and PostCond α ps. We do that by doing unfoldReducible on the forall telescope. The type for StateM Nat and one excess state arg s becomes

prf : ∀ (α : Type) (x : StateT Nat Id α) (β : Type) (f : α → StateT Nat Id β)
        (Q : (β → Nat → ULift Prop) × ExceptConds (PostShape.arg Nat PostShape.pure)) (s : Nat)
        (P : ULift Prop) (hpre : P ⊢ₛ wp⟦x⟧ (fun a => wp⟦f a⟧ Q, Q.snd) s),
        P ⊢ₛ wp⟦x >>= f⟧ Q s

We are still investigating how to get rid of more kernel unfolding overhead, such as for wp and List.rec.

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleFromSimpSpec (specThm : SpecAttr.SpecTheoremNew) (m σs ps instWP : Expr) (excessArgs : Array Expr) : Meta.Sym.SymM Meta.Sym.BackwardRule

Create a backward rule for a simp/equational spec ∀ xs, lhs = rhs.

Instantiates the equation, unifies with the monad m, synthesizes typeclass instances, reduces projections and applies unfoldReducible to the RHS. Then builds a backward rule of the form:

∀ Q s₁ ... sₙ P (h : P ⊢ₛ wp⟦rhs_reduced⟧ Q s₁ ... sₙ), P ⊢ₛ wp⟦lhs⟧ Q s₁ ... sₙ

using Eq.mpr with a congrArg proof.

For example, MonadState.get.eq_1 : get = self.1 with m = StateT σ m' yields a rule that rewrites wp⟦get⟧ to wp⟦MonadStateOf.get⟧ (after instance synthesis + projection reduction + unfoldReducible).

Equations

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

def Lean.Elab.Tactic.Do.Internal.VCGen.mkBackwardRuleForSplit (splitInfo : SplitInfo) (m σs ps instWP : Expr) (excessArgs : Array Expr) : Meta.Sym.SymM Meta.Sym.BackwardRule

Creates a reusable backward rule for splitting ite, dite, or matchers.

Uses SplitInfo.withAbstract to open fvars for the split, then SplitInfo.splitWith to build the splitting proof. Hypothesis types are discovered via rwIfOrMatcher inside the splitter telescope.

Equations

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