doc: update lean 3 -> lean 4 in declarations.md
This commit is contained in:
Mario Carneiro
Leonardo de Moura
parent
5478485de1
commit
bff9cdbfb3
1 changed files with 272 additions and 293 deletions
|
|
@ -165,70 +165,70 @@ Below are some common examples of inductive types, many of which are defined in
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
universes u v
|
||||
namespace Hide
|
||||
universe u v
|
||||
|
||||
-- BEGIN
|
||||
inductive empty : Type
|
||||
inductive Empty : Type
|
||||
|
||||
inductive unit : Type
|
||||
| star : unit
|
||||
inductive Unit : Type
|
||||
| unit : Unit
|
||||
|
||||
inductive bool : Type
|
||||
| ff : bool
|
||||
| tt : bool
|
||||
inductive Bool : Type
|
||||
| false : Bool
|
||||
| true : Bool
|
||||
|
||||
inductive prod (α : Type u) (β : Type v) : Type (max u v)
|
||||
| mk : α → β → prod
|
||||
inductive Prod (α : Type u) (β : Type v) : Type (max u v)
|
||||
| mk : α → β → Prod α β
|
||||
|
||||
inductive sum (α : Type u) (β : Type v)
|
||||
| inl : α → sum
|
||||
| inr : β → sum
|
||||
inductive Sum (α : Type u) (β : Type v)
|
||||
| inl : α → Sum α β
|
||||
| inr : β → Sum α β
|
||||
|
||||
inductive sigma (α : Type u) (β : α → Type v)
|
||||
| mk : Π a : α, β a → sigma
|
||||
inductive Sigma (α : Type u) (β : α → Type v)
|
||||
| mk : (a : α) → β a → Sigma α β
|
||||
|
||||
inductive false : Prop
|
||||
|
||||
inductive true : Prop
|
||||
| trivial : true
|
||||
inductive True : Prop
|
||||
| trivial : True
|
||||
|
||||
inductive and (p q : Prop) : Prop
|
||||
| intro : p → q → and
|
||||
inductive And (p q : Prop) : Prop
|
||||
| intro : p → q → And p q
|
||||
|
||||
inductive or (p q : Prop) : Prop
|
||||
| inl : p → or
|
||||
| inr : q → or
|
||||
inductive Or (p q : Prop) : Prop
|
||||
| inl : p → Or p q
|
||||
| inr : q → Or p q
|
||||
|
||||
inductive Exists (α : Type u) (p : α → Prop) : Prop
|
||||
| intro : ∀ x : α, p x → Exists
|
||||
| intro : ∀ x : α, p x → Exists α p
|
||||
|
||||
inductive subtype (α : Type u) (p : α → Prop) : Type u
|
||||
| intro : ∀ x : α, p x → subtype
|
||||
inductive Subtype (α : Type u) (p : α → Prop) : Type u
|
||||
| intro : ∀ x : α, p x → Subtype α p
|
||||
|
||||
inductive nat : Type
|
||||
| zero : nat
|
||||
| succ : nat → nat
|
||||
inductive Nat : Type
|
||||
| zero : Nat
|
||||
| succ : Nat → Nat
|
||||
|
||||
inductive list (α : Type u)
|
||||
| nil : list
|
||||
| cons : α → list → list
|
||||
inductive List (α : Type u)
|
||||
| nil : List α
|
||||
| cons : α → List α → List α
|
||||
|
||||
-- full binary tree with nodes and leaves labeled from α
|
||||
inductive bintree (α : Type u)
|
||||
| leaf : α → bintree
|
||||
| node : bintree → α → bintree → bintree
|
||||
inductive BinTree (α : Type u)
|
||||
| leaf : α → BinTree α
|
||||
| node : BinTree α → α → BinTree α → BinTree α
|
||||
|
||||
-- every internal node has subtrees indexed by Nat
|
||||
inductive cbt (α : Type u)
|
||||
| leaf : α → cbt
|
||||
| node : (Nat → cbt) → cbt
|
||||
inductive CBT (α : Type u)
|
||||
| leaf : α → CBT α
|
||||
| node : (Nat → CBT α) → CBT α
|
||||
-- END
|
||||
end hide
|
||||
|
||||
Note that in the syntax of the inductive definition ``foo``, the context ``(a : α)`` is left implicit. In other words, constructors and recursive arguments are written as though they have return type ``foo`` rather than ``foo a``.
|
||||
Note that in the syntax of the inductive definition ``Foo``, the context ``(a : α)`` is left implicit. In other words, constructors and recursive arguments are written as though they have return type ``Foo`` rather than ``Foo a``.
|
||||
|
||||
Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[pattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler).
|
||||
Elements of the context ``(a : α)`` can be marked implicit as described in [Implicit Arguments](#implicit.md#implicit_arguments). These annotations bear only on the type former, ``Foo``. Lean uses a heuristic to determine which arguments to the constructors should be marked implicit, namely, an argument is marked implicit if it can be inferred from the type of a subsequent argument. If the annotation ``{}`` appears after the constructor, a argument is marked implicit if it can be inferred from the type of a subsequent argument *or the return type*. For example, it is useful to let ``nil`` denote the empty list of any type, since the type can usually be inferred in the context in which it appears. These heuristics are imperfect, and you may sometimes wish to define your own constructors in terms of the default ones. In that case, use the ``[matchPattern]`` [attribute](TODO: missing link) to ensure that these will be used appropriately by the [Equation Compiler](#the-equation-compiler).
|
||||
|
||||
There are restrictions on the universe ``u`` in the return type ``Sort u`` of the type former. There are also restrictions on the universe ``u`` in the return type ``Sort u`` of the motive of the eliminator. These will be discussed in the next section in the more general setting of inductive families.
|
||||
|
||||
|
|
@ -236,69 +236,69 @@ Lean allows some additional syntactic conveniences. You can omit the return type
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
namespace Hide
|
||||
universe u
|
||||
|
||||
-- BEGIN
|
||||
inductive weekday
|
||||
inductive Weekday
|
||||
| sunday | monday | tuesday | wednesday
|
||||
| thursday | friday | saturday
|
||||
|
||||
inductive nat
|
||||
inductive Nat
|
||||
| zero
|
||||
| succ (n : nat) : nat
|
||||
| succ (n : Nat) : Nat
|
||||
|
||||
inductive list (α : Type u)
|
||||
| nil {} : list
|
||||
| cons (a : α) (l : list) : list
|
||||
inductive List (α : Type u)
|
||||
| nil : List α
|
||||
| cons (a : α) (l : List α) : List α
|
||||
|
||||
@[pattern]
|
||||
def list.nil' (α : Type u) : list α := list.nil
|
||||
@[matchPattern]
|
||||
def List.nil' (α : Type u) : List α := List.nil
|
||||
|
||||
def length {α : Type u} : list α → Nat
|
||||
| (list.nil' .(α)) := 0
|
||||
| (list.cons a l) := 1 + length l
|
||||
def length {α : Type u} : List α → Nat
|
||||
| (List.nil' _) => 0
|
||||
| (List.cons a l) => 1 + length l
|
||||
-- END
|
||||
|
||||
end hide
|
||||
end Hide
|
||||
|
||||
The type former, constructors, and eliminator are all part of Lean's axiomatic foundation, which is to say, they are part of the trusted kernel. In addition to these axiomatically declared constants, Lean automatically defines some additional objects in terms of these, and adds them to the environment. These include the following:
|
||||
|
||||
- ``foo.rec_on`` : a variant of the eliminator, in which the major premise comes first
|
||||
- ``foo.cases_on`` : a restricted version of the eliminator which omits any recursive calls
|
||||
- ``foo.no_confusion_type``, ``foo.no_confusion`` : functions which witness the fact that the inductive type is freely generated, i.e. that the constructors are injective and that distinct constructors produce distinct objects
|
||||
- ``foo.below``, ``foo.ibelow`` : functions used by the equation compiler to implement structural recursion
|
||||
- ``foo.sizeof`` : a measure which can be used for well-founded recursion
|
||||
- ``Foo.recOn`` : a variant of the eliminator, in which the major premise comes first
|
||||
- ``Foo.casesOn`` : a restricted version of the eliminator which omits any recursive calls
|
||||
- ``Foo.noConfusionType``, ``Foo.noConfusion`` : functions which witness the fact that the inductive type is freely generated, i.e. that the constructors are injective and that distinct constructors produce distinct objects
|
||||
- ``Foo.below``, ``Foo.ibelow`` : functions used by the equation compiler to implement structural recursion
|
||||
- ``instance : SizeOf Foo`` : a measure which can be used for well-founded recursion
|
||||
|
||||
Note that it is common to put definitions and theorems related to a datatype ``foo`` in a namespace of the same name. This makes it possible to use projection notation described in [Structures](struct.md#structures) and [Namespaces](namespaces.md#namespaces).
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
namespace Hide
|
||||
universe u
|
||||
|
||||
-- BEGIN
|
||||
inductive nat
|
||||
inductive Nat
|
||||
| zero
|
||||
| succ (n : nat) : nat
|
||||
| succ (n : Nat) : Nat
|
||||
|
||||
#check nat
|
||||
#check nat.rec
|
||||
#check nat.zero
|
||||
#check nat.succ
|
||||
#check Nat
|
||||
#check @Nat.rec
|
||||
#check Nat.zero
|
||||
#check Nat.succ
|
||||
|
||||
#check nat.rec_on
|
||||
#check nat.cases_on
|
||||
#check nat.no_confusion_type
|
||||
#check @nat.no_confusion
|
||||
#check nat.brec_on
|
||||
#check nat.below
|
||||
#check nat.ibelow
|
||||
#check nat.sizeof
|
||||
#check @Nat.recOn
|
||||
#check @Nat.casesOn
|
||||
#check @Nat.noConfusionType
|
||||
#check @Nat.noConfusion
|
||||
#check @Nat.brecOn
|
||||
#check Nat.below
|
||||
#check Nat.ibelow
|
||||
#check Nat._sizeOf_1
|
||||
|
||||
-- END
|
||||
|
||||
end hide
|
||||
end Hide
|
||||
|
||||
.. _inductive_families:
|
||||
|
||||
|
|
@ -309,39 +309,39 @@ In fact, Lean implements a slight generalization of the inductive types describe
|
|||
|
||||
.. code-block:: text
|
||||
|
||||
inductive foo (a : α) : Π (c : γ), Sort u
|
||||
| constructor₁ : Π (b : β₁), foo t₁
|
||||
| constructor₂ : Π (b : β₂), foo t₂
|
||||
inductive Foo (a : α) : Π (c : γ), Sort u
|
||||
| constructor₁ : Π (b : β₁), Foo t₁
|
||||
| constructor₂ : Π (b : β₂), Foo t₂
|
||||
...
|
||||
| constructorₙ : Π (b : βₙ), foo tₙ
|
||||
| constructorₙ : Π (b : βₙ), Foo tₙ
|
||||
|
||||
Here ``(a : α)`` is a context, ``(c : γ)`` is a telescope in context ``(a : α)``, each ``(b : βᵢ)`` is a telescope in the context ``(a : α)`` together with ``(foo : Π (c : γ), Sort u)`` subject to the constraints below, and each ``tᵢ`` is a tuple of terms in the context ``(a : α) (b : βᵢ)`` having the types ``γ``. Instead of defining a single inductive type ``foo a``, we are now defining a family of types ``foo a c`` indexed by elements ``c : γ``. Each constructor, ``constructorᵢ``, places its result in the type ``foo a tᵢ``, the member of the family with index ``tᵢ``.
|
||||
Here ``(a : α)`` is a context, ``(c : γ)`` is a telescope in context ``(a : α)``, each ``(b : βᵢ)`` is a telescope in the context ``(a : α)`` together with ``(Foo : Π (c : γ), Sort u)`` subject to the constraints below, and each ``tᵢ`` is a tuple of terms in the context ``(a : α) (b : βᵢ)`` having the types ``γ``. Instead of defining a single inductive type ``Foo a``, we are now defining a family of types ``Foo a c`` indexed by elements ``c : γ``. Each constructor, ``constructorᵢ``, places its result in the type ``Foo a tᵢ``, the member of the family with index ``tᵢ``.
|
||||
|
||||
The modifications to the scheme in the previous section are straightforward. Suppose the telescope ``(b : βᵢ)`` is ``(b₁ : βᵢ₁) ... (bᵤ : βᵢᵤ)``.
|
||||
|
||||
- As before, an argument ``(bⱼ : βᵢⱼ)`` is *nonrecursive* if ``βᵢⱼ`` does not refer to ``foo,`` the inductive type being defined. In that case, ``βᵢⱼ`` can be any type, so long as it does not refer to any nonrecursive arguments.
|
||||
- As before, an argument ``(bⱼ : βᵢⱼ)`` is *nonrecursive* if ``βᵢⱼ`` does not refer to ``Foo,`` the inductive type being defined. In that case, ``βᵢⱼ`` can be any type, so long as it does not refer to any nonrecursive arguments.
|
||||
|
||||
- An argument ``(bⱼ : βᵢⱼ)`` is *recursive* if ``βᵢⱼ`` is of the form ``Π (d : δ), foo s`` where ``(d : δ)`` is a telescope which does not refer to ``foo`` or any nonrecursive arguments and ``s`` is a tuple of terms in context ``(a : α)`` and the previous nonrecursive ``bⱼ``'s with types ``γ``.
|
||||
- An argument ``(bⱼ : βᵢⱼ)`` is *recursive* if ``βᵢⱼ`` is of the form ``Π (d : δ), Foo s`` where ``(d : δ)`` is a telescope which does not refer to ``Foo`` or any nonrecursive arguments and ``s`` is a tuple of terms in context ``(a : α)`` and the previous nonrecursive ``bⱼ``'s with types ``γ``.
|
||||
|
||||
The declaration of the type ``foo`` as above results in the addition of the following constants to the environment:
|
||||
The declaration of the type ``Foo`` as above results in the addition of the following constants to the environment:
|
||||
|
||||
- the *type former* ``foo : Π (a : α) (c : γ), Sort u``
|
||||
- for each ``i``, the *constructor* ``foo.constructorᵢ : Π (a : α) (b : βᵢ), foo a tᵢ``
|
||||
- the *eliminator* ``foo.rec``, which takes arguments
|
||||
- the *type former* ``Foo : Π (a : α) (c : γ), Sort u``
|
||||
- for each ``i``, the *constructor* ``Foo.constructorᵢ : Π (a : α) (b : βᵢ), Foo a tᵢ``
|
||||
- the *eliminator* ``Foo.rec``, which takes arguments
|
||||
|
||||
+ ``(a : α)`` (the parameters)
|
||||
+ ``{C : Π (c : γ), foo a c → Type u}`` (the motive of the elimination)
|
||||
+ ``{C : Π (c : γ), Foo a c → Type u}`` (the motive of the elimination)
|
||||
+ for each ``i``, the minor premise corresponding to ``constructorᵢ``
|
||||
+ ``(x : foo a)`` (the major premise)
|
||||
+ ``(x : Foo a)`` (the major premise)
|
||||
|
||||
and returns an element of ``C x``. Here, The ith minor premise is a function which takes
|
||||
|
||||
+ ``(b : βᵢ)`` (the arguments to the constructor)
|
||||
+ an argument of type ``Π (d : δ), C s (bⱼ d)`` corresponding to each recursive argument ``(bⱼ : βᵢⱼ)``, where ``βᵢⱼ`` is of the form ``Π (d : δ), foo s``
|
||||
+ an argument of type ``Π (d : δ), C s (bⱼ d)`` corresponding to each recursive argument ``(bⱼ : βᵢⱼ)``, where ``βᵢⱼ`` is of the form ``Π (d : δ), Foo s``
|
||||
|
||||
and returns an element of ``C tᵢ (constructorᵢ a b)``.
|
||||
|
||||
Suppose we set ``F := foo.rec a C f₁ ... fₙ``. Then for each constructor, we have the definitional reduction, as before:
|
||||
Suppose we set ``F := Foo.rec a C f₁ ... fₙ``. Then for each constructor, we have the definitional reduction, as before:
|
||||
|
||||
.. code-block :: text
|
||||
|
||||
|
|
@ -353,24 +353,24 @@ The following are examples of inductive families.
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
namespace Hide
|
||||
universe u
|
||||
|
||||
-- BEGIN
|
||||
inductive vector (α : Type u) : Nat → Type u
|
||||
| nil : vector 0
|
||||
| succ : Π n, vector n → vector (n + 1)
|
||||
inductive Vector (α : Type u) : Nat → Type u
|
||||
| nil : Vector 0
|
||||
| succ : Π n, Vector n → Vector (n + 1)
|
||||
|
||||
-- 'is_prod s n' means n is a product of elements of s
|
||||
inductive is_prod (s : set Nat) : Nat → Prop
|
||||
| base : ∀ n ∈ s, is_prod n
|
||||
| step : ∀ m n, is_prod m → is_prod n → is_prod (m * n)
|
||||
-- 'IsProd s n' means n is a product of elements of s
|
||||
inductive IsProd (s : Set Nat) : Nat → Prop
|
||||
| base : ∀ n ∈ s, IsProd n
|
||||
| step : ∀ m n, IsProd m → IsProd n → IsProd (m * n)
|
||||
|
||||
inductive eq {α : Sort u} (a : α) : α → Prop
|
||||
| refl : eq a
|
||||
inductive Eq {α : Sort u} (a : α) : α → Prop
|
||||
| refl : Eq a
|
||||
-- END
|
||||
|
||||
end hide
|
||||
end Hide
|
||||
|
||||
We can now describe the constraints on the return type of the type former, ``Sort u``. We can always take ``u`` to be ``0``, in which case we are defining an inductive family of propositions. If ``u`` is nonzero, however, it must satisfy the following constraint: for each type ``βᵢⱼ : Sort v`` occurring in the constructors, we must have ``u ≥ v``. In the set-theoretic interpretation, this ensures that the universe in which the resulting type resides is large enough to contain the inductively generated family, given the number of distinctly-labeled constructors. The restriction does not hold for inductively defined propositions, since these contain no data.
|
||||
|
||||
|
|
@ -387,42 +387,47 @@ The first generalization allows for multiple inductive types to be defined simul
|
|||
|
||||
.. code-block:: text
|
||||
|
||||
mutual inductive foo, bar (a : α)
|
||||
with foo : Π (c : γ), Sort u
|
||||
| constructor₁₁ : Π (b : β₁₁), foo t₁₁
|
||||
| constructor₁₂ : Π (b : β₁₂), foo t₁₂
|
||||
mutual
|
||||
|
||||
inductive Foo (a : α) : Π (c : γ₁), Sort u
|
||||
| constructor₁₁ : Π (b : β₁₁), Foo a t₁₁
|
||||
| constructor₁₂ : Π (b : β₁₂), Foo a t₁₂
|
||||
...
|
||||
| constructor₁ₙ : Π (b : β₁ₙ), foo t₁ₙ
|
||||
with bar :
|
||||
| constructor₂₁ : Π (b : β₂₁), bar t₂₁
|
||||
| constructor₂₂ : Π (b : β₂₂), bar t₂₂
|
||||
| constructor₁ₙ : Π (b : β₁ₙ), Foo a t₁ₙ
|
||||
|
||||
inductive Bar (a : α) : Π (c : γ₂), Sort u
|
||||
| constructor₂₁ : Π (b : β₂₁), Bar a t₂₁
|
||||
| constructor₂₂ : Π (b : β₂₂), Bar a t₂₂
|
||||
...
|
||||
| constructor₂ₘ : Π (b : β₂ₘ), bar t₂ₘ
|
||||
| constructor₂ₘ : Π (b : β₂ₘ), Bar a t₂ₘ
|
||||
|
||||
Here the syntax is shown for defining two inductive families, ``foo`` and ``bar``, but any number is allowed. The restrictions are almost the same as for ordinary inductive families. For example, each ``(b : βᵢⱼ)`` is a telescope relative to the context ``(a : α)``. The difference is that the constructors can now have recursive arguments whose return types are any of the inductive families currently being defined, in this case ``foo`` and ``bar``. Note that all of the inductive definitions share the same parameters ``(a : α)``, though they may have different indices.
|
||||
end
|
||||
|
||||
A mutual inductive definition is compiled down to an ordinary inductive definition using an extra finite-valued index to distinguish the components. The details of the internal construction are meant to be hidden from most users. Lean defines the expected type formers ``foo`` and ``bar`` and constructors ``constructorᵢⱼ`` from the internal inductive definition. There is no straightforward elimination principle, however. Instead, Lean defines an appropriate ``sizeof`` measure, meant for use with well-founded recursion, with the property that the recursive arguments to a constructor are smaller than the constructed value.
|
||||
Here the syntax is shown for defining two inductive families, ``Foo`` and ``Bar``, but any number is allowed. The restrictions are almost the same as for ordinary inductive families. For example, each ``(b : βᵢⱼ)`` is a telescope relative to the context ``(a : α)``. The difference is that the constructors can now have recursive arguments whose return types are any of the inductive families currently being defined, in this case ``Foo`` and ``Bar``. Note that all of the inductive definitions share the same parameters ``(a : α)``, though they may have different indices.
|
||||
|
||||
The second generalization relaxes the restriction that in the recursive definition of ``foo``, ``foo`` can only occur strictly positively in the type of any of its recursive arguments. Specifically, in a nested inductive definition, ``foo`` can appear as an argument to another inductive type constructor, so long as the corresponding parameter occurs strictly positively in the constructors for *that* inductive type. This process can be iterated, so that additional type constructors can be applied to those, and so on.
|
||||
A mutual inductive definition is compiled down to an ordinary inductive definition using an extra finite-valued index to distinguish the components. The details of the internal construction are meant to be hidden from most users. Lean defines the expected type formers ``Foo`` and ``Bar`` and constructors ``constructorᵢⱼ`` from the internal inductive definition. There is no straightforward elimination principle, however. Instead, Lean defines an appropriate ``sizeOf`` measure, meant for use with well-founded recursion, with the property that the recursive arguments to a constructor are smaller than the constructed value.
|
||||
|
||||
A nested inductive definition is compiled down to an ordinary inductive definition using a mutual inductive definition to define copies of all the nested types simultaneously. Lean then constructs isomorphisms between the mutually defined nested types and their independently defined counterparts. Once again, the internal details are not meant to be manipulated by users. Rather, the type former and constructors are made available and work as expected, while an appropriate ``sizeof`` measure is generated for use with well-founded recursion.
|
||||
The second generalization relaxes the restriction that in the recursive definition of ``Foo``, ``Foo`` can only occur strictly positively in the type of any of its recursive arguments. Specifically, in a nested inductive definition, ``Foo`` can appear as an argument to another inductive type constructor, so long as the corresponding parameter occurs strictly positively in the constructors for *that* inductive type. This process can be iterated, so that additional type constructors can be applied to those, and so on.
|
||||
|
||||
A nested inductive definition is compiled down to an ordinary inductive definition using a mutual inductive definition to define copies of all the nested types simultaneously. Lean then constructs isomorphisms between the mutually defined nested types and their independently defined counterparts. Once again, the internal details are not meant to be manipulated by users. Rather, the type former and constructors are made available and work as expected, while an appropriate ``sizeOf`` measure is generated for use with well-founded recursion.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
universe u
|
||||
-- BEGIN
|
||||
mutual inductive even, odd
|
||||
with even : Nat → Prop
|
||||
| even_zero : even 0
|
||||
| even_succ : ∀ n, odd n → even (n + 1)
|
||||
with odd : Nat → Prop
|
||||
| odd_succ : ∀ n, even n → odd (n + 1)
|
||||
mutual
|
||||
inductive Even : Nat → Prop
|
||||
| even_zero : Even 0
|
||||
| even_succ : ∀ n, Odd n → Even (n + 1)
|
||||
inductive Odd : Nat → Prop
|
||||
| odd_succ : ∀ n, Even n → Odd (n + 1)
|
||||
end
|
||||
|
||||
inductive tree (α : Type u)
|
||||
| mk : α → list tree → tree
|
||||
inductive Tree (α : Type u)
|
||||
| mk : α → List (Tree α) → Tree α
|
||||
|
||||
inductive double_tree (α : Type u)
|
||||
| mk : α → list double_tree × list double_tree → double_tree
|
||||
inductive DoubleTree (α : Type u)
|
||||
| mk : α → List (DoubleTree α) × List (DoubleTree α) → DoubleTree α
|
||||
-- END
|
||||
|
||||
.. _the_equation_compiler:
|
||||
|
|
@ -435,9 +440,9 @@ The equation compiler takes an equational description of a function or proof and
|
|||
.. code-block:: text
|
||||
|
||||
def foo (a : α) : Π (b : β), γ
|
||||
| [patterns₁] := t₁
|
||||
| [patterns₁] => t₁
|
||||
...
|
||||
| [patternsₙ] := tₙ
|
||||
| [patternsₙ] => tₙ
|
||||
|
||||
Here ``(a : α)`` is a telescope, ``(b : β)`` is a telescope in the context ``(a : α)``, and ``γ`` is an expression in the context ``(a : α) (b : β)`` denoting a ``Type`` or a ``Prop``.
|
||||
|
||||
|
|
@ -450,78 +455,78 @@ Each ``patternsᵢ`` is a sequence of patterns of the same length as ``(b : β)`
|
|||
|
||||
In the last case, the pattern must be enclosed in parentheses.
|
||||
|
||||
Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``:=``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see [Rewrite](tactics.md#rewrite) and _[TODO: where is simplifier tactic documented?]_. If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error.
|
||||
Each term ``tᵢ`` is an expression in the context ``(a : α)`` together with the variables introduced on the left-hand side of the token ``=>``. The term ``tᵢ`` can also include recursive calls to ``foo``, as described below. The equation compiler does case splitting on the variables ``(b : β)`` as necessary to match the patterns, and defines ``foo`` so that it has the value ``tᵢ`` in each of the cases. In ideal circumstances (see below), the equations hold definitionally. Whether they hold definitionally or only propositionally, the equation compiler proves the relevant equations and assigns them internal names. They are accessible by the ``rewrite`` and ``simp`` tactics under the name ``foo`` (see [Rewrite](tactics.md#rewrite) and _[TODO: where is simplifier tactic documented?]_. If some of the patterns overlap, the equation compiler interprets the definition so that the first matching pattern applies in each case. Thus, if the last pattern is a variable, it covers all the remaining cases. If the patterns that are presented do not cover all possible cases, the equation compiler raises an error.
|
||||
|
||||
When identifiers are marked with the ``[pattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``nat.succ n`` and ``nat.zero`` in patterns.
|
||||
When identifiers are marked with the ``[matchPattern]`` attribute, the equation compiler unfolds them in the hopes of exposing a constructor. For example, this makes it possible to write ``n+1`` and ``0`` instead of ``Nat.succ n`` and ``Nat.zero`` in patterns.
|
||||
|
||||
For a nonrecursive definition involving case splits, the defining equations will hold definitionally. With inductive types like ``char``, ``string``, and ``fin n``, a case split would produce definitions with an inordinate number of cases. To avoid this, the equation compiler uses ``if ... then ... else`` instead of ``cases_on`` when defining the function. In this case, the defining equations hold definitionally as well.
|
||||
For a nonrecursive definition involving case splits, the defining equations will hold definitionally. With inductive types like ``Char``, ``String``, and ``Fin n``, a case split would produce definitions with an inordinate number of cases. To avoid this, the equation compiler uses ``if ... then ... else`` instead of ``casesOn`` when defining the function. In this case, the defining equations hold definitionally as well.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
open nat
|
||||
open Nat
|
||||
|
||||
def sub2 : Nat → Nat
|
||||
| zero := 0
|
||||
| (succ zero) := 0
|
||||
| (succ (succ a)) := a
|
||||
| zero => 0
|
||||
| succ zero => 0
|
||||
| succ (succ a) => a
|
||||
|
||||
def bar : Nat → list Nat → bool → Nat
|
||||
| 0 _ ff := 0
|
||||
| 0 (b :: _) _ := b
|
||||
| 0 [] tt := 7
|
||||
| (a+1) [] ff := a
|
||||
| (a+1) [] tt := a + 1
|
||||
| (a+1) (b :: _) _ := a + b
|
||||
def bar : Nat → List Nat → Bool → Nat
|
||||
| 0, _, false => 0
|
||||
| 0, b :: _, _ => b
|
||||
| 0, [], true => 7
|
||||
| a+1, [], false => a
|
||||
| a+1, [], true => a + 1
|
||||
| a+1, b :: _, _ => a + b
|
||||
|
||||
def baz : char → Nat
|
||||
| 'A' := 1
|
||||
| 'B' := 2
|
||||
| _ := 3
|
||||
def baz : Char → Nat
|
||||
| 'A' => 1
|
||||
| 'B' => 2
|
||||
| _ => 3
|
||||
|
||||
If any of the terms ``tᵢ`` in the template above contain a recursive call to ``foo``, the equation compiler tries to interpret the definition as a structural recursion. In order for that to succeed, the recursive arguments must be subterms of the corresponding arguments on the left-hand side. The function is then defined using a *course of values* recursion, using automatically generated functions ``below`` and ``brec`` in the namespace corresponding to the inductive type of the recursive argument. In this case the defining equations hold definitionally, possibly with additional case splits.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
namespace Hide
|
||||
|
||||
-- BEGIN
|
||||
def fib : nat → nat
|
||||
| 0 := 1
|
||||
| 1 := 1
|
||||
| (n+2) := fib (n+1) + fib n
|
||||
def fib : Nat → Nat
|
||||
| 0 => 1
|
||||
| 1 => 1
|
||||
| (n+2) => fib (n+1) + fib n
|
||||
|
||||
def append {α : Type} : list α → list α → list α
|
||||
| [] l := l
|
||||
| (h::t) l := h :: append t l
|
||||
def append {α : Type} : List α → List α → List α
|
||||
| [], l => l
|
||||
| h::t, l => h :: append t l
|
||||
|
||||
example : append [(1 : Nat), 2, 3] [4, 5] = [1, 2, 3, 4, 5] := rfl
|
||||
example : append [(1 : Nat), 2, 3] [4, 5] = [1, 2, 3, 4, 5] => rfl
|
||||
-- END
|
||||
|
||||
end hide
|
||||
end Hide
|
||||
|
||||
If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``has_sizeof`` for the type of each argument, and then show that each recursive call is decreasing under the lexicographic order of the arguments with respect to ``sizeof`` measure. If it fails, the error message provides information as to the goal that Lean tried to prove. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition. In this case of well-founded recursion, the defining equations hold only propositionally, and can be accessed using ``simp`` and ``rewrite`` with the name ``foo``.
|
||||
If structural recursion fails, the equation compiler falls back on well-founded recursion. It tries to infer an instance of ``SizeOf`` for the type of each argument, and then show that each recursive call is decreasing under the lexicographic order of the arguments with respect to ``sizeOf`` measure. If it fails, the error message provides information as to the goal that Lean tried to prove. Lean uses information in the local context, so you can often provide the relevant proof manually using ``have`` in the body of the definition. In this case of well-founded recursion, the defining equations hold only propositionally, and can be accessed using ``simp`` and ``rewrite`` with the name ``foo``.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
namespace hide
|
||||
open nat
|
||||
namespace Hide
|
||||
open Nat
|
||||
|
||||
-- BEGIN
|
||||
def div : Nat → Nat → Nat
|
||||
| x y :=
|
||||
| x, y =>
|
||||
if h : 0 < y ∧ y ≤ x then
|
||||
have x - y < x,
|
||||
from sub_lt (lt_of_lt_of_le h.left h.right) h.left,
|
||||
have : x - y < x :=
|
||||
sub_lt (Nat.lt_of_lt_of_le h.left h.right) h.left
|
||||
div (x - y) y + 1
|
||||
else
|
||||
0
|
||||
|
||||
example (x y : Nat) :
|
||||
div x y = if 0 < y ∧ y ≤ x then div (x - y) y + 1 else 0 :=
|
||||
by rw [div]
|
||||
by rw [div]; rfl
|
||||
-- END
|
||||
|
||||
end hide
|
||||
end Hide
|
||||
|
||||
Note that recursive definitions can in general require nested recursions, that is, recursion on different arguments of ``foo`` in the template above. The equation compiler handles this by abstracting later arguments, and recursively defining higher-order functions to meet the specification.
|
||||
|
||||
|
|
@ -529,13 +534,14 @@ The equation compiler also allows mutual recursive definitions, with a syntax si
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
mutual def even, odd
|
||||
with even : Nat → bool
|
||||
| 0 := tt
|
||||
| (a+1) := odd a
|
||||
with odd : Nat → bool
|
||||
| 0 := ff
|
||||
| (a+1) := even a
|
||||
mutual
|
||||
def even : Nat → Bool
|
||||
| 0 => true
|
||||
| a+1 => odd a
|
||||
def odd : Nat → Bool
|
||||
| 0 => false
|
||||
| a+1 => even a
|
||||
end
|
||||
|
||||
example (a : Nat) : even (a + 1) = odd a :=
|
||||
by simp [even]
|
||||
|
|
@ -547,36 +553,39 @@ Well-founded recursion is especially useful with [Mutual and Nested Inductive De
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
mutual inductive even, odd
|
||||
with even : Nat → Prop
|
||||
| even_zero : even 0
|
||||
| even_succ : ∀ n, odd n → even (n + 1)
|
||||
with odd : Nat → Prop
|
||||
| odd_succ : ∀ n, even n → odd (n + 1)
|
||||
mutual
|
||||
inductive Even : Nat → Prop
|
||||
| even_zero : Even 0
|
||||
| even_succ : ∀ n, Odd n → Even (n + 1)
|
||||
inductive Odd : Nat → Prop
|
||||
| odd_succ : ∀ n, Even n → Odd (n + 1)
|
||||
end
|
||||
|
||||
open even odd
|
||||
open Even Odd
|
||||
|
||||
theorem not_odd_zero : ¬ odd 0.
|
||||
theorem not_odd_zero : ¬ Odd 0 := fun x => nomatch x
|
||||
|
||||
mutual theorem even_of_odd_succ, odd_of_even_succ
|
||||
with even_of_odd_succ : ∀ n, odd (n + 1) → even n
|
||||
| _ (odd_succ n h) := h
|
||||
with odd_of_even_succ : ∀ n, even (n + 1) → odd n
|
||||
| _ (even_succ n h) := h
|
||||
mutual
|
||||
theorem even_of_odd_succ : ∀ n, Odd (n + 1) → Even n
|
||||
| _, odd_succ n h => h
|
||||
theorem odd_of_even_succ : ∀ n, Even (n + 1) → Odd n
|
||||
| _, even_succ n h => h
|
||||
end
|
||||
|
||||
inductive term
|
||||
| const : string → term
|
||||
| app : string → list term → term
|
||||
inductive Term
|
||||
| const : String → Term
|
||||
| app : String → List Term → Term
|
||||
|
||||
open term
|
||||
open Term
|
||||
|
||||
mutual def num_consts, num_consts_lst
|
||||
with num_consts : term → nat
|
||||
| (term.const n) := 1
|
||||
| (term.app n ts) := num_consts_lst ts
|
||||
with num_consts_lst : list term → nat
|
||||
| [] := 0
|
||||
| (t::ts) := num_consts t + num_consts_lst ts
|
||||
mutual
|
||||
def num_consts : Term → Nat
|
||||
| .const n => 1
|
||||
| .app n ts => num_consts_lst ts
|
||||
def num_consts_lst : List Term → Nat
|
||||
| [] => 0
|
||||
| t::ts => num_consts t + num_consts_lst ts
|
||||
end
|
||||
|
||||
The case where patterns are matched against an argument whose type is an inductive family is known as *dependent pattern matching*. This is more complicated, because the type of the function being defined can impose constraints on the patterns that are matched. In this case, the equation compiler will detect inconsistent cases and rule them out.
|
||||
|
||||
|
|
@ -584,52 +593,24 @@ The case where patterns are matched against an argument whose type is an inducti
|
|||
|
||||
universe u
|
||||
|
||||
inductive vector (α : Type u) : Nat → Type u
|
||||
| nil {} : vector 0
|
||||
| cons : Π {n}, α → vector n → vector (n+1)
|
||||
inductive Vector (α : Type u) : Nat → Type u
|
||||
| nil : Vector α 0
|
||||
| cons : α → Vector α n → Vector α (n+1)
|
||||
|
||||
namespace vector
|
||||
namespace Vector
|
||||
|
||||
def head {α : Type} : Π {n}, vector α (n+1) → α
|
||||
| n (cons h t) := h
|
||||
def head {α : Type} : Vector α (n+1) → α
|
||||
| cons h t => h
|
||||
|
||||
def tail {α : Type} : Π {n}, vector α (n+1) → vector α n
|
||||
| n (cons h t) := t
|
||||
def tail {α : Type} : Vector α (n+1) → Vector α n
|
||||
| cons h t => t
|
||||
|
||||
def map {α β γ : Type} (f : α → β → γ) :
|
||||
Π {n}, vector α n → vector β n → vector γ n
|
||||
| 0 nil nil := nil
|
||||
| (n+1) (cons a va) (cons b vb) := cons (f a b) (map va vb)
|
||||
∀ {n}, Vector α n → Vector β n → Vector γ n
|
||||
| 0, nil, nil => nil
|
||||
| n+1, cons a va, cons b vb => cons (f a b) (map f va vb)
|
||||
|
||||
end vector
|
||||
|
||||
An expression of the form ``.(t)`` in a pattern is known as an *inaccessible term*. It is not viewed as part of the pattern; rather, it is explicit information that is used by the elaborator and equation compiler when interpreting the definition. Inaccessible terms do not participate in pattern matching. They are sometimes needed for a pattern to make sense, for example, when a constructor depends on a parameter that is not a pattern-matching variable. In other cases, they can be used to inform the equation compiler that certain arguments do not require a case split, and they can be used to make a definition more readable.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
universe u
|
||||
|
||||
inductive vector (α : Type u) : Nat → Type u
|
||||
| nil {} : vector 0
|
||||
| cons : Π {n}, α → vector n → vector (n+1)
|
||||
|
||||
namespace vector
|
||||
|
||||
-- BEGIN
|
||||
variable {α : Type u}
|
||||
|
||||
def add [has_add α] :
|
||||
Π {n : Nat}, vector α n → vector α n → vector α n
|
||||
| ._ nil nil := nil
|
||||
| ._ (cons a v) (cons b w) := cons (a + b) (add v w)
|
||||
|
||||
def add' [has_add α] :
|
||||
Π {n : Nat}, vector α n → vector α n → vector α n
|
||||
| .(0) nil nil := nil
|
||||
| .(n+1) (@cons .(α) n a v) (cons b w) := cons (a + b) (add' v w)
|
||||
-- END
|
||||
|
||||
end vector
|
||||
end Vector
|
||||
|
||||
.. _match_expressions:
|
||||
|
||||
|
|
@ -641,9 +622,9 @@ Lean supports a ``match ... with ...`` construct similar to ones found in most f
|
|||
.. code-block:: text
|
||||
|
||||
match t₁, ..., tₙ with
|
||||
| p₁₁, ..., p₁ₙ := s₁
|
||||
| p₁₁, ..., p₁ₙ => s₁
|
||||
...
|
||||
| pₘ₁, ..., pₘₙ := sₘ
|
||||
| pₘ₁, ..., pₘₙ => sₘ
|
||||
|
||||
Here ``t₁, ..., tₙ`` are any terms in the context in which the expression appears, the expressions ``pᵢⱼ`` are patterns, and the terms ``sᵢ`` are expressions in the local context together with variables introduced by the patterns on the left-hand side. Each ``sᵢ`` should have the expected type of the entire ``match`` expression.
|
||||
|
||||
|
|
@ -651,29 +632,28 @@ Any ``match`` expression is interpreted using the equation compiler, which gener
|
|||
|
||||
.. code-block:: lean
|
||||
|
||||
def foo (n : Nat) (b c : bool) :=
|
||||
def foo (n : Nat) (b c : Bool) :=
|
||||
5 + match n - 5, b && c with
|
||||
| 0, tt := 0
|
||||
| m+1, tt := m + 7
|
||||
| 0, ff := 5
|
||||
| m+1, ff := m + 3
|
||||
end
|
||||
| 0, true => 0
|
||||
| m+1, true => m + 7
|
||||
| 0, false => 5
|
||||
| m+1, false => m + 3
|
||||
|
||||
When a ``match`` has only one line, the vertical bar may be left out. In that case, Lean provides alternative syntax with a destructuring ``let``, as well as a destructuring lambda abstraction. Thus the following definitions all have the same net effect.
|
||||
When a ``match`` has only one line, Lean provides alternative syntax with a destructuring ``let``, as well as a destructuring lambda abstraction. Thus the following definitions all have the same net effect.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
def bar₁ : Nat × Nat → Nat
|
||||
| (m, n) := m + n
|
||||
| (m, n) => m + n
|
||||
|
||||
def bar₂ (p : Nat × Nat) : Nat :=
|
||||
match p with (m, n) := m + n end
|
||||
match p with | (m, n) => m + n
|
||||
|
||||
def bar₃ : Nat × Nat → Nat :=
|
||||
fun ⟨m, n⟩ => m + n
|
||||
|
||||
def bar₄ (p : Nat × Nat) : Nat :=
|
||||
let ⟨m, n⟩ := p in m + n
|
||||
let ⟨m, n⟩ := p; m + n
|
||||
|
||||
Information about the term being matched can be preserved in each branch using the syntax `match h : t with`. For example, a user may want to match a term `ns ++ ms : List Nat`, while tracking the hypothesis `ns ++ ms = []` or `ns ++ ms= h :: t` in the respective match arm:
|
||||
|
||||
|
|
@ -698,114 +678,113 @@ The ``structure`` command in Lean is used to define an inductive data type with
|
|||
|
||||
.. code-block:: text
|
||||
|
||||
structure foo (a : α) extends bar, baz : Sort u :=
|
||||
structure Foo (a : α) extends Bar, Baz : Sort u :=
|
||||
constructor :: (field₁ : β₁) ... (fieldₙ : βₙ)
|
||||
|
||||
Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``foo,`` and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
|
||||
Here ``(a : α)`` is a telescope, that is, the parameters to the inductive definition. The name ``constructor`` followed by the double colon is optional; if it is not present, the name ``mk`` is used by default. The keyword ``extends`` followed by a list of previously defined structures is also optional; if it is present, an instance of each of these structures is included among the fields to ``Foo``, and the types ``βᵢ`` can refer to their fields as well. The output type, ``Sort u``, can be omitted, in which case Lean infers to smallest non-``Prop`` sort possible. Finally, ``(field₁ : β₁) ... (fieldₙ : βₙ)`` is a telescope relative to ``(a : α)`` and the fields in ``bar`` and ``baz``.
|
||||
|
||||
The declaration above is syntactic sugar for an inductive type declaration, and so results in the addition of the following constants to the environment:
|
||||
|
||||
- the type former : ``foo : Π (a : α), Sort u``
|
||||
- the type former : ``Foo : Π (a : α), Sort u``
|
||||
- the single constructor :
|
||||
|
||||
.. code-block:: text
|
||||
|
||||
foo.constructor : Π (a : α) (_to_foo : foo) (_to_bar : bar)
|
||||
(field₁ : β₁) ... (fieldₙ : βₙ), foo a
|
||||
Foo.constructor : Π (a : α) (toBar : Bar) (toBaz : Baz)
|
||||
(field₁ : β₁) ... (fieldₙ : βₙ), Foo a
|
||||
|
||||
- the eliminator ``foo.rec`` for the inductive type with that constructor
|
||||
- the eliminator ``Foo.rec`` for the inductive type with that constructor
|
||||
|
||||
In addition, Lean defines
|
||||
|
||||
- the projections : ``fieldᵢ : Π (a : α) (c : foo) : βᵢ`` for each ``i``
|
||||
- the projections : ``fieldᵢ : Π (a : α) (c : Foo) : βᵢ`` for each ``i``
|
||||
|
||||
where any other fields mentioned in ``βᵢ`` are replaced by the relevant projections from ``c``.
|
||||
|
||||
Given ``c : foo``, Lean offers the following convenient syntax for the projection ``foo.fieldᵢ c``:
|
||||
Given ``c : Foo``, Lean offers the following convenient syntax for the projection ``Foo.fieldᵢ c``:
|
||||
|
||||
- *anonymous projections* : ``c.fieldᵢ``
|
||||
- *numbered projections* : ``c.i``
|
||||
|
||||
These can be used in any situation where Lean can infer that the type of ``c`` is of the form ``foo a``. The convention for anonymous projections is extended to any function ``f`` defined in the namespace ``foo``, as described in [Namespaces](namespaces.md).
|
||||
These can be used in any situation where Lean can infer that the type of ``c`` is of the form ``Foo a``. The convention for anonymous projections is extended to any function ``f`` defined in the namespace ``Foo``, as described in [Namespaces](namespaces.md).
|
||||
|
||||
Similarly, Lean offers the following convenient syntax for constructing elements of ``foo``. They are equivalent to ``foo.constructor b₁ b₂ f₁ f₁ ... fₙ``, where ``b₁ : foo``, ``b₂ : bar``, and each ``fᵢ : βᵢ`` :
|
||||
Similarly, Lean offers the following convenient syntax for constructing elements of ``Foo``. They are equivalent to ``Foo.constructor b₁ b₂ f₁ f₁ ... fₙ``, where ``b₁ : Bar``, ``b₂ : Baz``, and each ``fᵢ : βᵢ`` :
|
||||
|
||||
- *anonymous constructor*: ``⟨ b₁, b₂, f₁, ..., fₙ ⟩``
|
||||
- *record notation*:
|
||||
|
||||
.. code-block:: text
|
||||
|
||||
{ foo . to_bar := b₁, to_baz := b₂, field₁ := f₁, ...,
|
||||
fieldₙ := fₙ }
|
||||
{ toBar := b₁, toBaz := b₂, field₁ := f₁, ...,
|
||||
fieldₙ := fₙ : Foo a }
|
||||
|
||||
The anonymous constructor can be used in any context where Lean can infer that the expression should have a type of the form ``foo a``. The unicode brackets are entered as ``\<`` and ``\>`` respectively. The tokens ``(|`` and ``|)`` are ascii equivalents.
|
||||
The anonymous constructor can be used in any context where Lean can infer that the expression should have a type of the form ``Foo a``. The unicode brackets are entered as ``\<`` and ``\>`` respectively.
|
||||
|
||||
When using record notation, you can omit the annotation ``foo .`` when Lean can infer that the expression should have a type of the form ``foo a``. You can replace either ``to_bar`` or ``to_baz`` by assignments to *their* fields as well, essentially acting as though the fields of ``bar`` and ``baz`` are simply imported into ``foo``. Finally, record notation also supports
|
||||
When using record notation, you can omit the annotation ``: Foo a`` when Lean can infer that the expression should have a type of the form ``Foo a``. You can replace either ``toBar`` or ``toBaz`` by assignments to *their* fields as well, essentially acting as though the fields of ``Bar`` and ``Baz`` are simply imported into ``Foo``. Finally, record notation also supports
|
||||
|
||||
- *record updates*: ``{ t with ... fieldᵢ := fᵢ ...}``
|
||||
|
||||
Here ``t`` is a term of type ``foo a`` for some ``a``. The notation instructs Lean to take values from ``t`` for any field assignment that is omitted from the list.
|
||||
Here ``t`` is a term of type ``Foo a`` for some ``a``. The notation instructs Lean to take values from ``t`` for any field assignment that is omitted from the list.
|
||||
|
||||
Lean also allows you to specify a default value for any field in a structure by writing ``(fieldᵢ : βᵢ := t)``. Here ``t`` specifies the value to use when the field ``fieldᵢ`` is left unspecified in an instance of record notation.
|
||||
|
||||
.. code-block:: lean
|
||||
|
||||
universes u v
|
||||
universe u v
|
||||
|
||||
structure vec (α : Type u) (n : Nat) :=
|
||||
(l : list α) (h : l.length = n)
|
||||
structure Vec (α : Type u) (n : Nat) :=
|
||||
(l : List α) (h : l.length = n)
|
||||
|
||||
structure foo (α : Type u) (β : Nat → Type v) : Type (max u v) :=
|
||||
structure Foo (α : Type u) (β : Nat → Type v) : Type (max u v) :=
|
||||
(a : α) (n : Nat) (b : β n)
|
||||
|
||||
structure bar :=
|
||||
structure Bar :=
|
||||
(c : Nat := 8) (d : Nat)
|
||||
|
||||
structure baz extends foo Nat (vec Nat), bar :=
|
||||
(v : vec Nat n)
|
||||
structure Baz extends Foo Nat (Vec Nat), Bar :=
|
||||
(v : Vec Nat n)
|
||||
|
||||
#check foo
|
||||
#check @foo.mk
|
||||
#check @foo.rec
|
||||
#check Foo
|
||||
#check @Foo.mk
|
||||
#check @Foo.rec
|
||||
|
||||
#check foo.a
|
||||
#check foo.n
|
||||
#check foo.b
|
||||
#check Foo.a
|
||||
#check Foo.n
|
||||
#check Foo.b
|
||||
|
||||
#check baz
|
||||
#check @baz.mk
|
||||
#check @baz.rec
|
||||
#check Baz
|
||||
#check @Baz.mk
|
||||
#check @Baz.rec
|
||||
|
||||
#check baz.to_foo
|
||||
#check baz.to_bar
|
||||
#check baz.v
|
||||
#check Baz.toFoo
|
||||
#check Baz.toBar
|
||||
#check Baz.v
|
||||
|
||||
def bzz := vec.mk [1, 2, 3] rfl
|
||||
def bzz := Vec.mk [1, 2, 3] rfl
|
||||
|
||||
#check vec.l bzz
|
||||
#check vec.h bzz
|
||||
#check Vec.l bzz
|
||||
#check Vec.h bzz
|
||||
#check bzz.l
|
||||
#check bzz.h
|
||||
#check bzz.1
|
||||
#check bzz.2
|
||||
|
||||
example : vec Nat 3 := vec.mk [1, 2, 3] rfl
|
||||
example : vec Nat 3 := ⟨[1, 2, 3], rfl⟩
|
||||
example : vec Nat 3 := (| [1, 2, 3], rfl |)
|
||||
example : vec Nat 3 := { vec . l := [1, 2, 3], h := rfl }
|
||||
example : vec Nat 3 := { l := [1, 2, 3], h := rfl }
|
||||
example : Vec Nat 3 := Vec.mk [1, 2, 3] rfl
|
||||
example : Vec Nat 3 := ⟨[1, 2, 3], rfl⟩
|
||||
example : Vec Nat 3 := { l := [1, 2, 3], h := rfl : Vec Nat 3 }
|
||||
example : Vec Nat 3 := { l := [1, 2, 3], h := rfl }
|
||||
|
||||
example : foo Nat (vec Nat) := ⟨1, 3, bzz⟩
|
||||
example : Foo Nat (Vec Nat) := ⟨1, 3, bzz⟩
|
||||
|
||||
example : baz := ⟨⟨1, 3, bzz⟩, ⟨5, 7⟩, bzz⟩
|
||||
example : baz := { a := 1, n := 3, b := bzz, c := 5, d := 7, v := bzz}
|
||||
def fzz : foo Nat (vec Nat) := {a := 1, n := 3, b := bzz}
|
||||
example : Baz := ⟨⟨1, 3, bzz⟩, ⟨5, 7⟩, bzz⟩
|
||||
example : Baz := { a := 1, n := 3, b := bzz, c := 5, d := 7, v := bzz}
|
||||
def fzz : Foo Nat (Vec Nat) := {a := 1, n := 3, b := bzz}
|
||||
|
||||
example : foo Nat (vec Nat) := { fzz with a := 7 }
|
||||
example : baz := { fzz with c := 5, d := 7, v := bzz }
|
||||
example : Foo Nat (Vec Nat) := { fzz with a := 7 }
|
||||
example : Baz := { fzz with c := 5, d := 7, v := bzz }
|
||||
|
||||
example : bar := { c := 8, d := 9 }
|
||||
example : bar := { d := 9 } -- uses the default value for c
|
||||
example : Bar := { c := 8, d := 9 }
|
||||
example : Bar := { d := 9 } -- uses the default value for c
|
||||
|
||||
.. _type_classes:
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue