17.2. 谓词变换器概述🔗

谓词变换器语义将程序解释为从谓词到谓词的函数，而不是从值到值的函数。 后置条件是在程序运行后成立的断言；前置条件则是为了保证后置条件成立而必须在程序运行前成立的断言。

mvcgen 使用的谓词变换器语义将后置条件变换为程序能够保证该后置条件成立时的最弱前置条件。若在所有状态下 P' 都足以证明 P，但 P 不足以证明 P'，则断言 P 弱于 P'。逻辑等价的断言视为相等。

这里的谓词是有状态的：它们可以提及程序的当前状态。此外，后置条件还可以把程序的返回值及其抛出的任何异常与最终状态关联起来。 SPred 是一种谓词类型，以单子状态为参数；该状态表示为组成状态的各字段类型所构成的列表。 SPred 定义了通常的逻辑联结词和量词。每个可与 mvcgen 配合使用的单子，都由 WP 实例为其指定状态类型；Assertion 是该单子对应的断言类型，用于前置条件。 Assertion 是 SPred 的包装：SPred 以状态类型列表为参数，而 Assertion 以信息更丰富的类型为参数，并将其转换为供 SPred 使用的状态类型列表。 PostCond 将关于返回值的 Assertion 与关于潜在异常的断言配对；可用的异常同样由该单子的 WP 实例指定。

17.2.1. 有状态谓词🔗

单子程序的谓词变换器语义建立在一种允许命题提及程序状态的逻辑之上。这里的“状态”不仅指可变状态，也包括通过 ReaderT 等方式提供的只读值。不同单子提供不同的状态类型，但每个具体状态始终都有类型。给定一个状态类型列表，SPred 就是这些状态上的谓词类型。

SPred 本身并不与单子验证框架绑定。相关的 Assertion 根据单子 WP 实例的 PostShape 输出参数所表示的状态，为该单子计算合适的 SPred。

定义

Std.Do.SPred.{u} (σs : List (Type u)) : Type u
Std.Do.SPred.{u} (σs : List (Type u)) :
  Type u

状态上的谓词，其中每个状态由一个组成状态类型列表定义。

示例：

SPred [Nat, Bool] = (Nat → Bool → ULift Prop)

不提及状态的普通命题可通过添加一个平凡的全称量化而用作有状态谓词。其语法写作 ⌜P⌝，这是 SPred.pure 的语法糖。

语法SPred 记法

term ::= ...
    | Embedding of pure Lean values into `SVal`. An alias for `SPred.pure`. ⌜term⌝

将纯 Lean 命题嵌入 SPred；这是 SPred.pure 的语法糖。

定义

Std.Do.SPred.pure.{u} {σs : List (Type u)} (P : Prop) : SPred σs
Std.Do.SPred.pure.{u} {σs : List (Type u)}
  (P : Prop) : SPred σs

将纯命题 P : Prop 嵌入 SPred。建议优先使用记法 ⌜P⌝。

有状态谓词示例

谓词 ItIsSecret 表示一个 String 类型的状态等于 "secret"：

def ItIsSecret : SPred [String] := fun s => ⌜s = "secret"⌝

在线查看 ↪

17.2.1.1. 蕴涵🔗

有状态谓词之间以蕴涵关系联系。有状态谓词的蕴涵定义为全称量化的蕴含：若 P 和 Q 是状态 \sigma 上的谓词，则当 ∀ s : \sigma, P(s) → Q(s) 时，称 P 蕴涵 Q（写作 P \vdash_s Q）。

定义

Std.Do.SPred.entails.{u} {σs : List (Type u)} (P Q : SPred σs) : Prop
Std.Do.SPred.entails.{u}
  {σs : List (Type u)} (P Q : SPred σs) :
  Prop

SPred 中的蕴涵。

如果在 P 为真的每个状态中 Q 也为真，就称谓词 P 蕴涵谓词 Q。与蕴含（SPred.imp）不同，蕴涵本身不是 SPred，而是普通命题。

定义

Std.Do.SPred.bientails.{u} {σs : List (Type u)} (P Q : SPred σs) : Prop
Std.Do.SPred.bientails.{u}
  {σs : List (Type u)} (P Q : SPred σs) :
  Prop

SPred 中的逻辑等价。

逻辑等价的谓词相等。可使用 SPred.bientails.to_eq 将双向蕴涵转换为等式。

语法SPred 蕴涵记法

term ::= ...
    | Entailment in `SPred`; sugar for `SPred.entails`. term ⊢ₛ term

SPred 中的蕴涵；SPred.entails 的语法糖。

term ::= ...
    | Tautology in `SPred`; sugar for `SPred.entails ⌜True⌝`. ⊢ₛ term

SPred 中的重言式；SPred.entails ⌜True⌝ 的语法糖。

term ::= ...
    | Bi-entailment in `SPred`; sugar for `SPred.bientails`. term ⊣⊢ₛ term

SPred 中的双向蕴涵；SPred.bientails 的语法糖。

有状态谓词逻辑包含蕴含联结词。蕴涵关系与蕴含联结词的区别在于：蕴涵关系是 Lean 逻辑中的命题，而蕴含联结词位于有状态逻辑内部。给定状态 σ 上的有状态谓词 P 和 Q，P ⊢ₛ Q 是 Prop，而 spred(P → Q) 是 SPred σ。

17.2.1.2. 记法🔗

有状态谓词的语法与普通 Lean 项的语法有所重叠。特别是，有状态谓词使用逻辑联结词和量词的通常语法。在前置条件和后置条件等明显需要有状态谓词的上下文中，相关语法会自动启用；其他上下文必须使用 Std.Do.«termSpred(_)» : termAn embedding of the special syntax for `SPred` into ordinary terms that provides alternative interpretations of logical connectives and quantifiers. Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.spred 显式启用该语法。使用 Std.Do.«termTerm(_)» : termEscapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers and connectives.term 运算符可恢复这些运算符的通常含义。

语法谓词项

Std.Do.«termSpred(_)» : termAn embedding of the special syntax for `SPred` into ordinary terms that provides alternative interpretations of logical connectives and quantifiers. Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.spred 表示应将逻辑联结词和量词理解为有状态谓词中的对应构造，而 Std.Do.«termTerm(_)» : termEscapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers and connectives.term 表示它们应取通常含义。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(term)

term ::= ...
    | Escapes from a surrounding `spred(...)` term, returning to the usual interpretations of quantifiers
and connectives.
term(term)

17.2.1.3. 联结词与量词🔗

语法谓词联结词

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`And a b`, or `a ∧ b`, is the conjunction of propositions. It can be
constructed and destructed like a pair: if `ha : a` and `hb : b` then
`⟨ha, hb⟩ : a ∧ b`, and if `h : a ∧ b` then `h.left : a` and `h.right : b`.


Conventions for notations in identifiers:

 * The recommended spelling of `∧` in identifiers is `and`.term ∧ term)

SPred.and 的语法糖。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`Or a b`, or `a ∨ b`, is the disjunction of propositions. There are two
constructors for `Or`, called `Or.inl : a → a ∨ b` and `Or.inr : b → a ∨ b`,
and you can use `match` or `cases` to destruct an `Or` assumption into the
two cases.


Conventions for notations in identifiers:

 * The recommended spelling of `∨` in identifiers is `or`.term ∨ term)

SPred.or 的语法糖。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(`Not p`, or `¬p`, is the negation of `p`. It is defined to be `p → False`,
so if your goal is `¬p` you can use `intro h` to turn the goal into
`h : p ⊢ False`, and if you have `hn : ¬p` and `h : p` then `hn h : False`
and `(hn h).elim` will prove anything.
For more information: [Propositional Logic](https://lean-lang.org/theorem_proving_in_lean4/propositions_and_proofs.html#propositional-logic)


Conventions for notations in identifiers:

 * The recommended spelling of `¬` in identifiers is `not`.¬ term)

SPred.not 的语法糖。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(term → term)

SPred.imp 的语法糖。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(If and only if, or logical bi-implication. `a ↔ b` means that `a` implies `b` and vice versa.
By `propext`, this implies that `a` and `b` are equal and hence any expression involving `a`
is equivalent to the corresponding expression with `b` instead.


Conventions for notations in identifiers:

 * The recommended spelling of `↔` in identifiers is `iff`.term ↔ term)

SPred.iff 的语法糖。

定义

Std.Do.SPred.and.{u} {σs : List (Type u)} (P Q : SPred σs) : SPred σs
Std.Do.SPred.and.{u} {σs : List (Type u)}
  (P Q : SPred σs) : SPred σs

SPred 中的合取：同时满足 P 和 Q 的状态满足 spred(P ∧ Q)。

定义

Std.Do.SPred.conjunction.{u} {σs : List (Type u)}
  (env : List (SPred σs)) : SPred σs
Std.Do.SPred.conjunction.{u}
  {σs : List (Type u)}
  (env : List (SPred σs)) : SPred σs

有状态谓词列表的合取。当且仅当一个状态满足 env 中的所有谓词时，它满足 conjunction env。

定义

Std.Do.SPred.or.{u} {σs : List (Type u)} (P Q : SPred σs) : SPred σs
Std.Do.SPred.or.{u} {σs : List (Type u)}
  (P Q : SPred σs) : SPred σs

SPred 中的析取：满足 P 或 Q 的状态满足 spred(P ∨ Q)。

定义

Std.Do.SPred.not.{u} {σs : List (Type u)} (P : SPred σs) : SPred σs
Std.Do.SPred.not.{u} {σs : List (Type u)}
  (P : SPred σs) : SPred σs

SPred 中的否定：不满足 P 的状态满足 spred(¬ P)。

定义

Std.Do.SPred.imp.{u} {σs : List (Type u)} (P Q : SPred σs) : SPred σs
Std.Do.SPred.imp.{u} {σs : List (Type u)}
  (P Q : SPred σs) : SPred σs

SPred 中的蕴含：只要满足 P 就也满足 Q 的状态满足 spred(P → Q)。

定义

Std.Do.SPred.iff.{u} {σs : List (Type u)} (P Q : SPred σs) : SPred σs
Std.Do.SPred.iff.{u} {σs : List (Type u)}
  (P Q : SPred σs) : SPred σs

SPred 中的双条件：同时满足 P 和 Q，或二者都不满足的状态满足 spred(P ↔ Q)。

语法谓词量词

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ ident, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ ident : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
(ident (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term),  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∀ Explicit binder, like `(x y : A)` or `(x y)`.
Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
(A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ (ident | A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
hole)* : term),  term)

每种全称量化形式都是调用 SPred.forall 的语法糖，所传函数以被量化变量为参数。

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
ident `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
binderIdent* : term),  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_, term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ : term,  term)

term ::= ...
    | An embedding of the special syntax for `SPred` into ordinary terms that provides alternative
interpretations of logical connectives and quantifiers.

Within `spred(...)`, `term(...)` escapes to the ordinary Lean interpretation of this syntax.
spred(∃ (`binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.

The way this works is that holes create fresh metavariables.
The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
This is often known as *unification*.

Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
* In `match` patterns, holes are catch-all patterns.
* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.

Related concept: implicit parameters are automatically filled in with holes during the elaboration process.

See also `?m` syntax (synthetic holes).
_ `binderIdent` matches an `ident` or a `_`. It is used for identifiers in binding
position, where `_` means that the value should be left unnamed and inaccessible.
binderIdent* : term),  term)

每种存在量化形式都是调用 SPred.exists 的语法糖，所传函数以被量化变量为参数。

定义

Std.Do.SPred.forall.{u, v} {α : Sort u} {σs : List (Type v)}
  (P : α → SPred σs) : SPred σs
Std.Do.SPred.forall.{u, v} {α : Sort u}
  {σs : List (Type v)}
  (P : α → SPred σs) : SPred σs

SPred 中的全称量词。

定义

Std.Do.SPred.exists.{u, v} {α : Sort u} {σs : List (Type v)}
  (P : α → SPred σs) : SPred σs
Std.Do.SPred.exists.{u, v} {α : Sort u}
  {σs : List (Type v)}
  (P : α → SPred σs) : SPred σs

SPred 中的存在量词。

17.2.1.4. 有状态值🔗

正如 SPred 表示状态上的谓词，SVal 表示由状态导出的值。

定义

Std.Do.SVal.{u} (σs : List (Type u)) (α : Type u) : Type u
Std.Do.SVal.{u} (σs : List (Type u))
  (α : Type u) : Type u

由柯里化的状态元组索引的值。

示例：

example : SVal [Nat, Bool] String = (Nat → Bool → String) := rfl

定义

Std.Do.SVal.getThe.{u} {σs : List (Type u)} (σ : Type u)
  [SVal.GetTy σ σs] : SVal σs σ
Std.Do.SVal.getThe.{u}
  {σs : List (Type u)} (σ : Type u)
  [SVal.GetTy σ σs] : SVal σs σ

获取 SVal 中类型为 σ 的最上层状态。

定义

Std.Do.SVal.StateTuple.{u} (σs : List (Type u)) : Type u
Std.Do.SVal.StateTuple.{u}
  (σs : List (Type u)) : Type u

捕获一个 SVal 完整状态的元组。

定义

Std.Do.SVal.curry.{u} {α : Type u} {σs : List (Type u)}
  (f : SVal.StateTuple σs → α) : SVal σs α
Std.Do.SVal.curry.{u} {α : Type u}
  {σs : List (Type u)}
  (f : SVal.StateTuple σs → α) : SVal σs α

将接受 StateTuple 的函数柯里化为 SVal。

定义

Std.Do.SVal.uncurry.{u} {α : Type u} {σs : List (Type u)}
  (f : SVal σs α) : SVal.StateTuple σs → α
