Lean 语言参考

20.20. 亚型🔗

结构 Subtype 表示满足某些谓词的类型的元素。 它们在数学和编程中广泛使用。在数学中，它们的使用方式与子集类似，而在编程中，它们允许以 Lean 逻辑可见的方式表示已知值的信息。

从语法上讲，Subtype 的元素类似于基本类型元素的元组以及它满足命题的证明。 它们与依赖对类型 (Sigma) 的不同之处在于，第二个元素是命题的证明而不是数据；它们与存在量化的不同之处在于，整个 Subtype 是类型而不是命题。 尽管它们在语法上是成对的，但 Subtype 实际上应该被视为具有相关证明义务的基本类型的元素。

子类型是 普通包装器。 因此，它们在编译代码中的表示方式与基本类型相同。

🔗structure
Subtype.{u} {α : Sort u} (p : α → Prop) : Sort (max 1 u)
Subtype.{u} {α : Sort u} (p : α → Prop) :
  Sort (max 1 u)

All the elements of a type that satisfy a predicate.

Subtype p, usually written { x : α // p x } or { x // p x }, contains all elements x : α for which p x is true. Its constructor is a pair of the value and the proof that it satisfies the predicate. In run-time code, { x : α // p x } is represented identically to α.

There is a coercion from { x : α // p x } to α, so elements of a subtype may be used where the underlying type is expected.

Examples:

  • { n : Nat // n % 2 = 0 } is the type of even numbers.

  • { xs : Array String // xs.size = 5 } is the type of arrays with five Strings.

  • Given xs : List α, List { x : α // x ∈ xs } is the type of lists in which all elements are contained in xs.

Conventions for notations in identifiers:

  • The recommended spelling of { x // p x } in identifiers is subtype.

Constructor

Subtype.mk.{u}

Fields

val : α

The value in the underlying type that satisfies the predicate.

property : p self.val

The proof that val satisfies the predicate p.

syntaxSubtypes
term ::= ...
    | All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.{ ident : term // term }

{ x : α // p } 是 Subtype fun (x : α) => p 的表示法。

类型归属可以省略：

term ::= ...
    | All the elements of a type that satisfy a predicate.

`Subtype p`, usually written `{ x : α // p x }` or `{ x // p x }`, contains all elements `x : α` for
which `p x` is true. Its constructor is a pair of the value and the proof that it satisfies the
predicate. In run-time code, `{ x : α // p x }` is represented identically to `α`.

There is a coercion from `{ x : α // p x }` to `α`, so elements of a subtype may be used where the
underlying type is expected.

Examples:
 * `{ n : Nat // n % 2 = 0 }` is the type of even numbers.
 * `{ xs : Array String // xs.size = 5 }` is the type of arrays with five `String`s.
 * Given `xs : List α`, `List { x : α // x ∈ xs }` is the type of lists in which all elements are
   contained in `xs`.


Conventions for notations in identifiers:

 * The recommended spelling of `{ x // p x }` in identifiers is `subtype`.{ ident // term }

{ x // p } 是 Subtype fun (x : _) => p 的表示法。

由于 证明无关性 和 η-相等，当基本类型的元素定义等价时，子类型的两个元素定义等价。 在证明中，ext策略可用于将子类型元素相等的目标转换为其值相等的目标。

Definitional Equality of Subtypes

非空字符串 s1 和 s2 在定义上是相等的，尽管它们嵌入的证明术语不同。 无需进行大小写分割即可证明它们相等。

def NonEmptyString := { x : String // x ≠ "" } def s1 : NonEmptyString := ⟨"equal", ne_of_beq_false rfl⟩ def s2 : NonEmptyString where val := "equal" property := fun h => List.cons_ne_nil _ _ (String.ext_iff.mp h) theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2 All goals completed! 🐙
Live ↪
Extensional Equality of Subtypes

非空字符串 s1 和 s2 在定义上是相等的。 忽略这一事实，可以使用嵌入字符串的相等性来证明它们是相等的。 ext策略将由非空字符串相等组成的目标转换为由字符串相等组成的目标。

abbrev NonEmptyString := { x : String // x ≠ "" } def s1 : NonEmptyString := ⟨"equal", ne_of_beq_false rfl⟩ def s2 : NonEmptyString where val := "equal" property := fun h => List.cons_ne_nil _ _ (String.ext_iff.mp h) theorem s1_eq_s2 : s1 = s2 := ⊢ s1 = s2 i✝:Nata✝:Char⊢ s1.val.toList[i✝]? = some a✝ ↔ s2.val.toList[i✝]? = some a✝ i✝:Nata✝:Char⊢ "equal".toList[i✝]? = some a✝ ↔ "equal".toList[i✝]? = some a✝ All goals completed! 🐙
Live ↪

存在从子类型到其基类型的强制。 这允许在需要基本类型的位置使用子类型，从本质上消除了该值满足谓词的证明。

Subtype Coercions

子类型的元素可以强制为其基本类型。 此处，nine 是从包含 3 到 Nat 倍数的 Nat 子类型强制转换而来。

abbrev DivBy3 := { x : Nat // x % 3 = 0 } def nine : DivBy3 := ⟨9, ⊢ 9 % 3 = 0 All goals completed! 🐙⟩ set_option eval.type true in 10 : Nat#eval Nat.succ nine 
10 : Nat
Live ↪