Assertion

The Assertion class and lattice capabilities such as total nondeterministic functions.

class Std.Internal.Do.Assertion (α : Type w) extends Lean.Order.CompleteLattice α : Type w

An assertion type is equipped with a CompleteLattice structure, used as the carrier for pre- and postconditions.

• rel : α → α → Prop
• rel_refl {x : α} : rel x x
• rel_trans {x y z : α} : rel x y → rel y z → rel x z
• rel_antisymm {x y : α} : rel x y → rel y x → x = y
• has_sup (c : α → Prop) : Exists (is_sup c)

Total nondeterministic functions

CompleteLattice can embed propositions (⌜_⌝) but not values of an arbitrary type α. NondetFun Pred Fun α equips an assertion lattice Pred with a notion of total nondeterministic functions Fun into α. For example, at Pred = Nat → Prop the instances are set up such that Fun := Nat → α, a function reading the Nat state. The assertion EvalsTo f a states that f evaluates to the value a; in the example it is fun s => ⌜f s = a⌝. The law total states that f evaluates to some value: (⨆ a, EvalsTo f a) = ⊤. The value type α is the outParam because instances are synthesized while only the function f is at hand: resolution knows Pred and Fun and computes α, whose values first occur in the assertions the instance builds.

class Std.Internal.Do.Assertion.NondetFun (Pred : Type u) (Fun : Type v) (α : outParam (Type w)) [Assertion Pred] : Type (max (max u v) w)

Pred interprets values of Fun as total nondeterministic functions into α. The value type α is an outParam computed from Pred and Fun.

• EvalsTo : Fun → α → Pred

  Relates a nondeterministic function to a value inside the assertion lattice.

• total (f : Fun) : (Lean.Order.iSup fun (a : α) => EvalsTo f a) = Lean.Order.top

  Every function hits some value.

@[instance_reducible, instance 100]

noncomputable instance Std.Internal.Do.Assertion.instNondetFun {Pred : Type u} {α : Type v} [Assertion Pred] : NondetFun Pred α α

Pure (state-independent) nondeterministic functions into α are just values of α. Low priority so that the σ-indexed instance is preferred when both apply.

Equations

• Std.Internal.Do.Assertion.instNondetFun = { EvalsTo := fun (f a : α) => Lean.Order.CompleteLattice.ofProp (f = a), total := ⋯ }

@[instance_reducible]

instance Std.Internal.Do.Assertion.instNondetFunForall {σ : Type s} {Pred : Type u} {Fun : Type v} {α : Type w} [Assertion Pred] [inst : NondetFun Pred Fun α] : NondetFun (σ → Pred) (σ → Fun) α

State-dependent nondeterministic functions: a function for σ → Pred is a σ-indexed function for Pred.

Equations

• Std.Internal.Do.Assertion.instNondetFunForall = { EvalsTo := fun (f : σ → Fun) (a : α) (s : σ) => Std.Internal.Do.Assertion.NondetFun.EvalsTo (f s) a, total := ⋯ }

@[simp]

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_pure {Pred : Type u} {α : Type v} [Assertion Pred] (f a : α) : EvalsTo f a = Lean.Order.CompleteLattice.ofProp (f = a)

@[simp]

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply {σ : Type s} {Pred : Type u} {Fun : Type v} {α : Type w} [Assertion Pred] [NondetFun Pred Fun α] (f : σ → Fun) (a : α) (s : σ) : EvalsTo f a s = EvalsTo (f s) a

Pointwise characterization of EvalsTo on a function lattice.

Prop-valued, fixed-arity specializations of NondetFun.evalsTo_apply: the graph of a state-dependent function at a state-indexed Prop lattice, applied to its states, is an equation. Fixing the carrier to Prop (a ground instance) leaves every parameter recoverable from the trigger, so these are usable @[grind =] lemmas where the general evalsTo_apply is not.

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply_1 {σ₁ α : Type} (f : σ₁ → α) (a : α) (s₁ : σ₁) : EvalsTo f a s₁ = (f s₁ = a)

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply_2 {σ₁ σ₂ α : Type} (f : σ₁ → σ₂ → α) (a : α) (s₁ : σ₁) (s₂ : σ₂) : EvalsTo f a s₁ s₂ = (f s₁ s₂ = a)

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply_3 {σ₁ σ₂ σ₃ α : Type} (f : σ₁ → σ₂ → σ₃ → α) (a : α) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) : EvalsTo f a s₁ s₂ s₃ = (f s₁ s₂ s₃ = a)

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply_4 {σ₁ σ₂ σ₃ σ₄ α : Type} (f : σ₁ → σ₂ → σ₃ → σ₄ → α) (a : α) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) : EvalsTo f a s₁ s₂ s₃ s₄ = (f s₁ s₂ s₃ s₄ = a)

theorem Std.Internal.Do.Assertion.NondetFun.evalsTo_apply_5 {σ₁ σ₂ σ₃ σ₄ σ₅ α : Type} (f : σ₁ → σ₂ → σ₃ → σ₄ → σ₅ → α) (a : α) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃) (s₄ : σ₄) (s₅ : σ₅) : EvalsTo f a s₁ s₂ s₃ s₄ s₅ = (f s₁ s₂ s₃ s₄ s₅ = a)

theorem Std.Internal.Do.Assertion.NondetFun.le_of_total_le {Pred : Type u} {Fun : Type v} {α : Type w} [Assertion Pred] [inst : NondetFun Pred Fun α] (f : Fun) {P Q : Pred} [Lean.Order.PreservesSup (Lean.Order.meet P)] (h : Lean.Order.PartialOrder.rel (Lean.Order.iSup fun (a : α) => Lean.Order.meet (EvalsTo f a) P) Q) : Lean.Order.PartialOrder.rel P Q

Eliminate the covering join of EvalsTo from the left of an entailment.