Std.Do.SVal.uncurry.{u} {α : Type u}
  {σs : List (Type u)} (f : SVal σs α) :
  SVal.StateTuple σs → α

将 SVal 反柯里化为接受 StateTuple 的函数。

17.2.2. 断言🔗

关于单子程序的断言语言以后置条件形状为参数；该形状描述给定单子中计算的输入和输出。前置条件可以提及单子状态的初始值；后置条件可以提及返回值和单子状态的最终值，并且还必须涵盖所有可能抛出的异常。给定单子的后置条件形状决定该单子中的状态和异常。 PostShape.pure 描述断言不能提及任何状态的单子，PostShape.arg 描述一个状态值，PostShape.except 描述一种可能的异常。由于可以不断添加这些构造器，单子变换器的后置条件形状可以用其所变换的底层单子的后置条件形状来定义。在幕后，后置条件形状会被转换为状态类型列表并丢弃异常，从而将 Assertion 转换为适当的 SPred。

归纳类型

Std.Do.PostShape.{u} : Type (u + 1)
Std.Do.PostShape.{u} : Type (u + 1)

用于对单子进行推理的后置条件的“形状”。

后置条件形状是对许多可能的单子效应的抽象，其依据是能够模拟这些效应的纯函数结构。单子的后置条件形状由其 WP 实例给出，并用于确定其 Assertion 和 PostCond。

构造子

Std.Do.PostShape.pure.{u} : PostShape

此单子中的断言和后置条件既不使用状态，也不使用异常。

Std.Do.PostShape.arg.{u} (σ : Type u) :
  PostShape → PostShape

此单子中的断言可以提及类型为 σ 的状态的当前值，后置条件则可以提及该状态的最终值。

Std.Do.PostShape.except.{u} (ε : Type u) :
  PostShape → PostShape

此单子中的后置条件包含关于类型为 ε、由提前终止产生的异常值的断言。

定义

Std.Do.PostShape.args.{u} : PostShape → List (Type u)
Std.Do.PostShape.args.{u} :
  PostShape → List (Type u)

提取 PostShape.arg 构造器下的状态类型列表，并丢弃异常类型。

这些状态类型决定单子中断言的形状。

定义

Std.Do.Assertion.{u} (ps : PostShape) : Type u
Std.Do.Assertion.{u} (ps : PostShape) :
  Type u

关于后置条件形状为 ps 的单子的各个状态字段的断言。

具体而言，它是将 SPred 应用于给定谓词形状中各个 .arg 的缩写，因此所有关于 SPred 的定理都适用。

示例：

example : Assertion (.arg ρ .pure) = (ρ → ULift Prop) := rfl
example : Assertion (.except ε .pure) = ULift Prop := rfl
example : Assertion (.arg σ (.except ε .pure)) = (σ → ULift Prop) := rfl
example : Assertion (.except ε (.arg σ .pure)) = (σ → ULift Prop) := rfl

定义

Std.Do.PostCond.{u} (α : Type u) (ps : PostShape) : Type u
Std.Do.PostCond.{u} (α : Type u)
  (ps : PostShape) : Type u

给定谓词形状的后置条件：正常终止情形有一个 Assertion，谓词形状中的每个 .except 层也各有一个 Assertion。

