forIn loop-invariant gadgets

forInPureWithInvariant and forInPureWithInvariant' annotate a forIn/forIn' loop with its invariant so that vcgen reads the invariant from the program. Their @[spec] specifications restate Spec.forIn_list/Spec.forIn'_list for every container with a PureForIn instance.

forInLoopWithInvariant, forInLoopWithVariant and forInLoopWithInvariantAndVariant do the same for a repeat loop, one per set of annotations the loop states. Each restates Spec.forIn_loop, leaving what the loop does not state to vcgen to infer.

Gadgets

@[inline]

def Std.WP.Gadget.forInPureWithInvariant {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred : Type (max u₁ u₂)} {ρ : Type w} [ForIn m ρ α] (xs : ρ) (init : β) (f : α → β → m (ForInStep β)) (inv : Invariant α β Pred) : m β

A forIn loop annotated with its loop invariant, which vcgen reads from the inv argument. It is definitionally forIn xs init f, so the annotation is erased at runtime. The invariant ranges over the elements consumed so far, the elements remaining, and the loop state.

Equations

• Std.WP.Gadget.forInPureWithInvariant xs init f inv = forIn xs init f

@[inline]

def Std.WP.Gadget.forInPureWithInvariant' {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred : Type (max u₁ u₂)} {ρ : Type w} {d : Membership α ρ} [ForIn' m ρ α d] (xs : ρ) (init : β) (f : (a : α) → a ∈ xs → β → m (ForInStep β)) (inv : Invariant α β Pred) : m β

A membership-aware forIn' loop annotated with its loop invariant, which vcgen reads from the inv argument. It is definitionally forIn' xs init f, so the annotation is erased at runtime. The invariant ranges over the elements consumed so far, the elements remaining, and the loop state.

Equations

• Std.WP.Gadget.forInPureWithInvariant' xs init f inv = forIn' xs init f

Specifications

theorem Std.WP.Spec.forInPure {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type w} [ForIn m ρ α] [ForIn Id ρ α] [Internal.PureForIn m ρ α] {xs : ρ} {init : β} {f : α → β → m (ForInStep β)} (inv : Invariant α β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α), ForIn.toList xs = pref ++ cur :: suff → ∀ (b : β), ⦃ binderNameHint pref inv (binderNameHint suff (inv pref) (binderNameHint cur f (binderNameHint b (inv pref (cur :: suff)) (inv pref (cur :: suff) b)))) ⦄ f cur b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pref ++ [cur]) suff b' | ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄) : ⦃ inv [] (ForIn.toList xs) init ⦄ Gadget.forInPureWithInvariant xs init f inv ⦃ fun (b : β) => binderNameHint b (inv (ForIn.toList xs) []) (inv (ForIn.toList xs) [] b); epost ⦄

theorem Std.WP.Spec.forInPure' {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [Monad m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {ρ : Type w} {d : Membership α ρ} [ForIn' m ρ α d] [ForIn Id ρ α] [Internal.LawfulMemForInId ρ α] [Internal.PureForIn' m ρ α] {xs : ρ} {init : β} {f : (a : α) → a ∈ xs → β → m (ForInStep β)} (inv : Invariant α β Pred) {epost : EPred} (step : ∀ (pref : List α) (cur : α) (suff : List α) (h : ForIn.toList xs = pref ++ cur :: suff) (b : β), ⦃ binderNameHint pref inv (binderNameHint suff (inv pref) (binderNameHint cur f (binderNameHint b (inv pref (cur :: suff)) (inv pref (cur :: suff) b)))) ⦄ f cur ⋯ b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => inv (pref ++ [cur]) suff b' | ForInStep.done b' => inv (ForIn.toList xs) [] b'; epost ⦄) : ⦃ inv [] (ForIn.toList xs) init ⦄ Gadget.forInPureWithInvariant' xs init f inv ⦃ fun (b : β) => binderNameHint b (inv (ForIn.toList xs) []) (inv (ForIn.toList xs) [] b); epost ⦄

@[inline]

def Std.WP.Gadget.forInLoopWithInvariant {β : Type u} {m : Type u → Type v} {Pred : Type uₚ} [Monad m] (l : Lean.Loop) (init : β) (f : Unit → β → m (ForInStep β)) (inv : WhileInvariant β Pred) : m β

A repeat loop annotated with the loop invariant that vcgen reads from the inv argument. It is definitionally forIn l init f, so the annotation is erased at runtime. The invariant takes the loop's exit flag, false while the loop iterates and true once it is done.

Equations

• Std.WP.Gadget.forInLoopWithInvariant l init f inv = forIn l init f

@[inline]

def Std.WP.Gadget.forInLoopWithVariant {β : Type u} {m : Type u → Type v} {Fun : Type} [Monad m] (l : Lean.Loop) (init : β) (f : Unit → β → m (ForInStep β)) (var : β → Fun) : m β

A repeat loop annotated with the termination measure that vcgen reads from the var argument. It is definitionally forIn l init f, so the annotation is erased at runtime. The measure is the function a Variant is built from, so that the assertion language it evaluates in is the one the specification is applied at.

Equations

• Std.WP.Gadget.forInLoopWithVariant l init f var = forIn l init f

@[inline]

def Std.WP.Gadget.forInLoopWithInvariantAndVariant {β : Type u} {m : Type u → Type v} {Pred : Type uₚ} {Fun : Type} [Monad m] (l : Lean.Loop) (init : β) (f : Unit → β → m (ForInStep β)) (inv : WhileInvariant β Pred) (var : β → Fun) : m β

A repeat loop annotated with the loop invariant and the termination measure that vcgen reads from the inv and var arguments. It is definitionally forIn l init f, so the annotations are erased at runtime. The invariant takes the loop's exit flag, false while the loop iterates and true once it is done. The measure is the function a Variant is built from, so that the assertion language it evaluates in is the one the specification is applied at.

Equations

• Std.WP.Gadget.forInLoopWithInvariantAndVariant l init f inv var = forIn l init f

theorem Std.WP.Spec.forInLoop_invariant_variant {β : Type u} {m : Type u → Type v} {Pred : Type uₚ} {EPred : Type uₑ} [Monad m] [Lean.Order.MonadTail m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {Fun : Type} {γ : Type uγ'} {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)} [Assertion.NondetFun Pred Fun γ] [WellFoundedRelation γ] [∀ (P : Pred), Lean.Order.PreservesSup (Lean.Order.meet P)] (measure : β → Fun) (inv : Bool → β → Pred) (einv : EPred) (step : ∀ (b : β) (mb : γ), ⦃ binderNameHint b (inv false) (Lean.Order.meet ((Variant.ofMeasure measure).EvalsTo b mb) (inv false b)) ⦄ f () b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => Lean.Order.meet ((Variant.ofMeasure measure).EvalsBelow b' mb) (inv false b') | ForInStep.done b' => inv true b'; einv ⦄) : ⦃ inv false init ⦄ Gadget.forInLoopWithInvariantAndVariant l init f (WhileInvariant.mk inv) measure ⦃ fun (b : β) => binderNameHint b (inv true) (inv true b); einv ⦄

theorem Std.WP.Spec.forInLoop_invariant {β : Type u} {m : Type u → Type v} {Pred : Type uₚ} {EPred : Type uₑ} [Monad m] [Lean.Order.MonadTail m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)} [∀ (P : Pred), Lean.Order.PreservesSup (Lean.Order.meet P)] (measure : Variant β Pred) (inv : Bool → β → Pred) (einv : EPred) (step : ∀ (b : β) (mb : measure.γ), ⦃ binderNameHint b (inv false) (Lean.Order.meet (measure.EvalsTo b mb) (inv false b)) ⦄ f () b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => Lean.Order.meet (measure.EvalsBelow b' mb) (inv false b') | ForInStep.done b' => inv true b'; einv ⦄) : ⦃ inv false init ⦄ Gadget.forInLoopWithInvariant l init f (WhileInvariant.mk inv) ⦃ fun (b : β) => binderNameHint b (inv true) (inv true b); einv ⦄

theorem Std.WP.Spec.forInLoop_variant {β : Type u} {m : Type u → Type v} {Pred : Type uₚ} {EPred : Type uₑ} [Monad m] [Lean.Order.MonadTail m] [Assertion Pred] [Assertion EPred] [WPMonad m Pred EPred] {Fun : Type} {γ : Type uγ'} {l : Lean.Loop} {init : β} {f : Unit → β → m (ForInStep β)} [Assertion.NondetFun Pred Fun γ] [WellFoundedRelation γ] [∀ (P : Pred), Lean.Order.PreservesSup (Lean.Order.meet P)] (measure : β → Fun) (inv : WhileInvariant β Pred) (einv : EPred) (step : ∀ (b : β) (mb : γ), ⦃ binderNameHint b (inv false) (Lean.Order.meet ((Variant.ofMeasure measure).EvalsTo b mb) (inv false b)) ⦄ f () b ⦃ fun (r : ForInStep β) => match r with | ForInStep.yield b' => Lean.Order.meet ((Variant.ofMeasure measure).EvalsBelow b' mb) (inv false b') | ForInStep.done b' => inv true b'; einv ⦄) : ⦃ inv false init ⦄ Gadget.forInLoopWithVariant l init f measure ⦃ fun (b : β) => binderNameHint b (inv true) (inv true b); einv ⦄