feat: Subtype

Closes #173

Manual/BasicTypes.lean

@@ -18,6 +18,7 @@ import Manual.BasicTypes.Empty
 import Manual.BasicTypes.Products
 import Manual.BasicTypes.Sum
 import Manual.BasicTypes.List
+import Manual.BasicTypes.Subtype
 
 open Manual.FFIDocType
 
@@ -356,17 +357,8 @@ end ShortCircuit
 
 {include 0 Manual.BasicTypes.Array}
 
-# Subtypes
-%%%
-tag := "Subtype"
-%%%
-
-:::planned 173
- * When to use them?
- * Run-time representation
-:::
+{include 0 Manual.BasicTypes.Subtype}
 
-{docstring Subtype}
 
 # Lazy Computations
 %%%

Manual/BasicTypes/List.lean

@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/

Manual/BasicTypes/Subtype.lean

@@ -0,0 +1,128 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import VersoManual
+
+import Manual.Meta
+
+import Manual.BasicTypes.Array.Subarray
+import Manual.BasicTypes.Array.FFI
+
+open Manual.FFIDocType
+
+open Verso.Genre Manual
+
+set_option pp.rawOnError true
+
+
+#doc (Manual) "Subtypes" =>
+%%%
+tag := "Subtype"
+%%%
+
+The structure {name}`Subtype` represents the elements of a type that satisfy some predicate.
+They are used pervasively both in mathematics and in programming; in mathematics, they are used similarly to subsets, while in programming, they allow information that is known about a value to be represented in a way that is visible to Lean's logic.
+
+Syntactically, an element of a {name}`Subtype` resembles a tuple of the base type's element and the proof that it satisfies the proposition.
+They differ from dependent pair types ({name}`Sigma`) in that the second element is a proof of a proposition rather than data, and from existential quantification in that the entire {name}`Subtype` is a type rather than a proposition.
+Even though they are pairs syntactically, {name}`Subtype` should really be thought of as elements of the base type with associated proof obligations.
+
+Subtypes are {ref "inductive-types-trivial-wrappers"}[trivial wrappers].
+They are thus represented identically to the base type in compiled code.
+
+
+{docstring Subtype}
+
+::::leanSection
+```lean (show := false)
+variable {α : Type u} {p : Prop}
+```
+:::syntax term (title := "Subtypes")
+```grammar
+{ $x : $t:term // $t:term }
+```
+
+{lean}`{ x : α // p }` is a notation for {lean}`Subtype fun (x : α) => p`.
+
+The type ascription may be omitted:
+
+```grammar
+{ $x:ident // $t:term }
+```
+
+{lean}`{ x // p }` is a notation for {lean}`Subtype fun (x : _) => p`.
+:::
+::::
+
+Due to {tech}[proof irrelevance] and {tech key:="η-equivalence"}[η-equality], two elements of a subtype are definitionally equal when the elements of the base type are definitionally equal.
+In a proof, the {tactic}`ext` tactic can be used to transform a goal of equality of elements of a subtype into equality of their values.
+
+:::example "Definitional Equality of Subtypes"
+
+The non-empty strings {lean}`s1` and {lean}`s2` are definitionally equal despite the fact that their embedded proof terms are different.
+No case splitting is needed in order to prove that they are equal.
+
+```lean
+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.data_eq_of_eq h)
+
+theorem s1_eq_s2 : s1 = s2 := by rfl
+```
+:::
+
+:::example "Extensional Equality of Subtypes"
+
+The non-empty strings {lean}`s1` and {lean}`s2` are definitionally equal.
+Ignoring that fact, the equality of the embedded strings can be used to prove that they are equal.
+The {tactic}`ext` tactic transforms a goal that consists of equality of non-empty strings into a goal that consists of equality of the strings.
+
+```lean
+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.data_eq_of_eq h)
+
+theorem s1_eq_s2 : s1 = s2 := by
+  ext
+  dsimp only [s1, s2]
+```
+:::
+
+There is a coercion from a subtype to its base type.
+This allows subtypes to be used in positions where the base type is expected, essentially erasing the proof that the value satisfies the predicate.
+
+:::example "Subtype Coercions"
+
+Elements of subtypes can be coerced to their base type.
+Here, {name}`nine` is coerced from a subtype of `Nat` that contains multiples of {lean type:="Nat"}`3` to {lean}`Nat`.
+
+```lean (name := subtype_coe)
+abbrev DivBy3 := { x : Nat // x % 3 = 0 }
+
+def nine : DivBy3 := ⟨9, by rfl⟩
+
+set_option eval.type true in
+#eval Nat.succ nine
+```
+```leanOutput subtype_coe
+10 : Nat
+```
+
+:::