variable (α σ ε : Type)
example : PostCond α (.arg σ .pure) = ((α → σ → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε .pure) = ((α → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.arg σ (.except ε .pure)) = ((α → σ → ULift Prop) × (ε → ULift Prop) × PUnit) := rfl
example : PostCond α (.except ε (.arg σ .pure)) = ((α → σ → ULift Prop) × (ε → σ → ULift Prop) × PUnit) := rfl

语法后置条件

term ::= ...
    | A postcondition expressing total correctness.
That is, it expresses that the asserted computation finishes without throwing an exception
*and* the result satisfies the given predicate `p`.
⇓ term* => term

这是嵌套积构造器序列的语法糖，并以 () 结尾；其中第一个元素是关于非异常返回值的断言，其余元素是关于后置条件中各异常情形的断言。

定义

Std.Do.ExceptConds.{u} : PostShape → Type u
Std.Do.ExceptConds.{u} :
  PostShape → Type u

关于后置条件形状中声明的每种潜在异常的断言。

示例：

example : ExceptConds (.pure) = Unit := rfl
example : ExceptConds (.except ε .pure) = ((ε → ULift Prop) × Unit) := rfl
example : ExceptConds (.arg σ (.except ε .pure)) = ((ε → ULift Prop) × Unit) := rfl
example : ExceptConds (.except ε (.arg σ .pure)) = ((ε → σ → ULift Prop) × Unit) := rfl

可能抛出异常的程序有两种后置条件。完全正确性解释 ⦃P⦄ prog ⦃⇓ r => Q' r⦄ 断言：若 P 成立，则 prog 会终止，且结果满足 Q'。部分正确性解释 ⦃P⦄ prog ⦃⇓? r => Q' r⦄ 断言：若 P 成立，并且 prog 终止，则结果满足 Q'。

语法无异常后置条件

term ::= ...
    | A postcondition expressing total correctness.
That is, it expresses that the asserted computation finishes without throwing an exception
*and* the result satisfies the given predicate `p`.
⇓ term* => term

表示完全正确性的后置条件。也就是说，它表示所断言的计算会无异常地结束，并且其结果满足给定谓词 p。

定义

Std.Do.PostCond.noThrow.{u_1} {α : Type u_1} {ps : PostShape}
  (p : α → Assertion ps) : PostCond α ps
Std.Do.PostCond.noThrow.{u_1}
  {α : Type u_1} {ps : PostShape}
  (p : α → Assertion ps) : PostCond α ps

表示完全正确性的后置条件。也就是说，它表示所断言的计算会无异常地结束，并且其结果满足给定谓词 p。

语法部分后置条件

term ::= ...
    | A postcondition expressing partial correctness.
That is, it expresses that *if* the asserted computation finishes without throwing an exception
*then* the result satisfies the given predicate `p`.
Nothing is asserted when the computation throws an exception.
⇓? term* => term

表示部分正确性的后置条件。也就是说，它表示如果所断言的计算无异常地结束，那么其结果满足给定谓词 p。当计算抛出异常时，不作任何断言。

定义

Std.Do.PostCond.mayThrow.{u_1} {α : Type u_1} {ps : PostShape}
  (p : α → Assertion ps) : PostCond α ps
Std.Do.PostCond.mayThrow.{u_1}
  {α : Type u_1} {ps : PostShape}
  (p : α → Assertion ps) : PostCond α ps

表示部分正确性的后置条件。也就是说，它表示如果所断言的计算无异常地结束，那么其结果满足给定谓词 p。当计算抛出异常时，不作任何断言。

语法后置条件蕴涵

term ::= ...
    | Entailment of postconditions.

This consists of:
 * Entailment of the assertion about the return value, for all possible return values.
 * Entailment of the exception conditions.

While implication of postconditions (`PostCond.imp`) results in a new postcondition, entailment is
an ordinary proposition.
term ⊢ₚ term

PostCond.entails 的语法糖。

定义

Std.Do.PostCond.entails.{u_1} {α : Type u_1} {ps : PostShape}
  (p q : PostCond α ps) : Prop
Std.Do.PostCond.entails.{u_1}
  {α : Type u_1} {ps : PostShape}
  (p q : PostCond α ps) : Prop

后置条件的蕴涵。

它由以下两部分组成：

对所有可能的返回值，关于返回值的断言之间存在蕴涵。
异常条件之间存在蕴涵。

后置条件的蕴含（PostCond.imp）会产生新的后置条件，而蕴涵则是普通命题。

语法后置条件合取

term ::= ...
    | Conjunction of postconditions.

This is defined pointwise, as the conjunction of the assertions about the return value and the
conjunctions of the assertions about each potential exception.
term ∧ₚ term

PostCond.and 的语法糖。

定义

Std.Do.PostCond.and.{u_1} {α : Type u_1} {ps : PostShape}
  (p q : PostCond α ps) : PostCond α ps
Std.Do.PostCond.and.{u_1} {α : Type u_1}
  {ps : PostShape} (p q : PostCond α ps) :
  PostCond α ps

后置条件的合取。

它按点定义：关于返回值的断言取合取，关于每种潜在异常的断言也分别取合取。

语法后置条件蕴含

term ::= ...
    | Implication of postconditions.

This is defined pointwise, as the implication of the assertions about the return value and the
implications of each of the assertions about each potential exception.

While entailment of postconditions (`PostCond.entails`) is an ordinary proposition, implication of
postconditions is itself a postcondition.
term →ₚ term

PostCond.imp 的语法糖。

定义

Std.Do.PostCond.imp.{u_1} {α : Type u_1} {ps : PostShape}
  (p q : PostCond α ps) : PostCond α ps
Std.Do.PostCond.imp.{u_1} {α : Type u_1}
  {ps : PostShape} (p q : PostCond α ps) :
  PostCond α ps

后置条件的蕴含。

它按点定义：关于返回值的断言取蕴含，关于每种潜在异常的断言也分别取蕴含。

后置条件的蕴涵（PostCond.entails）是普通命题，而后置条件的蕴含本身仍是后置条件。

17.2.3. 谓词变换器🔗

谓词变换器是一个函数，它将某种后置条件状态上的后置条件映射为该状态上的断言。该函数必须是合取的，即必须对 PostCond.and 满足分配律。

结构体

Std.Do.PredTrans.{u} (ps : PostShape) (α : Type u) : Type u
Std.Do.PredTrans.{u} (ps : PostShape)
  (α : Type u) : Type u

给定 ps : PostShape 和返回类型 α : Type 时的谓词变换器类型。谓词变换器 x : PredTrans ps α 是一个函数：它接受后置条件 Q : PostCond α ps，并返回前置条件 x.apply Q : Assertion ps。

构造子

Std.Do.PredTrans.mk.{u}

字段

trans : PostCond α ps → Assertion ps

实现谓词变换器的函数。

conjunctiveRaw : PredTrans.Conjunctive self.trans

谓词变换器满足合取性：t (Q₁ ∧ₚ Q₂) ⊣⊢ₛ t Q₁ ∧ t Q₂。因此，后置条件越强，得到的前置条件也越强。

定义

Std.Do.PredTrans.Conjunctive.{u} {ps : PostShape} {α : Type u}
  (t : PostCond α ps → Assertion ps) : Prop
Std.Do.PredTrans.Conjunctive.{u}
  {ps : PostShape} {α : Type u}
  (t : PostCond α ps → Assertion ps) :
  Prop

变换后置条件的合取，等价于对各后置条件分别变换后再取合取。

定义

Std.Do.PredTrans.Monotonic.{u} {ps : PostShape} {α : Type u}
  (t : PostCond α ps → Assertion ps) : Prop
Std.Do.PredTrans.Monotonic.{u}
  {ps : PostShape} {α : Type u}
  (t : PostCond α ps → Assertion ps) :
  Prop

变换后的前置条件会随后置条件增强而增强。

谓词变换器构成一个单子。 pure 运算符是恒等变换器；它只是用自己的参数实例化后置条件。 bind 运算符组合谓词变换器。

定义

Std.Do.PredTrans.pure.{u} {ps : PostShape} {α : Type u} (a : α) :
  PredTrans ps α
Std.Do.PredTrans.pure.{u} {ps : PostShape}
  {α : Type u} (a : α) : PredTrans ps α

恒等谓词变换器：它把后置条件中关于返回值的断言实例化到 a。

定义

Std.Do.PredTrans.bind.{u} {ps : PostShape} {α β : Type u}
  (x : PredTrans ps α) (f : α → PredTrans ps β) : PredTrans ps β
Std.Do.PredTrans.bind.{u} {ps : PostShape}
  {α β : Type u} (x : PredTrans ps α)
  (f : α → PredTrans ps β) :
  PredTrans ps β

通过复合两个谓词变换器，将它们按顺序连接起来。

辅助运算符 PredTrans.pushArg、PredTrans.pushExcept 和 PredTrans.pushOption 通过添加一种标准副作用来修改谓词变换器。它们用于实现 StateT、ExceptT 和 OptionT 等变换器的 WP 实例；也可用来实现可按这些变换器之一理解的单子。例如，PredTrans.pushArg 通常用于状态单子，但也可以用它实现读取器单子的实例，将读取器的值视为只读状态。

定义

Std.Do.PredTrans.pushArg.{u} {ps : PostShape} {α σ : Type u}
  (x : StateT σ (PredTrans ps) α) : PredTrans (PostShape.arg σ ps) α
Std.Do.PredTrans.pushArg.{u}
  {ps : PostShape} {α σ : Type u}
  (x : StateT σ (PredTrans ps) α) :
  PredTrans (PostShape.arg σ ps) α

为后置条件形状为 ps 的谓词变换器加入对 σ 类型状态作断言的能力，所得后置条件形状为 .arg σ ps。这是通过把 StateT σ (PredTrans ps) α 解释为 PredTrans (.arg σ ps) α 实现的。

这种解释也适用于读取器效应或只能追加的状态等各种类似状态的效应，只需将它们视为状态即可。

定义

Std.Do.PredTrans.pushExcept.{u_1} {ps : PostShape} {α ε : Type u_1}
  (x : ExceptT ε (PredTrans ps) α) : PredTrans (PostShape.except ε ps) α
Std.Do.PredTrans.pushExcept.{u_1}
  {ps : PostShape} {α ε : Type u_1}
  (x : ExceptT ε (PredTrans ps) α) :
  PredTrans (PostShape.except ε ps) α

为后置条件形状为 ps 的谓词变换器加入对 ε 类型异常作断言的能力，所得后置条件形状为 .except ε ps。这是通过把 ExceptT ε (PredTrans ps) α 解释为 PredTrans (.except ε ps) α 实现的。

这种解释也适用于提前终止等各种类似异常的效应，只需将它们视为异常即可。

定义

Std.Do.PredTrans.pushOption.{u_1} {ps : PostShape} {α : Type u_1}
  (x : OptionT (PredTrans ps) α) :
  PredTrans (PostShape.except PUnit ps) α
Std.Do.PredTrans.pushOption.{u_1}
  {ps : PostShape} {α : Type u_1}
  (x : OptionT (PredTrans ps) α) :
  PredTrans (PostShape.except PUnit ps) α

为后置条件形状为 ps 的谓词变换器加入对提前终止作断言的能力，所得后置条件形状为 .except PUnit ps。这是通过把 OptionT (PredTrans ps) α 解释为 PredTrans (.except PUnit ps) α 实现的，其中将 Option 建模为等价于 Except PUnit。

17.2.3.1. 最弱前置条件🔗

单子的最弱前置条件语义由 WP 类型类提供。 WP 实例决定单子的后置条件形状，并提供逻辑规则，将单子操作解释为该后置条件形状上的谓词变换器。

类型类

Std.Do.WP.{u, v} (m : Type u → Type v) (ps : outParam PostShape) :
  Type (max (u + 1) v)
Std.Do.WP.{u, v} (m : Type u → Type v)
  (ps : outParam PostShape) :
  Type (max (u + 1) v)

用谓词变换器 PredTrans ps α 表示单子程序 x : m α 的最弱前置条件解释。单子 m 决定 ps : PostShape。

在实际推理中，除了 WP m ps，通常还需要一个 WPMonad m ps 实例。

实例构造子

Std.Do.WP.mk.{u, v}

方法

wp : {α : Type u} → m α → PredTrans ps α

将单子程序 x : m α 解释为谓词变换器 PredTrans ps α。

语法wp 最弱前置条件记法

term ::= ...
    | `wp⟦x⟧ Q` is defined as `(WP.wp x).apply Q`. wp⟦term (: term)?⟧

wp⟦x⟧ Q 按定义等于 (WP.wp x).apply Q。

17.2.3.2. 最弱前置条件单子态射🔗

除了 WP 实例外，mvcgen 的大多数内置规约引理还依赖 WPMonad 实例。除了满足单子定律外，单子对 pure 和 bind 的实现之最弱前置条件，还应分别对应谓词变换器单子的 pure 和 bind 运算符。缺少 WPMonad 实例时，mvcgen 通常会原样返回初始证明目标。

类型类

Std.Do.WPMonad.{u, v} (m : Type u → Type v) (ps : outParam PostShape)
  [Monad m] : Type (max (u + 1) v)
Std.Do.WPMonad.{u, v}
  (m : Type u → Type v)
  (ps : outParam PostShape) [Monad m] :
  Type (max (u + 1) v)

带最弱前置条件（WP）的单子，并且其解释还是一个保持 pure 和 bind 的单子态射。

实践中，对于没有 WPMonad 实例的单子，mvcgen 通常无法有效地推理程序。 Pure.pure、Bind.bind 以及 Functor.map 等运算符的规约引理，都要求相应单子具有 WPMonad 实例。

实例构造子

Std.Do.WPMonad.mk.{u, v}

扩展

LawfulMonad m
WP m ps

方法

map_const : ∀ {α β : Type u}, Functor.mapConst = Functor.map ∘ Function.const β

继承自父结构。

id_map : ∀ {α : Type u} (x : m α), id <$> x = x

继承自父结构。

comp_map : ∀ {α β γ : Type u} (g : α → β) (h : β → γ) (x : m α), (h ∘ g) <$> x = h <$> g <$> x

继承自父结构。

seqLeft_eq : ∀ {α β : Type u} (x : m α) (y : m β), x <* y = Function.const β <$> x <*> y

继承自父结构。

seqRight_eq : ∀ {α β : Type u} (x : m α) (y : m β), x *> y = Function.const α id <$> x <*> y

继承自父结构。

pure_seq : ∀ {α β : Type u} (g : α → β) (x : m α), pure g <*> x = g <$> x

继承自父结构。

map_pure : ∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)

继承自父结构。

seq_pure : ∀ {α β : Type u} (g : m (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g

继承自父结构。

seq_assoc : ∀ {α β γ : Type u} (x : m α) (g : m (α → β)) (h : m (β → γ)), h <*> (g <*> x) = Function.comp <$> h <*> g <*> x

继承自父结构。

bind_pure_comp : ∀ {α β : Type u} (f : α → β) (x : m α),
  (do
      let a ← x
      pure (f a)) =
    f <$> x

继承自父结构。

bind_map : ∀ {α β : Type u} (f : m (α → β)) (x : m α),
  (do
      let x_1 ← f
      x_1 <$> x) =
    f <*> x

继承自父结构。

pure_bind : ∀ {α β : Type u} (x : α) (f : α → m β), pure x >>= f = f x

继承自父结构。

bind_assoc : ∀ {α β γ : Type u} (x : m α) (f : α → m β) (g : β → m γ), x >>= f >>= g = x >>= fun x => f x >>= g

继承自父结构。

wp : {α : Type u} → m α → PredTrans ps α

继承自父结构。

wp_pure : ∀ {α : Type u} (a : α), wp (pure a) = pure a

WP.wp 保持 pure。

wp_bind : ∀ {α β : Type u} (x : m α) (f : α → m β),
  (wp do
      let a ← x
      f a) =
    do
    let a ← wp x
    wp (f a)

WP.wp 保持 bind。

缺少 WPMonad 实例

单字段结构 Identity 的行为类似恒等单子 Id。它有 WP 实例，但没有 WPMonad 实例：

structure Identity (α : Type u) where
  run : α

variable {α : Type u}

instance : Monad Identity where
  pure x := ⟨x⟩
  bind x f := f x.run

instance : WP Identity .pure where
  wp x := PredTrans.pure x.run

theorem Identity.of_wp_run_eq {x : α} {prog : Identity α}
    (h : Identity.run prog = x) (P : α → Prop) :
    (⊢ₛ wp⟦prog⟧ (⇓ a => ⟨P a⟩)) → P x := byα:Type ux:αprog:Identity αh:prog.run = xP:α → Prop⊢ (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun a => { down := P a })) → P x
  simp_all [WP.wp, ← h]All goals completed! 🐙

缺少该实例会使 mvcgen 无法使用 pure 和 bind 的规约。其通常表现为生成一个与原目标相同的验证条件。下面这个函数反转列表：

def rev (xs : List α) : Identity (List α) := do
  let mut out := []
  for x in xs do
    out := x :: out
  return out

若其结果等于 List.reverse，它就是正确的。然而，mvcgen 并没有让目标变得更容易证明：

theorem rev_correct :
    (rev xs).run = xs.reverse := unsolved goals
vc1α✝:Type u_1xs x:List α✝h:(rev xs).run = xout✝:List α✝ := []⊢ (wp⟦do
      let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s))
      pure __s⟧
    (PostCond.noThrow fun a => { down := a = xs.reverse })).downbyα✝:Type u_1xs:List α✝⊢ (rev xs).run = xs.reverse
  generalize h : (rev xs).run = xα✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = x⊢ x = xs.reverse
  apply Identity.of_wp_run_eq hα✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = x⊢ ⊢ₛ wp⟦rev xs⟧ (PostCond.noThrow fun a => { down := a = xs.reverse })
  mvcgen [rev]vc1α✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = xout✝:List α✝ := []⊢ (wp⟦do
      let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s))
      pure __s⟧
    (PostCond.noThrow fun a => { down := a = xs.reverse })).down

