diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md index 467dd655b2..9c6b306b92 100644 --- a/doc/SUMMARY.md +++ b/doc/SUMMARY.md @@ -6,18 +6,26 @@ - [Quickstart](./quickstart.md) # Language Manual - +- [Using Lean](./using_lean.md) +- [Lexical Structure](./lexical_structure.md) +- [Expressions](./expressions.md) +- [Declarations](./declarations.md) +- [Organizational features](./organization.md) + - [Sections](./sections.md) + - [Namespaces](./namespaces.md) + - [Implicit Arguments](./implicit.md) + - [Auto Bound Implicit Arguments](./autobound.md) - [Dependent Types](./deptypes.md) - [Simple Type Theory](./simptypes.md) - [Types as objects](./typeobjs.md) - [Function Abstraction and Evaluation](./funabst.md) - [Introducing Definitions](./introdef.md) - [What makes dependent type theory dependent?](./dep.md) -- [Organizational features](./organization.md) - - [Sections](./sections.md) - - [Namespaces](./namespaces.md) - - [Implicit Arguments](./implicit.md) - - [Auto Bound Implicit Arguments](./autobound.md) +- [Tactics](./tactics.md) +- [Syntax Extensions](./syntax.md) + - [The `do` Notation](./do.md) + - [String Interpolation](./stringinterp.md) +- [Metaprogramming](./metaprogramming.md) - [Declaring New Types](./decltypes.md) - [Enumerated Types](./enum.md) - [Inductive Types](./inductive.md) @@ -38,9 +46,6 @@ - [Task and Thread](./task.md) - [Functions](./functions.md) - [Tactics](./tactics.md) -- [Syntax Extensions](./syntax.md) - - [The `do` Notation](./do.md) - - [String Interpolation](./stringinterp.md) # Other diff --git a/doc/declarations.md b/doc/declarations.md new file mode 100644 index 0000000000..787b78acaf --- /dev/null +++ b/doc/declarations.md @@ -0,0 +1,804 @@ +# Declarations + +-- TODO (fix) + +Declaration Names +================= + +A declaration name is a :ref:`hierarchical identifier ` that is interpreted relative to the current namespace as well as (during lookup) to the set of open namespaces. + +.. code-block:: lean + + namespace a + constant b.c : Nat + #print b.c -- constant a.b.c : Nat + end a + + #print a.b.c -- constant a.b.c : Nat + open a + #print b.c -- constant a.b.c : Nat + +Declaration names starting with an underscore are reserved for internal use. Names starting with the special atomic name ``_root_`` are interpreted as absolute names. + +.. code-block:: lean + + constant a : Nat + namespace a + constant a : Int + #print _root_.a -- constant a : Nat + #print a.a -- constant a.a : Int + end a + +Contexts and Telescopes +======================= + +When processing user input, Lean first parses text to a raw expression format. It then uses background information and type constants to disambiguate overloaded symbols and infer implicit arguments, resulting in a fully-formed expression. This process is known as *elaboration*. + +As hinted in :numref:`expression_syntax`, expressions are parsed and +elaborated with respect to an *environment* and a *local +context*. Roughly speaking, an environment represents the state of +Lean at the point where an expression is parsed, including previously +declared axioms, constants, definitions, and theorems. In a given +environment, a *local context* consists of a sequence ``(a₁ : α₁) +(a₂ : α₂) ... (aₙ : αₙ)`` where each ``aᵢ`` is a name denoting a local +constant and each ``αᵢ`` is an expression of type ``Sort u`` for some +``u`` which can involve elements of the environment and the local +constants ``aⱼ`` for ``j < i``. + +Intuitively, a local context is a list of variables that are held constant while an expression is being elaborated. Consider the following + +```lean +def f (a b : Nat) : Nat → Nat := fun c => a + (b + c) +``` + +Here the expression ``fun c => a + (b + c)`` is elaborated in the context ``(a : Nat) (b : Nat)`` and the expression ``a + (b + c)`` is elaborated in the context ``(a : Nat) (b : Nat) (c : Nat)``. If you replace the expression ``a + (b + c)`` with an underscore, the error message from Lean will include the current *goal*: + +.. code-block:: text + + a b c : Nat + ⊢ Nat + +Here ``a b c : Nat`` indicates the local context, and the second ``Nat`` indicates the expected type of the result. + +A *context* is sometimes called a *telescope*, but the latter is used more generally to include a sequence of declarations occuring relative to a given context. For example, relative to the context ``(a₁ : α₁) (a₂ : α₂) ... (aₙ : αₙ)``, the types ``βᵢ`` in a telescope ``(b₁ : β₁) (b₂ : β₂) ... (bₙ : βₙ)`` can refer to ``a₁, ..., aₙ``. Thus a context can be viewed as a telescope relative to the empty context. + +Telescopes are often used to describe a list of arguments, or parameters, to a declaration. In such cases, it is often notationally convenient to let ``(a : α)`` stand for a telescope rather than just a single argument. In general, the annotations described in :ref:`implicit_arguments` can be used to mark arguments as implicit. + +.. _basic_declarations: + +Basic Declarations +================== + +Lean provides ways of adding new objects to the environment. The following provide straightforward ways of declaring new objects: + +* ``axiom c : α`` : declare a constant named ``c`` of type ``α``, it is postulating that `α` is not an empty type. +* ``def c : α := v`` : defines ``c`` to denote ``v``, which should have type ``α``. +* ``theorem c : p := v`` : similar to ``def``, but intended to be used when ``p`` is a proposition. +* ``constant c : α (:= v)?`` : declares a opaque constant named ``c`` of type ``α``, the optional value `v` is must have type `α` + and can be viewed as a certificate that ``α`` is not an empty type. If the value is not provided, Lean tries to find one + using a proceture based on type class resolution. The value `v` is hidden from the type checker. You can assume that + Lean "forgets" `v` after type checking this kind of declaration. + +It is sometimes useful to be able to simulate a definition or theorem without naming it or adding it to the environment. + +* ``example : α := t`` : elaborates ``t`` and checks that it has sort ``α`` (often a proposition), without adding it to the environment. + +In ``def``, the type (``α`` or ``p``, respectively) can be omitted when it can be inferred by Lean. Constants declared with ``theorem`` are marked as ``irreducible``. + +Any of ``def``, ``theorem``, ``axiom``, or ``example`` can take a list of arguments (that is, a context) before the colon. If ``(a : α)`` is a context, the definition ``def foo (a : α) : β := t`` +is interpreted as ``def foo : (a : α) → β := fun a : α => t``. Similarly, a theorem ``theorem foo (a : α) : p := t`` is interpreted as ``theorem foo : ∀ a : α, p := fun a : α => t``. + +```lean +constant c : Nat +constant d : Nat +axiom cd_eq : c = d + +def foo : Nat := 5 +def bar := 6 +def baz (x y : Nat) (s : List Nat) := [x, y] ++ s + +theorem foo_eq_five : foo = 5 := rfl +theorem baz_theorem (x y : Nat) : baz x y [] = [x, y] := rfl + +example (x y : Nat) : baz x y [] = [x, y] := rfl +``` + +Inductive Types +=============== + +Lean's axiomatic foundation allows users to declare arbitrary +inductive families, following the pattern described by [Dybjer]_. To +make the presentation more manageable, we first describe inductive +*types*, and then describe the generalization to inductive *families* +in the next section. The declaration of an inductive type has the +following form: + +``` +inductive Foo (a : α) where + | constructor₁ : (b : β₁) → Foo a + | constructor₂ : (b : β₂) → Foo a + ... + | constructorₙ : (b : βₙ) → Foo a +``` + +Here ``(a : α)`` is a context and each ``(b : βᵢ)`` is a telescope in the context ``(a : α)`` together with ``Foo``, subject to the following constraints. + +Suppose the telescope ``(b : βᵢ)`` is ``(b₁ : βᵢ₁) ... (bᵤ : βᵢᵤ)``. Each argument in the telescope is either *nonrecursive* or *recursive*. + +- 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 it ``βᵢⱼ`` of the form ``Π (d : δ), foo`` where ``(d : δ)`` is a telescope which does not refer to ``foo`` or any nonrecursive arguments. + +The inductive type ``foo`` represents a type that is freely generated by the constructors. Each constructor can take arbitrary data and facts as arguments (the nonrecursive arguments), as well as indexed sequences of elements of ``foo`` that have been previously constructed (the recursive arguments). In set theoretic models, such sets can be represented by well-founded trees labeled by the constructor data, or they can defined using other transfinite or impredicative means. + +The declaration of the type ``foo`` as above results in the addition of the following constants to the environment: + +- the *type former* ``foo : Π (a : α), Sort u`` +- for each ``i``, the *constructor* ``foo.constructorᵢ : Π (a : α) (b : βᵢ), foo a`` +- the *eliminator* ``foo.rec``, which takes arguments + + + ``(a : α)`` (the parameters) + + ``{C : foo a → Type u}`` (the *motive* of the elimination) + + for each ``i``, the *minor premise* corresponding to ``constructorᵢ`` + + ``(x : foo)`` (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 (bⱼ d)`` corresponding to each recursive argument ``(bⱼ : βᵢⱼ)``, where ``βᵢⱼ`` is of the form ``Π (d : δ), foo`` (the recursive values of the function being defined) + + and returns an element of ``C (constructorᵢ a b)``, the intended value of the function at ``constructorᵢ a b``. + +The eliminator represents a principle of recursion: to construct an element of ``C x`` where ``x : foo a``, it suffices to consider each of the cases where ``x`` is of the form ``constructorᵢ a b`` and to provide an auxiliary construction in each case. In the case where some of the arguments to ``constructorᵢ`` are recursive, we can assume that we have already constructed values of ``C y`` for each value ``y`` constructed at an earlier stage. + +Under the propositions-as-type correspondence, when ``C x`` is an element of ``Prop``, the eliminator represents a principle of induction. In order to show ``∀ x, C x``, it suffices to show that ``C`` holds for each constructor, under the inductive hypothesis that it holds for all recursive inputs to the constructor. + +The eliminator and constructors satisfy the following identities, in which all the arguments are shown explicitly. Suppose we set ``F := foo.rec a C f₁ ... fₙ``. Then for each constructor, we have the definitional reduction: + +.. code-block :: text + + F (constructorᵢ a b) = fᵢ b ... (fun d : δᵢⱼ => F (bⱼ d)) ... + +where the ellipses include one entry for each recursive argument. + +Below are some common examples of inductive types, many of which are defined in the core library. + +.. code-block:: lean + + namespace hide + universes u v + + -- BEGIN + inductive empty : Type + + inductive unit : Type + | star : unit + + inductive bool : Type + | ff : bool + | tt : bool + + inductive prod (α : Type u) (β : Type v) : Type (max u v) + | mk : α → β → prod + + inductive sum (α : Type u) (β : Type v) + | inl : α → sum + | inr : β → sum + + inductive sigma (α : Type u) (β : α → Type v) + | mk : Π a : α, β a → sigma + + inductive false : Prop + + inductive true : Prop + | trivial : true + + inductive and (p q : Prop) : Prop + | intro : p → q → and + + inductive or (p q : Prop) : Prop + | inl : p → or + | inr : q → or + + inductive Exists (α : Type u) (p : α → Prop) : Prop + | intro : ∀ x : α, p x → Exists + + inductive subtype (α : Type u) (p : α → Prop) : Type u + | intro : ∀ x : α, p x → subtype + + inductive nat : Type + | zero : nat + | succ : nat → nat + + 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 + + -- every internal node has subtrees indexed by Nat + 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``. + +Elements of the context ``(a : α)`` can be marked implicit as described in :numref:`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]`` :ref:`attribute ` to ensure that these will be used appropriately by the :ref:`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. + +Lean allows some additional syntactic conveniences. You can omit the return type of the type former, ``Sort u``, in which case Lean will infer the minimal possible nonzero value for ``u``. As with function definitions, you can list arguments to the constructors before the colon. In an enumerated type (that is, one where the constructors have no arguments), you can also leave out the return type of the constructors. + +.. code-block:: lean + + namespace hide + universe u + + -- BEGIN + inductive weekday + | sunday | monday | tuesday | wednesday + | thursday | friday | saturday + + inductive nat + | zero + | succ (n : nat) : nat + + inductive list (α : Type u) + | nil {} : list + | cons (a : α) (l : list) : list + + @[pattern] + def list.nil' (α : Type u) : list α := list.nil + + def length {α : Type u} : list α → Nat + | (list.nil' .(α)) := 0 + | (list.cons a l) := 1 + length l + -- END + + 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 + +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 :numref:`structures_and_records` and :numref:`namespaces`. + +.. code-block:: lean + + namespace hide + universe u + + -- BEGIN + inductive nat + | zero + | succ (n : nat) : nat + + #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 + + -- END + + end hide + +.. _inductive_families: + +Inductive Families +================== + +In fact, Lean implements a slight generalization of the inductive types described in the previous section, namely, inductive *families*. The declaration of an inductive family in Lean has the following form: + +.. code-block:: text + + inductive foo (a : α) : Π (c : γ), Sort u + | 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ᵢ``. + +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. + +- 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 *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) + + for each ``i``, the minor premise corresponding to ``constructorᵢ`` + + ``(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`` + + 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: + +.. code-block :: text + + F (constructorᵢ a b) = fᵢ b ... (fun d : δᵢⱼ => F (bⱼ d)) ... + +where the ellipses include one entry for each recursive argument. + +The following are examples of inductive families. + +.. code-block:: lean + + namespace hide + universe u + + -- BEGIN + 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) + + inductive eq {α : Sort u} (a : α) : α → Prop + | refl : eq a + -- END + + 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. + +Putting an inductive family in ``Prop``, however, does impose a restriction on the eliminator. Generally speaking, for an inductive family in ``Prop``, the motive in the eliminator is required to be in ``Prop``. But there is an exception to this rule: you are allowed to eliminate from an inductively defined ``Prop`` to an arbitrary ``Sort`` when there is only one constructor, and each argument to that constructor is either in ``Prop`` or an index. The intuition is that in this case the elimination does not make use of any information that is not already given by the mere fact that the type of argument is inhabited. This special case is known as *singleton elimination*. + +.. _mutual_and_nested_inductive_definitions: + +Mutual and Nested Inductive Definitions +======================================= + +Lean supports two generalizations of the inductive families described above, namely, *mutual* and *nested* inductive definitions. These are *not* implemented natively in the kernel. Rather, the definitions are compiled down to the primitive inductive types and families. + +The first generalization allows for multiple inductive types to be defined simultaneously. + +.. code-block:: text + + mutual inductive foo, bar (a : α) + with foo : Π (c : γ), Sort u + | constructor₁₁ : Π (b : β₁₁), foo t₁₁ + | constructor₁₂ : Π (b : β₁₂), foo t₁₂ + ... + | constructor₁ₙ : Π (b : β₁ₙ), foo t₁ₙ + with bar : + | constructor₂₁ : Π (b : β₂₁), bar t₂₁ + | constructor₂₂ : Π (b : β₂₂), bar t₂₂ + ... + | constructor₂ₘ : Π (b : β₂ₘ), bar 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. + +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. + +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) + + inductive tree (α : Type u) + | mk : α → list tree → tree + + inductive double_tree (α : Type u) + | mk : α → list double_tree × list double_tree → double_tree + -- END + +.. _the_equation_compiler: + +The Equation Compiler +===================== + +The equation compiler takes an equational description of a function or proof and tries to define an object meeting that specification. It expects input with the following syntax: + +.. code-block:: text + + def foo (a : α) : Π (b : β), γ + | [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``. + +Each ``patternsᵢ`` is a sequence of patterns of the same length as ``(b : β)``. A pattern is either: + +- a variable, denoting an arbitrary value of the relevant type, +- an underscore, denoting a *wildcard* or *anonymous variable*, +- an inaccessible term (see below), or +- a constructor for the inductive type of the corresponding argument, applied to a sequence of patterns. + +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 :numref:`the_rewriter` and :numref:`the_simplifier`). 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. + +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. + +.. code-block:: lean + + open nat + + def sub2 : Nat → Nat + | 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 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 + + -- BEGIN + 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 + + example : append [(1 : Nat), 2, 3] [4, 5] = [1, 2, 3, 4, 5] := rfl + -- END + + 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``. + +.. code-block:: lean + + namespace hide + open nat + + -- BEGIN + def div : Nat → Nat → Nat + | 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, + 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] + -- END + + 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. + +The equation compiler also allows mutual recursive definitions, with a syntax similar to that of :ref:`mutual inductive definitions `. They are compiled using well-founded recursion, and so once again the defining equations hold only propositionally. + +.. 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 + + example (a : Nat) : even (a + 1) = odd a := + by simp [even] + + example (a : Nat) : odd (a + 1) = even a := + by simp [odd] + +Well-founded recursion is especially useful with :ref:`mutual and nested inductive definitions `, since it provides the canonical way of defining functions on these types. + +.. 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) + + open even odd + + theorem not_odd_zero : ¬ odd 0. + + 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 + + inductive term + | const : string → term + | app : string → list term → 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 + +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. + +.. code-block:: lean + + universe u + + inductive vector (α : Type u) : Nat → Type u + | nil {} : vector 0 + | cons : Π {n}, α → vector n → vector (n+1) + + namespace vector + + def head {α : Type} : Π {n}, vector α (n+1) → α + | n (cons h t) := h + + def tail {α : Type} : Π {n}, vector α (n+1) → vector α n + | 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) + + 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 + +.. _match_expressions: + +Match Expressions +================= + +Lean supports a ``match ... with ...`` construct similar to ones found in most functional programming languages. The syntax is as follows: + +.. code-block:: text + + match t₁, ..., tₙ with + | 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. + +Any ``match`` expression is interpreted using the equation compiler, which generalizes ``t₁, ..., tₙ``, defines an internal function meeting the specification, and then applies it to ``t₁, ..., tₙ``. In contrast to the definitions in :numref:`the_equation_compiler`, the terms ``tᵢ`` are arbitrary terms rather than just variables, and the expression can occur anywhere within a Lean expression, not just at the top level of a definition. Note that the syntax here is somewhat different: both the terms ``tᵢ`` and the patterns ``pᵢⱼ`` are separated by commas. + +.. code-block:: lean + + 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 + +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. + +.. code-block:: lean + + def bar₁ : Nat × Nat → Nat + | (m, n) := m + n + + def bar₂ (p : Nat × Nat) : Nat := + match p with (m, n) := m + n end + + def bar₃ : Nat × Nat → Nat := + fun ⟨m, n⟩ => m + n + + def bar₄ (p : Nat × Nat) : Nat := + let ⟨m, n⟩ := p in m + n + +.. _structures_and_records: + +Structures and Records +====================== + +The ``structure`` command in Lean is used to define an inductive data type with a single constructor and to define its projections at the same time. The syntax is as follows: + +.. code-block:: text + + 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``. + +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 single constructor : + + .. code-block:: text + + foo.constructor : Π (a : α) (_to_foo : foo) (_to_bar : bar) + (field₁ : β₁) ... (fieldₙ : βₙ), foo a + +- the eliminator ``foo.rec`` for the inductive type with that constructor + +In addition, Lean defines + +- 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``: + +- *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 :numref:`namespaces`. + +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ᵢ : βᵢ`` : + +- *anonymous constructor*: ``⟨ b₁, b₂, f₁, ..., fₙ ⟩`` +- *record notation*: + + .. code-block:: text + + { foo . to_bar := b₁, to_baz := b₂, field₁ := f₁, ..., + fieldₙ := fₙ } + +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. + +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 + +- *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. + +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 + + structure vec (α : Type u) (n : Nat) := + (l : list α) (h : l.length = n) + + structure foo (α : Type u) (β : Nat → Type v) : Type (max u v) := + (a : α) (n : Nat) (b : β n) + + structure bar := + (c : Nat := 8) (d : Nat) + + structure baz extends foo Nat (vec Nat), bar := + (v : vec Nat n) + + #check foo + #check @foo.mk + #check @foo.rec + + #check foo.a + #check foo.n + #check foo.b + + #check baz + #check @baz.mk + #check @baz.rec + + #check baz.to_foo + #check baz.to_bar + #check baz.v + + def bzz := vec.mk [1, 2, 3] rfl + + #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 : 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 : 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 + +.. _type_classes: + +Type Classes +============ + +(Classes and instances. Anonymous instances. Local instances.) + + +.. [Dybjer] Dybjer, Peter, *Inductive Families*. Formal Aspects of Computing 6, 1994, pages 440-465. diff --git a/doc/expressions.md b/doc/expressions.md new file mode 100644 index 0000000000..5e2a787d49 --- /dev/null +++ b/doc/expressions.md @@ -0,0 +1,577 @@ +Expressions +=========== + + +Universes +========= + +Every type in Lean is, by definition, an expression of type ``Sort u`` +for some universe level ``u``. A universe level is one of the +following: + +* a natural number, ``n`` +* a universe variable, ``u`` (declared with the command ``universe`` or ``universes``) +* an expression ``u + n``, where ``u`` is a universe level and ``n`` is a natural number +* an expression ``max u v``, where ``u`` and ``v`` are universes +* an expression ``imax u v``, where ``u`` and ``v`` are universe levels + +The last one denotes the universe level ``0`` if ``v`` is ``0``, and ``max u v`` otherwise. + +```lean +universe u v + +#check Sort u +#check Sort 5 +#check Sort (u + 1) +#check Sort (u + 3) +#check Sort (max u v) +#check Sort (max (u + 3) v) +#check Sort (imax (u + 3) v) +#check Prop +#check Type +``` + +Expression Syntax +================= + +The set of expressions in Lean is defined inductively as follows: + +* ``Sort u`` : the universe of types at universe level ``u`` +* ``c`` : where ``c`` is an identifier denoting a declared constant or a defined object +* ``x`` : where ``x`` is a variable in the local context in which the expression is interpreted +* `m?` : where `m?` is a metavariable in the metavariable context in which the expression is interpreted, + you can view metavariable as a "hole" that still needs to be synthesized +* ``(x : α) → β`` : the type of functions taking an element ``x`` of ``α`` to an element of ``β``, + where ``β`` is an expression whose type is a ``Sort`` +* ``s t`` : the result of applying ``s`` to ``t``, where ``s`` and ``t`` are expressions +* ``fun x : α => t`` or `λ x : α => t`: the function mapping any value ``x`` of type ``α`` to ``t``, where ``t`` is an expression +* ``let x := t; s`` : a local definition, denotes the value of ``s`` when ``x`` is replaced by ``t`` +* `s.i` : a projection, denotes the value of the `i`-th field of `s` +* `lit` : a natural number or string literal +* `mdata k s` : the expression `s` decorated with metadata `k`, where is a key-value map + +Every well formed term in Lean has a *type*, which itself is an expression of type ``Sort u`` for some ``u``. The fact that a term ``t`` has type ``α`` is written ``t : α``. + +For an expression to be well formed, its components have to satisfy certain typing constraints. These, in turn, determine the type of the resulting term, as follows: + +* ``Sort u : Sort (u + 1)`` +* ``c : α``, where ``α`` is the type that ``c`` has been declared or defined to have +* ``x : α``, where ``α`` is the type that ``x`` has been assigned in the local context where it is interpreted +* ``?m : α``, where ``α`` is the type that ``?m`` has been declared in the metavariable context where it is interpreted +* ``(x : α) → β : Sort (imax u v)`` where ``α : Sort u``, and ``β : Sort v`` assuming ``x : α`` +* ``s t : β[t/x]`` where ``s`` has type ``(x : α) → β`` and ``t`` has type ``α`` +* ``(fun x : α => t) : (x : α) → β`` if ``t`` has type ``β`` whenever ``x`` has type ``α`` +* ``(let x := t; s) : β[t/x]`` where ``t`` has type ``α`` and ``s`` has type ``β`` assuming ``x : α`` +* `lit : Nat` if `lit` is a numeral +* `lit : String` if `lit` is a string literal +* `mdata k s : α` if `s : α` +* `s.i : α` if `s : β` and `β` is an inductive datatype with only one constructor, and `i`-th field has type `α` + +``Prop`` abbreviates ``Sort 0``, ``Type`` abbreviates ``Sort 1``, and +``Type u`` abbreviates ``Sort (u + 1)`` when ``u`` is a universe +variable. We say "``α`` is a type" to express ``α : Type u`` for some +``u``, and we say "``p`` is a proposition" to express +``p : Prop``. Using the *propositions as types* correspondence, given +``p : Prop``, we refer to an expression ``t : p`` as a *proof* of ``p``. In +contrast, given ``α : Type u`` for some ``u`` and ``t : α``, we +sometimes refer to ``t`` as *data*. + +When the expression ``β`` in ``(x : α) → β`` does not depend on ``x``, +it can be written ``α → β``. As usual, the variable ``x`` is bound in +``(x : α) → β``, ``fun x : α => t``, and ``let x := t; s``. The +expression ``∀ x : α, β`` is alternative syntax for ``(x : α) → β``, +and is intended to be used when ``β`` is a proposition. An underscore +can be used to generate an internal variable in a binder, as in +``fun _ : α => t``. + +*Metavariables*, that is, temporary placeholders, are used in the +process of constructing terms. Terms that are added to the +environment contain neither metavariable nor variables, which is to +say, they are fully elaborated and make sense in the empty context. + +Axioms can be declared using the ``axiom`` keyword. +Similarly, objects can be defined in various ways, such as using ``def`` and ``theorem`` keywords. +See [Chapter Declarations](./declarations.md) for more information. + +Writing an expression ``(t : α)`` forces Lean to elaborate ``t`` so that it has type ``α`` or report an error if it fails. + +Lean supports anonymous constructor notation, anonymous projections, +and various forms of match syntax, including destructuring ``fun`` and +``let``. These, as well as notation for common data types (like pairs, +lists, and so on) are discussed in [Chapter Declarations](./declarations.md) +in connection with inductive types. + +```lean +universe u + +#check Sort 0 +#check Prop +#check Sort 1 +#check Type +#check Sort u +#check Sort (u+1) + +#check Nat → Bool +#check (α : Type u) → List α +#check (α : Type u) → (β : Type u) → Sum α β +#check fun x : Nat => x +#check fun (α : Type u) (x : α) => x +#check let x := 5; x * 2 +#check "hello" +#check (fun x => x) true +``` + +Implicit Arguments +================== + +When declaring arguments to defined objects in Lean (for example, with +``def``, ``theorem``, ``axiom``, ``constant``, ``inductive``, or +``structure``; see [Chapter Declarations](./declarations.md) or when +declaring variables in sections (see [Chapter Other Commands](./other_commands.md)), +arguments can be annotated as *explicit* or *implicit*. +This determines how expressions containing the object are interpreted. + +* ``(x : α)`` : an explicit argument of type ``α`` +* ``{x : α}`` : an implicit argument, eagerly inserted +* ``⦃x : α⦄`` or ``{{x : α}}`` : an implicit argument, weakly inserted +* ``[x : α]`` : an implicit argument that should be inferred by type class resolution +* ``(x : α := v)`` : an optional argument, with default value ``v`` +* ``(x : α := by tac)`` : an implicit argument, to be synthesized by tactic ``tac`` + +The name of the variable can be omitted from a class resolution +argument, in which case an internal name is generated. + +When a function has an explicit argument, you can nonetheless ask +Lean's elaborator to infer the argument automatically, by entering it +as an underscore (``_``). Conversely, writing ``@foo`` indicates that +all of the arguments to be ``foo`` are to be given explicitly, +independent of how ``foo`` was declared. You can also provide a value +for an implicit parameter using named arguments. Named arguments +enable you to specify an argument for a parameter by matching the +argument with its name rather than with its position in the parameter +list. If you don't remember the order of the parameters but know +their names, you can send the arguments in any order. You may also +provide the value for an implicit parameter whenLean failed to infer +it. Named arguments also improve the readability of your code by +identifying what each argument represents. + + +```lean +def add (x y : Nat) : Nat := + x + y + +#check add 2 3 -- Nat +#eval add 2 3 -- 5 + +def id1 (α : Type u) (x : α) : α := x + +#check id1 Nat 3 +#check id1 _ 3 + +def id2 {α : Type u} (x : α) : α := x + +#check id2 3 +#check @id2 Nat 3 +#check id2 (α := Nat) 3 +#check id2 +#check id2 (α := Nat) + +def id3 {{α : Type u}} (x : α) : α := x + +#check id3 3 +#check @id3 Nat 3 +#check (id3 : (α : Type) → α → α) + +class Cls where + val : Nat + +instance Cls_five : Cls where + val := 5 + +def ex2 [c : Cls] : Nat := c.val + +example : ex2 = 5 := rfl + +def ex2a [Cls] : Nat := ex2 + +example : ex2a = 5 := rfl + +def ex3 (x : Nat := 5) := x + +#check ex3 2 +#check ex3 + +example : ex3 = 5 := rfl + +def ex4 (x : Nat) (y : Nat := x) : Nat := + x * y + +example : ex4 x = x * x := + rfl +``` + +Basic Data Types and Assertions +=============================== + +The core library contains a number of basic data types, such as the +natural numbers (`Nat`), the integers (`Int`), the +booleans (``Bool``), and common operations on these, as well as the +usual logical quantifiers and connectives. Some example are given +below. A list of common notations and their precedences can be found +in a [file](https://github.com/leanprover/lean4/blob/master/src/Init/Notation.lean) +in the core library. The core library also contains a number of basic +data type constructors. Definitions can also be found the +[Data](https://github.com/leanprover/lean4/blob/master/src/Init/Data) +directory of the core library. For more information, see also [Chapter libraries](./libraries.md). + +``` +/- numbers -/ +def f1 (a b c : Nat) : Nat := + a^2 + b^2 + c^2 + +def p1 (a b c d : Nat) : Prop := + (a + b)^c ≤ d + +def p2 (i j k : Int) : Prop := + i % (j * k) = 0 + + +/- booleans -/ + +def f2 (a b c : Bool) : Bool := + a && (b || c) + +/- pairs -/ + +#eval (1, 2) + +def p : Nat × Bool := (1, + +section +variables (a b c : Nat) (p : Nat × bool) + +#check (1, 2) +#check p.1 * 2 +#check p.2 && tt +#check ((1, 2, 3) : Nat × Nat × Nat) +end + +/- lists -/ +section +variables x y z : Nat +variables xs ys zs : list Nat +open list + +#check (1 :: xs) ++ (y :: zs) ++ [1,2,3] +#check append (cons 1 xs) (cons y zs) +#check map (λ x, x^2) [1, 2, 3] +end + +/- sets -/ +section +variables s t u : set Nat + +#check ({1, 2, 3} ∩ s) ∪ ({x | x < 7} ∩ t) +end + +/- strings and characters -/ +#check "hello world" +#check 'a' + +/- assertions -/ +#check ∀ a b c n : Nat, + a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ n > 2 → a^n + b^n ≠ c^n + +def unbounded (f : Nat → Nat) : Prop := ∀ M, ∃ n, f n ≥ M +``` +.. _constructors_projections_and_matching: + +Constructors, Projections, and Matching +======================================= + +Lean's foundation, the *Calculus of Inductive Constructions*, supports the declaration of *inductive types*. Such types can have any number of *constructors*, and an associated *eliminator* (or *recursor*). Inductive types with one constructor, known as *structures*, have *projections*. The full syntax of inductive types is described in :numref:`Chapter %s `, but here we describe some syntactic elements that facilitate their use in expressions. + +When Lean can infer the type of an expression and it is an inductive type with one constructor, then one can write ``⟨a1, a2, ..., an⟩`` to apply the constructor without naming it. For example, ``⟨a, b⟩`` denotes ``prod.mk a b`` in a context where the expression can be inferred to be a pair, and ``⟨h₁, h₂⟩`` denotes ``and.intro h₁ h₂`` in a context when the expression can be inferred to be a conjunction. The notation will nest constructions automatically, so ``⟨a1, a2, a3⟩`` is interpreted as ``prod.mk a1 (prod.mk a2 a3)`` when the expression is expected to have a type of the form ``α1 × α2 × α3``. (The latter is interpreted as ``α1 × (α2 × α3)``, since the product associates to the right.) + +Similarly, one can use "dot notation" for projections: one can write ``p.fst`` and ``p.snd`` for ``prod.fst p`` and ``prod.snd p`` when Lean can infer that ``p`` is an element of a product, and ``h.left`` and ``h.right`` for ``and.left h`` and ``and.right h`` when ``h`` is a conjunction. + +The anonymous projector notation can used more generally for any objects defined in a *namespace* (see :numref:`Chapter %s `). For example, if ``l`` has type ``list α`` then ``l.map f`` abbreviates ``list.map f l``, in which ``l`` has been placed at the first argument position where ``list.map`` expects a ``list``. + +Finally, for data types with one constructor, one destruct an element by pattern matching using the ``let`` and ``assume`` constructs, as in the examples below. Internally, these are interpreted using the ``match`` construct, which is in turn compiled down for the eliminator for the inductive type, as described in :numref:`Chapter %s `. + +.. code-block:: lean + + universes u v + variables {α : Type u} {β : Type v} + + def p : Nat × ℤ := ⟨1, 2⟩ + #check p.fst + #check p.snd + + def p' : Nat × ℤ × bool := ⟨1, 2, tt⟩ + #check p'.fst + #check p'.snd.fst + #check p'.snd.snd + + def swap_pair (p : α × β) : β × α := + ⟨p.snd, p.fst⟩ + + theorem swap_conj {a b : Prop} (h : a ∧ b) : b ∧ a := + ⟨h.right, h.left⟩ + + #check [1, 2, 3].append [2, 3, 4] + #check [1, 2, 3].map (λ x, x^2) + + example (p q : Prop) : p ∧ q → q ∧ p := + λ h, ⟨h.right, h.left⟩ + + def swap_pair' (p : α × β) : β × α := + let (x, y) := p in (y, x) + + theorem swap_conj' {a b : Prop} (h : a ∧ b) : b ∧ a := + let ⟨ha, hb⟩ := h in ⟨hb, ha⟩ + + def swap_pair'' : α × β → β × α := + λ ⟨x, y⟩, (y, x) + + theorem swap_conj'' {a b : Prop} : a ∧ b → b ∧ a := + assume ⟨ha, hb⟩, ⟨hb, ha⟩ + +Structured Proofs +================= + +Syntactic sugar is provided for writing structured proof terms: + +* ``have h : p := s; t`` is sugar for ``(fun h : p => t) s`` +* ``suffices h : p from s; t`` is sugar for ``(λ h : p => s) t`` +* ``suffices h : p by s; t`` is sugar for ``(suffixes h : p from by s; t)`` +* ``show p from t`` is sugar for ``(have this : p := t; this)`` +* ``show p by tac`` is sugar for ``(show p from by tac)`` + +Types can be omitted when they can be inferred by Lean. Lean also +allows ``have : p := t; s``, which gives the assumption the +name ``this`` in the local context. Similarly, Lean recognizes the +variant ``suffices p from s; t``, which use the name ``this`` for the new hypothesis. + +The notation ``‹p›`` is notation for ``(by assumption : p)``, and can +therefore be used to apply hypotheses in the local context. + +As noted in [Constructors, Projections and Matching](#constructors_projections_and_matching), +anonymous constructors and projections and match syntax can be used in proofs just as in expressions that denote data. + +.. code-block:: lean + + example (p q r : Prop) : p → (q ∧ r) → p ∧ q := + assume h₁ : p, + assume h₂ : q ∧ r, + have h₃ : q, from and.left h₂, + show p ∧ q, from and.intro h₁ h₃ + + example (p q r : Prop) : p → (q ∧ r) → p ∧ q := + assume : p, + assume : q ∧ r, + have q, from and.left this, + show p ∧ q, from and.intro ‹p› this + + example (p q r : Prop) : p → (q ∧ r) → p ∧ q := + assume h₁ : p, + assume h₂ : q ∧ r, + suffices h₃ : q, from and.intro h₁ h₃, + show q, from and.left h₂ + +Lean also supports a calculational environment, which is introduced with the keyword ``calc``. The syntax is as follows: + +.. code-block:: text + + calc + _0 'op_1' _1 ':' _1 + '...' 'op_2' _2 ':' _2 + ... + '...' 'op_n' _n ':' _n + +Each ``_i`` is a proof for ``_{i-1} op_i _i``. + +Here is an example: + +.. code-block:: lean + + variables (a b c d e : Nat) + variable h1 : a = b + variable h2 : b = c + 1 + variable h3 : c = d + variable h4 : e = 1 + d + + theorem T : a = e := + calc + a = b : h1 + ... = c + 1 : h2 + ... = d + 1 : congr_arg _ h3 + ... = 1 + d : add_comm d (1 : Nat) + ... = e : eq.symm h4 + +The style of writing proofs is most effective when it is used in conjunction with the ``simp`` and ``rewrite`` tactics. + +.. _computation: + +Computation +=========== + +Two expressions that differ up to a renaming of their bound variables are said to be *α-equivalent*, and are treated as syntactically equivalent by Lean. + +Every expression in Lean has a natural computational interpretation, unless it involves classical elements that block computation, as described in the next section. The system recognizes the following notions of *reduction*: + +* *β-reduction* : An expression ``(λ x, t) s`` β-reduces to ``t[s/x]``, that is, the result of replacing ``x`` by ``s`` in ``t``. +* *ζ-reduction* : An expression ``let x := s in t`` ζ-reduces to ``t[s/x]``. +* *δ-reduction* : If ``c`` is a defined constant with definition ``t``, then ``c`` δ-reduces to to ``t``. +* *ι-reduction* : When a function defined by recursion on an inductive type is applied to an element given by an explicit constructor, the result ι-reduces to the specified function value, as described in :numref:`inductive_types`. + +The reduction relation is transitive, which is to say, is ``s`` reduces to ``s'`` and ``t`` reduces to ``t'``, then ``s t`` reduces to ``s' t'``, ``λ x, s`` reduces to ``λ x, s'``, and so on. If ``s`` and ``t`` reduce to a common term, they are said to be *definitionally equal*. Definitional equality is defined to be the smallest equivalence relation that satisfies all these properties and also includes α-equivalence and the following two relations: + +* *η-equivalence* : An expression ``(λx, t x)`` is η-equivalent to ``t``, assuming ``x`` does not occur in ``t``. +* *proof irrelevance* : If ``p : Prop``, ``s : p``, and ``t : p``, then ``s`` and ``t`` are considered to be equivalent. + +This last fact reflects the intuition that once we have proved a proposition ``p``, we only care that is has been proved; the proof does nothing more than witness the fact that ``p`` is true. + +Definitional equality is a strong notion of equalty of values. Lean's logical foundations sanction treating definitionally equal terms as being the same when checking that a term is well-typed and/or that it has a given type. + +The reduction relation is believed to be strongly normalizing, which is to say, every sequence of reductions applied to a term will eventually terminate. The property guarantees that Lean's type-checking algorithm terminates, at least in principle. The consistency of Lean and its soundness with respect to set-theoretic semantics do not depend on either of these properties. + +Lean provides two commands to compute with expressions: + +* ``#reduce t`` : use the kernel type-checking procedures to carry out reductions on ``t`` until no more reductions are possible, and show the result +* ``#eval t`` : evaluate ``t`` using a fast bytecode evaluator, and show the result + +Every computable definition in Lean is compiled to bytecode at definition time. Bytecode evaluation is more liberal than kernel evaluation: types and all propositional information are erased, and functions are evaluated using a stack-based virtual machine. As a result, ``#eval`` is more efficient than ``#reduce,`` and can be used to execute complex programs. In contrast, ``#reduce`` is designed to be small and reliable, and to produce type-correct terms at each step. Bytecode is never used in type checking, so as far as soundness and consistency are concerned, only kernel reduction is part of the trusted computing base. + +.. code-block:: lean + + #reduce (λ x, x + 3) 5 + #eval (λ x, x + 3) 5 + + #reduce let x := 5 in x + 3 + #eval let x := 5 in x + 3 + + def f x := x + 3 + + #reduce f 5 + #eval f 5 + + #reduce @nat.rec (λ n, Nat) (0 : Nat) + (λ n recval : Nat, recval + n + 1) (5 : Nat) + #eval @nat.rec (λ n, Nat) (0 : Nat) + (λ n recval : Nat, recval + n + 1) (5 : Nat) + + def g : Nat → Nat + | 0 := 0 + | (n+1) := g n + n + 1 + + #reduce g 5 + #eval g 5 + + #eval g 50000 + + example : (λ x, x + 3) 5 = 8 := rfl + example : (λ x, f x) = f := rfl + example (p : Prop) (h₁ h₂ : p) : h₁ = h₂ := rfl + +Note: the combination of proof irrelevance and singleton ``Prop`` elimination in ι-reduction renders the ideal version of definitional equality, as described above, undecidable. Lean's procedure for checking definitional equality is only an approximation to the ideal. It is not transitive, as illustrated by the example below. Once again, this does not compromise the consistency or soundness of Lean; it only means that Lean is more conservative in the terms it recognizes as well typed, and this does not cause problems in practice. Singleton elimination will be discussed in greater detail in :numref:`inductive_types`. + +.. code-block:: lean + + def R (x y : unit) := false + def accrec := @acc.rec unit R (λ_, unit) (λ _ a ih, ()) () + example (h) : accrec h = accrec (acc.intro _ (λ y, acc.inv h)) := + rfl + example (h) : accrec (acc.intro _ (λ y, acc.inv h)) = () := rfl + example (h) : accrec h = () := sorry -- rfl fails + + +Axioms +====== + +Lean's foundational framework consists of: + +- type universes and dependent function types, as described above + +- inductive definitions, as described in :numref:`inductive_types` and :numref:`inductive_families`. + +In addition, the core library defines (and trusts) the following axiomatic extensions: + +- propositional extensionality: + + .. code-block:: lean + + namespace hide + + -- BEGIN + axiom propext {a b : Prop} : (a ↔ b) → a = b + -- END + + end hide + +- quotients: + + .. code-block:: lean + + namespace hide + -- BEGIN + universes u v + + constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u + + constant quot.mk : Π {α : Sort u} (r : α → α → Prop), + α → quot r + + axiom quot.ind : ∀ {α : Sort u} {r : α → α → Prop} + {β : quot r → Prop}, + (∀ a, β (quot.mk r a)) → + ∀ (q : quot r), β q + + constant quot.lift : Π {α : Sort u} {r : α → α → Prop} + {β : Sort u} (f : α → β), + (∀ a b, r a b → f a = f b) → quot r → β + + axiom quot.sound : ∀ {α : Type u} {r : α → α → Prop} + {a b : α}, + r a b → quot.mk r a = quot.mk r b + -- END + end hide + + ``quot r`` represents the quotient of ``α`` by the smallest equivalence relation containing ``r``. ``quot.mk`` and ``quot.lift`` satisfy the following computation rule: + + .. code-block:: text + + quot.lift f h (quot.mk r a) = f a + +- choice: + + .. code-block:: lean + + namespace hide + universe u + + -- BEGIN + axiom choice {α : Sort u} : nonempty α → α + -- END + + end hide + + Here ``nonempty α`` is defined as follows: + + .. code-block:: lean + + namespace hide + universe u + + -- BEGIN + class inductive nonempty (α : Sort u) : Prop + | intro : α → nonempty + -- END + + end hide + + It is equivalent to ``∃ x : α, true``. + +The quotient construction implies function extensionality. The ``choice`` principle, in conjunction with the others, makes the axiomatic foundation classical; in particular, it implies the law of the excluded middle and propositional decidability. Functions that make use of ``choice`` to produce data are incompatible with a computational interpretation, and do not produce bytecode. They have to be declared ``noncomputable``. + +For metaprogramming purposes, Lean also allows the definition of objects which stand outside the object language. These are denoted with the ``meta`` keyword, as described in :numref:`Chapter %s `. diff --git a/doc/lexical_structure.md b/doc/lexical_structure.md new file mode 100644 index 0000000000..ad98c0f3c0 --- /dev/null +++ b/doc/lexical_structure.md @@ -0,0 +1,158 @@ +Lexical Structure +================= + +This section describes the detailed lexical structure of the Lean +language. Many readers will want to skip this section on a first +reading. + +Lean input is processed into a stream of tokens by its scanner, using +the UTF-8 encoding. The next token is the longest matching prefix of +the remaining input. + +``` + token: `symbol` | `command` | `ident` | `string` | `char` | `numeral` | + : `decimal` | `quoted_symbol` | `doc_comment` | `mod_doc_comment` | + : `field_notation` +``` + +Tokens can be separated by the whitespace characters space, tab, line +feed, and carriage return, as well as comments. Single-line comments +start with ``--``, whereas multi-line comments are enclosed by ``/-`` +and ``-/`` and can be nested. + +Symbols and Commands +==================== + +.. *(TODO: list built-in symbols and command tokens?)* + +Symbols are static tokens that are used in term notations and +commands. They can be both keyword-like (e.g. the :keyword:`have +` keyword) or use arbitrary Unicode characters. + +Command tokens are static tokens that prefix any top-level declaration +or action. They are usually keyword-like, with transitory commands +like :keyword:`#print ` prefixed by an additional +``#``. The set of built-in commands is listed in the :numref:`Chapter +%s ` section. + +Users can dynamically extend the sets of both symbols (via the +commands listed in :numref:`quoted_symbols`) and command tokens (via +the :keyword:`[user_command] ` attribute). + +.. _identifiers: + +Identifiers +=========== + +An *atomic identifier*, or *atomic name*, is (roughly) an alphanumeric +string that does not begin with a numeral. A (hierarchical) +*identifier*, or *name*, consists of one or more atomic names +separated by periods. + +Parts of atomic names can be escaped by enclosing them in pairs of French double quotes ``«»``. + +```lean + def Foo.«bar.baz» := 0 -- name parts ["Foo", "bar.baz"] +``` + +``` + ident: `atomic_ident` | `ident` "." `atomic_ident` + atomic_ident: `atomic_ident_start` `atomic_ident_rest`* + atomic_ident_start: `letterlike` | "_" | `escaped_ident_part` + letterlike: [a-zA-Z] | `greek` | `coptic` | `letterlike_symbols` + greek: <[α-ωΑ-Ωἀ-῾] except for [λΠΣ]> + coptic: [ϊ-ϻ] + letterlike_symbols: [℀-⅏] + escaped_ident_part: "«" [^«»\r\n\t]* "»" + atomic_ident_rest: `atomic_ident_start` | [0-9'ⁿ] | `subscript` + subscript: [₀-₉ₐ-ₜᵢ-ᵪ] +``` + +String Literals +=============== + +String literals are enclosed by double quotes (``"``). They may contain line breaks, which are conserved in the string value. + +``` + string : '"' `string_item` '"' + string_item : `string_char` | `string_escape` + string_char : [^\\] + string_escape: "\" ("\" | '"' | "'" | "n" | "t" | "x" `hex_char` `hex_char`) + hex_char : [0-9a-fA-F] +``` + +Char Literals +============= + +Char literals are enclosed by single quotes (``'``). + +``` + char: "'" `string_item` "'" +``` + +Numeric Literals +================ + +Numeric literals can be specified in various bases. + +``` + numeral : `numeral10` | `numeral2` | `numeral8` | `numeral16` + numeral10 : [0-9]+ + numeral2 : "0" [bB] [0-1]+ + numeral8 : "0" [oO] [0-7]+ + numeral16 : "0" [xX] `hex_char`+ +``` + +Decimal literals are currently only being used for some :keyword:`set_option ` values. + + +``` + decimal : [0-9]+ "." [0-9]+ +``` + +Quoted Symbols +============== + +In a fixed set of commands (:keyword:`notation +`, :keyword:`local notation +`, and :keyword:`reserve +`), symbols (known or unknown) can be quoted by +enclosing them in backticks (`````). Quoted symbols are used by these +commands for registering new notations and symbols. + +``` + quoted_symbol : "`" " "* `quoted_symbol_start` `quoted_symbol_rest`* " "* "`" + quoted_symbol_start: [^0-9"\n\t `] + quoted_symbol_rest : [^"\n\t `] +``` + +A quoted symbol may contain surrounding whitespace, which is +customarily used for pretty printing the symbol and ignored while +scanning. + +While backticks are not allowed in a user-defined symbol, they are +used in some built-in symbols (see :ref:`quotations`), which are +accessible outside of the set of commands noted above. + +Doc Comments +============ + +A special form of comments, doc comments are used to document modules +and declarations. + +``` + doc_comment: "/--" ([^-] | "-" [^/])* "-/" + mod_doc_comment: "/-!" ([^-] | "-" [^/])* "-/" +``` + +Field Notation +============== + +Trailing field notation tokens are used in expressions such as +``(1+1).to_string``. Note that ``a.toString`` is a single +:ref:`identifier `, but may be interpreted as a field +notation expression by the parser. + +``` + field_notation: "." ([0-9]+ | `atomic_ident`) +``` diff --git a/doc/metaprogramming.md b/doc/metaprogramming.md new file mode 100644 index 0000000000..c3ac672896 --- /dev/null +++ b/doc/metaprogramming.md @@ -0,0 +1 @@ +# Metaprogramming diff --git a/doc/mission.md b/doc/mission.md new file mode 100644 index 0000000000..0cc211aabd --- /dev/null +++ b/doc/mission.md @@ -0,0 +1,12 @@ +Mission +======= + +Empower software developers to design, develop, and reason about programs. +Empower mathematicians and scientists to design, develop, and reason about formal models. + +How +--- + +Lean is an efficient functional programming language based on dependent type theory. +It is under heavy development, but it already generates very efficient code. +It also has a powerful meta-programming framework, extensible parser, and IDE support based on LSP. diff --git a/doc/using_lean.md b/doc/using_lean.md new file mode 100644 index 0000000000..a9b4c8233b --- /dev/null +++ b/doc/using_lean.md @@ -0,0 +1 @@ +# Using Lean