Manual/Elaboration.lean

@@ -165,7 +165,7 @@ The language implemented by the kernel is a version of the Calculus of Construct
  * A {tech}[predicative], non-cumulative hierarchy of universes of data
  * {ref "quotients"}[Quotient types] with a definitional computation rule
  * Propositional function extensionality{margin}[Function extensionality is a theorem that can be proved using quotient types, but it is such an important consequence that it's worth listing separately.]
- * Definitional η-equality for functions and products
+ * Definitional {tech key:="η-equivalence"}[η-equality] for functions and products
  * Universe-polymorphic definitions
  * Consistency: there is no axiom-free closed term of type {lean}`False`
 

Manual/Language/Functions.lean

@@ -165,7 +165,7 @@ axiom f : (x : α) → β x
 example : (fun x => f x) = f := by rfl
 ```
 
-In addition to reduction and renaming of bound variables, definitional equality does support one limited form of extensionality, called {deftech}_η-equivalence_, in which functions are equal to abstractions whose bodies apply them to the argument.
+In addition to reduction and renaming of bound variables, definitional equality does support one limited form of extensionality, called {tech}_η-equivalence_, in which functions are equal to abstractions whose bodies apply them to the argument.
 Given {lean}`f` with type {lean}`(x : α) → β x`, {lean}`f` is definitionally equal to {lean}`fun x => f x`.
 ::::
 

Manual/Meta/Lean.lean

@@ -558,6 +558,16 @@ def option.descr : InlineDescr where
       | .ok (hl : Highlighted) =>
         hl.inlineHtml "examples"
 
+@[directive_expander leanSection]
+def leanSection : DirectiveExpander
+  | args, contents => do
+    let name? ← ArgParse.run ((some <$> .positional `name .string) <|> pure none) args
+    let arg ← `(argument| «show» := false)
+    let code := name?.map (s!"section {·}") |>.getD "section"
+    let start ← `(block|```lean $arg | $(quote code) ```)
+    let code := name?.map (s!"end {·}") |>.getD "end"
+    let «end» ← `(block|```lean $arg | $(quote code) ```)
+    return #[← elabBlock start] ++ (← contents.mapM elabBlock) ++ #[← elabBlock «end»]
 
 
 def Block.signature : Block where

Manual/Types.lean

@@ -79,7 +79,7 @@ example : S.mk x.f1 x.f2 = x := by rfl
 export S (f1 f2)
 ```
 
-Definitional equality includes η-equivalence of functions and single-constructor inductive types.
+Definitional equality includes {deftech}[η-equivalence] of functions and single-constructor inductive types.
 That is, {lean}`fun x => f x` is definitionally equal to {lean}`f`, and {lean}`S.mk x.f1 x.f2` is definitionally equal to {lean}`x`, if {lean}`S` is a structure with fields {lean}`f1` and {lean}`f2`.
 It also features {deftech}_proof irrelevance_: any two proofs of the same proposition are definitionally equal.
 It is reflexive, symmetric, and a congruence.

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d15e407047fcfd248694d69b6236ade1198449db",
+   "rev": "c9f190cc9f6911bc20c7062e7f2930f0b05269b9",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",