unsolved goals
vc1α✝:Type u_1xs x:List α✝h:(rev xs).run = xout✝:List α✝ := []⊢ (wp⟦do
      let __s ← forIn xs out✝ fun x __s => pure (ForInStep.yield (x :: __s))
      pure __s⟧
    (PostCond.noThrow fun a => { down := a = xs.reverse })).down

如果验证条件就是原问题，甚至没有对 bind 做任何简化，通常是因为缺少 WPMonad 实例。添加合适的实例即可解决此问题：

instance : WPMonad Identity .pure where
  wp_pure _ := rfl
  wp_bind _ _ := rfl

有了该实例和合适的不变式，mvcgen 与 grind 就能证明该定理。

theorem rev_correct :
    (rev xs).run = xs.reverse := byα✝:Type u_1xs:List α✝⊢ (rev xs).run = xs.reverse
  generalize h : (rev xs).run = xα✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = x⊢ x = xs.reverse
  apply Identity.of_wp_run_eq hα✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = x⊢ ⊢ₛ wp⟦rev xs⟧ (PostCond.noThrow fun a => { down := a = xs.reverse })
  simp only [rev]α✝:Type u_1xs:List α✝x:List α✝h:(rev xs).run = x⊢ ⊢ₛ
  wp⟦do
      let __s ← forIn xs [] fun x __s => pure (ForInStep.yield (x :: __s))
      pure __s⟧
    (PostCond.noThrow fun a => { down := a = xs.reverse })
  mvcgen invariants
  · ⇓⟨xs, out⟩ =>
    ⌜out = xs.prefix.reverse⌝
  with grindAll goals completed! 🐙

