Hoare triple specifications for for loops over Std.Sat.CNF.Clause, enabling mvcgen to
generate verification conditions for them.
theorem
Std.Do.Spec.forIn'_cnfClause
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Sat.CNF.Clause α}
{init : β}
{f : (a : Sat.Literal α) → a ∈ xs → β → m (ForInStep β)}
(inv : Invariant xs.literals β ps)
(step :
∀ (pref : List (Sat.Literal α)) (cur : Sat.Literal α) (suff : List (Sat.Literal α))
(h : xs.literals = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur ⋯ b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.literals, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
:
theorem
Std.Do.Spec.forIn_cnfClause
{α : Type u₁}
{β : Type (max u₁ u₂)}
{m : Type (max u₁ u₂) → Type v}
{ps : PostShape}
[Monad m]
[WPMonad m ps]
{xs : Sat.CNF.Clause α}
{init : β}
{f : Sat.Literal α → β → m (ForInStep β)}
(inv : Invariant xs.literals β ps)
(step :
∀ (pref : List (Sat.Literal α)) (cur : Sat.Literal α) (suff : List (Sat.Literal α))
(h : xs.literals = pref ++ cur :: suff) (b : β),
⦃inv.fst ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄ f cur b ⦃(fun (r : ForInStep β) =>
match r with
| ForInStep.yield b' => inv.fst ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
| ForInStep.done b' => inv.fst ({ «prefix» := xs.literals, suffix := [], property := ⋯ }, b'), inv.snd)⦄)
: