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)⦄) :