在线查看 ↪

17.2.3.3. 充分性引理🔗

可从纯代码调用的单子通常会提供一个调用运算符：它以任何必需的输入状态为参数，返回与输出状态配对的值，或某种异常值。例如 StateT.run、ExceptT.run 和 Id.run。 充分性引理在关于单子程序调用的陈述与由其 WP 实例给出的程序最弱前置条件语义之间架起桥梁。它们表明：若调用的最弱前置条件为真，则关于该调用的性质为真。

定理

Std.Do.Id.of_wp_run_eq.{u} {α : Type u} {x : α} {prog : Id α}
  (h : prog.run = x) (P : α → Prop) :
  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun a => { down := P a })) → P x
Std.Do.Id.of_wp_run_eq.{u} {α : Type u}
  {x : α} {prog : Id α} (h : prog.run = x)
  (P : α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (PostCond.noThrow fun a =>
          { down := P a })) →
    P x

Id.run 的可靠性引理。它由 WPSound.of_wp_canReturn 推导而来： Id.run prog = x 正是 MonadAttach.CanReturn prog x 的见证。

定理

Std.Do.StateM.of_wp_run_eq {α σ : Type} {x : α × σ} {s : σ}
  {prog : StateM σ α} (h : StateT.run prog s = x) (P : α × σ → Prop) :
  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun a s' => ⌜P (a, s')⌝) s) → P x
Std.Do.StateM.of_wp_run_eq {α σ : Type}
  {x : α × σ} {s : σ} {prog : StateM σ α}
  (h : StateT.run prog s = x)
  (P : α × σ → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (PostCond.noThrow fun a s' =>
          ⌜P (a, s')⌝)
        s) →
    P x

StateM.run 的可靠性引理；它是 StateT.of_wp_run 在 Id 上的特化。

定理

Std.Do.StateM.of_wp_run'_eq {α σ : Type} {x : α} {s : σ}
  {prog : StateM σ α} (h : StateT.run' prog s = x) (P : α → Prop) :
  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun a => ⌜P a⌝) s) → P x
Std.Do.StateM.of_wp_run'_eq {α σ : Type}
  {x : α} {s : σ} {prog : StateM σ α}
  (h : StateT.run' prog s = x)
  (P : α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (PostCond.noThrow fun a => ⌜P a⌝)
        s) →
    P x

StateM.run' 的可靠性引理；它是 StateT.of_wp_run 在 Id 上的特化。

定理

Std.Do.ReaderM.of_wp_run_eq.{u} {α ρ : Type u} {x : α} {r : ρ}
  {prog : ReaderM ρ α} (h : ReaderT.run prog r = x) (P : α → Prop) :
  (⊢ₛ wp⟦prog⟧ (PostCond.noThrow fun a x => ⌜P a⌝) r) → P x
Std.Do.ReaderM.of_wp_run_eq.{u}
  {α ρ : Type u} {x : α} {r : ρ}
  {prog : ReaderM ρ α}
  (h : ReaderT.run prog r = x)
  (P : α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (PostCond.noThrow fun a x =>
          ⌜P a⌝)
        r) →
    P x

ReaderM.run 的可靠性引理；它是 ReaderT.of_wp_run 在 Id 上的特化。

定理

Std.Do.Except.of_wp_eq {ε α : Type} {x prog : Except ε α} (h : prog = x)
  (P : Except ε α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (fun a => ⌜P (Except.ok a)⌝, fun e => ⌜P (Except.error e)⌝,
          PUnit.unit)) →
    P x
Std.Do.Except.of_wp_eq {ε α : Type}
  {x prog : Except ε α} (h : prog = x)
  (P : Except ε α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (fun a => ⌜P (Except.ok a)⌝,
          fun e => ⌜P (Except.error e)⌝,
          PUnit.unit)) →
    P x

Except 的可靠性引理；它是 ExceptT.of_wp_run 在 Id 上的特化。

定理

Std.Do.EStateM.of_wp_run_eq.{u_1} {ε σ : Type u_1} {s : σ}
  {α : Type u_1} {x : EStateM.Result ε σ α} {prog : EStateM ε σ α}
  (h : prog.run s = x) (P : EStateM.Result ε σ α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (fun a s' => ⌜P (EStateM.Result.ok a s')⌝, fun e s' =>
          ⌜P (EStateM.Result.error e s')⌝, PUnit.unit)
        s) →
    P x
Std.Do.EStateM.of_wp_run_eq.{u_1}
  {ε σ : Type u_1} {s : σ} {α : Type u_1}
  {x : EStateM.Result ε σ α}
  {prog : EStateM ε σ α}
  (h : prog.run s = x)
  (P : EStateM.Result ε σ α → Prop) :
  (⊢ₛ
      wp⟦prog⟧
        (fun a s' =>
          ⌜P (EStateM.Result.ok a s')⌝,
          fun e s' =>
          ⌜P (EStateM.Result.error e s')⌝,
          PUnit.unit)
        s) →
    P x

EStateM.run 的可靠性引理。当需要证明表达式 x（定义为 EStateM.run prog s）的性质，并希望用 mvcgen 推理 prog 时，此引理很有用。

17.2.4. 霍尔三元组🔗

霍尔三元组 (Hoare, 1969)C. A. R. Hoare (1969). “An Axiomatic Basis for Computer Programming”. Communications of the ACM. 12(10), pp. 576–583. 由前置条件、程序和后置条件组成。若在满足前置条件的状态中运行程序，所得状态将满足后置条件。

定义

Std.Do.Triple.{u, v} {m : Type u → Type v} {ps : PostShape} [WP m ps]
  {α : Type u} (x : m α) (P : Assertion ps) (Q : PostCond α ps) : Prop
Std.Do.Triple.{u, v} {m : Type u → Type v}
  {ps : PostShape} [WP m ps] {α : Type u}
  (x : m α) (P : Assertion ps)
  (Q : PostCond α ps) : Prop

用于推理单子程序的霍尔三元组。霍尔三元组 Triple x P Q 是 x 的一个规约：若断言 P 在 x 运行前成立，则后置条件 Q 在 x 运行后成立。

⦃P⦄ x ⦃Q⦄ 是 Triple x P Q 的便捷语法。

语法霍尔三元组记法

term ::= ...
    | A Hoare triple for reasoning about monadic programs. A Hoare triple `Triple x P Q` is a
*specification* for `x`: if assertion `P` holds before `x`, then postcondition `Q` holds after
running `x`.

`⦃P⦄ x ⦃Q⦄` is convenient syntax for `Triple x P Q`.
⦃ term ⦄ term ⦃ term ⦄

⦃P⦄ x ⦃Q⦄ 是 Triple x P Q 的语法糖。

定理

Std.Do.Triple.and.{u, v} {m : Type u → Type v} {ps : PostShape}
  {α : Type u} {P₁ : Assertion ps} {Q₁ : PostCond α ps}
  {P₂ : Assertion ps} {Q₂ : PostCond α ps} [WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₂⦄) : ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄
Std.Do.Triple.and.{u, v}
  {m : Type u → Type v} {ps : PostShape}
  {α : Type u} {P₁ : Assertion ps}
  {Q₁ : PostCond α ps} {P₂ : Assertion ps}
  {Q₂ : PostCond α ps} [WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₂⦄) :
  ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄

同一程序 x 的两个霍尔三元组规约的合取。该定理便于分解证明：可分别证明关于 x 的互不相关的事实，再用此定理将它们合并。

定理

Std.Do.Triple.mp.{u, v} {m : Type u → Type v} {ps : PostShape}
  {α : Type u} {P₁ : Assertion ps} {Q₁ : PostCond α ps}
  {P₂ : Assertion ps} {Q₂ : PostCond α ps} [WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄) (h₂ : ⦃P₂⦄ x ⦃Q₁ →ₚ Q₂⦄) : ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄
Std.Do.Triple.mp.{u, v}
  {m : Type u → Type v} {ps : PostShape}
  {α : Type u} {P₁ : Assertion ps}
  {Q₁ : PostCond α ps} {P₂ : Assertion ps}
  {Q₂ : PostCond α ps} [WP m ps] (x : m α)
  (h₁ : ⦃P₁⦄ x ⦃Q₁⦄)
  (h₂ : ⦃P₂⦄ x ⦃Q₁ →ₚ Q₂⦄) :
  ⦃P₁ ∧ P₂⦄ x ⦃Q₁ ∧ₚ Q₂⦄

同一程序 x 的两个霍尔三元组规约上的肯定前件规则。该定理便于拆分证明。若 h₁ : Triple x P₁ Q₁ 证明了 x 的基础性质，而 h₂ : Triple x P₂ (Q₁ →ₚ Q₂) 是建立在 Q₁ 基础上的 Q₂ 高级证明，则 mp x h₁ h₂ 给出关于 x 的 Q₂ 证明。

17.2.5. 规约引理🔗

规约引理是将函数与霍尔三元组关联起来的指定定理。当 mvcgen 遇到函数时，它会检查是否注册了规约引理，并尝试用它们解决中间的验证条件。若没有适用的规约引理，语句的前置条件与后置条件之间的联系就会成为验证条件。规约引理使我们能对单子代码库进行组合式推理。

将 spec 属性应用于陈述为霍尔三元组的定理时，会把该定理注册为规约引理。这些引理按优先级顺序使用。

spec 属性也可以应用于定义。用于定义时，它表示应在生成验证条件期间展开该定义。

属性spec 规约属性

attr ::= ...
    | Theorems tagged with the `spec` attribute are used by the `mspec` and `mvcgen` tactics.

* When used on a theorem `foo_spec : Triple (foo a b c) P Q`, then `mspec` and `mvcgen` will use
  `foo_spec` as a specification for calls to `foo`.
* Otherwise, when used on a definition that `@[simp]` would work on, it is added to the internal
  simp set of `mvcgen` that is used within `wp⟦·⟧` contexts to simplify match discriminants and
  applications of constants.
spec prio?

带 spec 属性的定理由 mspec 和 mvcgen 策略使用。

当该属性用于定理 foo_spec : Triple (foo a b c) P Q 时，mspec 和 mvcgen 会将 foo_spec 用作调用 foo 的规约。
否则，当该属性用于一个可由 @[simp] 化简的定义时，该定义会加入 mvcgen 的内部 simp 集；此 simp 集用于在 wp⟦·⟧ 上下文中化简模式匹配的判别项和常量的应用。

规约引理中的全称量化变量可用于关联输入状态、输出状态和返回值。这些变量称为模式变量。

模式变量

函数 double 将 Nat 状态的值翻倍：

def double : StateM Nat Unit := do
  modify (2 * ·)

它的规约应当关联初始状态和最终状态，但无法预知它们的确切值。该规约使用一个模式变量代表初始状态：

theorem double_spec :
    ⦃ fun s => ⌜s = n⌝ ⦄ double ⦃ ⇓ () s => ⌜s = 2 * n⌝ ⦄ := byn:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ double ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  simp [double]n:Nat⊢ ⦃fun s => ⌜s = n⌝⦄ modify fun x => 2 * x ⦃PostCond.noThrow fun x s => ⌜s = 2 * n⌝⦄
  mvcgen with grindAll goals completed! 🐙

前置条件中的断言之所以是函数，是因为 StateM Nat 的 PostShape 为 .arg Nat .pure，而 Assertion (.arg Nat .pure) 即 SPred [Nat]。

在线查看 ↪

17.2.6. 不变式规约🔗

这些类型用于不变式。 ForIn.forIn 和 ForIn'.forIn' 的规约引理采用 Invariant 类型的参数，而 mvcgen 会确保其他自动化过程不会意外生成不变式。

定义

Std.Do.Invariant.{u₁, u₂} {α : Type u₁} (xs : List α) (β : Type u₂)
  (ps : PostShape) : Type (max u₂ u₁)
Std.Do.Invariant.{u₁, u₂} {α : Type u₁}
  (xs : List α) (β : Type u₂)
  (ps : PostShape) : Type (max u₂ u₁)

for ... in ... 循环的规约所使用的循环不变式类型。循环不变式是一个接受下列参数的 PostCond：

表示循环迭代状态的 List.Cursor xs。它以 for 循环迭代的元素列表 xs 为参数。
类型为 β 的状态元组；它是若干层 MProd 的嵌套，表示 let mut 变量和提前返回。

循环规约引理按如下方式使用它：进入循环前，游标前缀为空，后缀为 xs；离开循环后，游标前缀为 xs，后缀为空；归纳步骤中，不变式对首元素为 x 的后缀成立；运行循环体后，把 x 移到前缀，不变式仍然成立。

定义

Std.Do.Invariant.withEarlyReturn.{u₁, u₂} {β : Type (max u₁ u₂)}
  {ps : PostShape} {α : Type (max u₁ u₂)} {xs : List α}
  {γ : Type (max u₁ u₂)} (onContinue : xs.Cursor → β → Assertion ps)
  (onReturn : γ → β → Assertion ps)
  (onExcept : ExceptConds ps := ExceptConds.false) :
  Invariant xs (MProd (Option γ) β) ps
Std.Do.Invariant.withEarlyReturn.{u₁, u₂}
  {β : Type (max u₁ u₂)} {ps : PostShape}
  {α : Type (max u₁ u₂)} {xs : List α}
  {γ : Type (max u₁ u₂)}
  (onContinue :
    xs.Cursor → β → Assertion ps)
  (onReturn : γ → β → Assertion ps)
  (onExcept : ExceptConds ps :=
    ExceptConds.false) :
  Invariant xs (MProd (Option γ) β) ps

用于为带提前返回的循环指定循环不变式的辅助定义。

返回类型为 γ 的 for ... in ... 循环会精译为如下调用：

forIn (β := MProd (Option γ) ...) (b := ⟨none, ...⟩) collection loopBody

注意，MProd 状态元组的第一个分量是可选的提前返回值。没有提前返回时它为 none，循环以 r 提前返回时则为 some r。

此函数可根据循环体是否提前终止来指定不同的不变式。发生提前返回时，循环实际上已经结束；不变式中的附加断言 ⌜xs.suffix = []⌝ 编码了这一事实。该断言对顺利证明归纳步骤至关重要：它与循环体开始处归纳假设中的 xs.suffix = x::rest 相矛盾，因此用户无需证明“循环已经提前返回，却又执行下一次循环体迭代”这一虚假情形。

不变式使用列表来建模 Lean.Parser.Term.doFor : doElem`for x in e do s` iterates over `e` assuming `e`'s type has an instance of the `ForIn` typeclass. `break` and `continue` are supported inside `for` loops. `for x in e, x2 in e2, ... do s` iterates over the given collections in parallel, until at least one of them is exhausted. The types of `e2` etc. must implement the `Std.ToStream` typeclass.for 循环中的值序列。循环中的当前位置用 List.Cursor 跟踪；它将列表中的位置表示为该位置左侧元素与右侧元素的组合。该类型并非传统的拉链结构；传统拉链为高效移动会反转前缀，而此类型用于规约和证明而非运行时代码，因此前缀保持原顺序。

结构体

List.Cursor.{u} {α : Type u} (l : List α) : Type u
List.Cursor.{u} {α : Type u}
  (l : List α) : Type u

指向列表中特定位置的指针。列表游标用于 mvcgen 策略的循环不变式。

将游标向左或向右移动所需时间与游标当前位置成线性关系，因此这种数据结构不适合运行时代码。

构造子

List.Cursor.mk.{u}

字段

prefix : List α

列表中位于当前位置之前的元素。

suffix : List α

从当前位置开始的元素。若当前位置在最后一个元素之后，则后缀为空；否则，后缀的第一个元素就是游标当前指向的元素。

property : self.prefix ++ self.suffix = l

将前缀与后缀连接起来可得到原列表。

定义

List.Cursor.at.{u_1} {α : Type u_1} (l : List α) (n : Nat) : l.Cursor
List.Cursor.at.{u_1} {α : Type u_1}
  (l : List α) (n : Nat) : l.Cursor

在列表 l 的位置 n 创建游标。前缀包含最前面的 n 个元素，后缀包含其余元素。若 n 大于列表长度，则游标位于列表末尾。

定义

List.Cursor.pos.{u_1} {α✝ : Type u_1} {l : List α✝} (c : l.Cursor) : Nat
List.Cursor.pos.{u_1} {α✝ : Type u_1}
  {l : List α✝} (c : l.Cursor) : Nat

游标在列表中的位置。这是前缀元素数量的简写。

定义

List.Cursor.current.{u_1} {α : Type u_1} {l : List α} (c : l.Cursor)
  (h : 0 < c.suffix.length := by get_elem_tactic) : α
List.Cursor.current.{u_1} {α : Type u_1}
  {l : List α} (c : l.Cursor)
  (h : 0 < c.suffix.length := by
    get_elem_tactic) :
  α

返回游标当前位置的元素。

要求当前位置确实存在元素：后缀必须非空，因此游标不能位于列表末尾。

定义

List.Cursor.tail.{u_1} {α✝ : Type u_1} {l : List α✝} (s : l.Cursor)
  (h : 0 < s.suffix.length := by get_elem_tactic) : l.Cursor
List.Cursor.tail.{u_1} {α✝ : Type u_1}
  {l : List α✝} (s : l.Cursor)
  (h : 0 < s.suffix.length := by
    get_elem_tactic) :
  l.Cursor

将游标向前推进一个位置，把当前元素从后缀移到前缀。

要求游标尚未位于列表末尾。

定义

List.Cursor.begin.{u_1} {α : Type u_1} (l : List α) : l.Cursor
List.Cursor.begin.{u_1} {α : Type u_1}
  (l : List α) : l.Cursor

在列表开头（位置 0）创建游标。前缀为空，后缀为整个列表。

定义

List.Cursor.end.{u_1} {α : Type u_1} (l : List α) : l.Cursor
List.Cursor.end.{u_1} {α : Type u_1}
  (l : List α) : l.Cursor

在列表末尾创建游标。前缀为整个列表，后缀为空。