* doc: add documentation on functors.
* fix: make comments green
* minor tweaks
* doc: add section on Applicatives.
* doc: add some more info on the laws from Mario.
* doc: add law list and move lazy evaluation up so the chapter ends properly.
* doc: Add something on seqLeft and seqRight.
* doc: add section on monads.
* doc: fix some typos.
* doc: switch to LeanInk for chaper on Monads.
* doc: remove old files.
* doc: fix mdbook test errors.
* doc: add part 4: readers
* doc: add section on State monads
* doc: fix some typos and add some more details.
* doc: fix typos and add some CR feedback.
* doc: add Except monad section.
* doc: add info on monad transformers.
* Delete transformers.lean.md
* doc: fix some typos.
* doc: fix typos and move forward reference to monad lifting.
* doc: Update `State` to `StateM`
* doc: fix references to State to become StateM.
* doc: generalize indexOf implementation.
* doc: add chapter on monad laws and move "law" sections to this chapter to avoid redundancy.
* doc: add theorem
* Delete laws.lean.md
* doc: fix some typos.
* doc: fix broken link.
* doc: fox typos.
* fix: language changed from "us" to "you".
* doc: fix code review comments.
* doc: some word smithing
* doc: some word smithing and sample simplification.
* doc: add bad_option_map example.
* doc: add side note on `return` statement and fix heading level consistency.
* Add `withReader` info
* doc: change language from us, our, your, we, we'll, we've to "you"
* doc: add some forward links.
* doc: put spaces around colon in function arguments like "(x : List Nat)"
* doc:
Add backticks on map
Remove commands on multiline structure instance
Fix centerdot
Add "one of"
* doc: Remove info about Functor in other languages.
* doc:
add info on <$> being left associative
remove another forward reference to monad
fix typo `operatoions`
remove unneccesary parens after <$>
* doc:
fix Type u -> Type v
fix you -> your
use `let val? ← IO.getEnv name`
in Readers call it "context" rather than "state".
* doc: fix withReader docs
use 'context' to describe the ReaderM state.
remove "trivial"
type inference => Lean
"abstract classes" => "abstract structures"
remove unnecessary parens
* doc: fix bug in explanation of `let x ← readerFunc2`
Fix explanation of equivalence between `def f (a : Nat) : String` and `def f : Nat → String`
* doc: move hasSomeItemGreaterThan to Except.lean
Add validateList List.anyM example.
fix `def f (a : Nat) : String` language.
* doc: fix "What transformation are you referring to"
* doc: fix typo.
* doc: add missing period.
* doc: fix validateList
* doc: explain `λ` notation.
* doc: reword the map, seq, bind comparison.
* doc: fix some more 'reader state' to 'reader context' language
* doc: fix wrote statement about return only works in do blocks.
* doc: fix typo
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* doc: improve language
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* doc: fix typo
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* Add info on what a do block is doing for you.
* doc: define definitionally equal
* doc: make `readerFunc3.run env` canonical.
* doc: remove unnecessary parens.
* doc: fix typos
* doc: make List.map a bit more clear in the intro to Functors.
* doc: simplify readerFunc3WithReader
* doc: switch to svg for diagram so it works better on dark themes.
* doc: align nodes in diagram and convert to svg.
* doc: simplify playGame using while true.
* doc: drop confusing statement about "definitionally equal"
* doc: switch to `import Lean.Data.HashMap`
* doc: fix typo "operatoins"
* doc: update diagram to add more info and polish the intro paragraphs so they better match the actual contents of each chapter.
* doc: fix typo
* doc: fix typo.
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Lean.Meta.forEachExpr should be general over monads rather than restricted to the MetaM monad.
This is similar to the generalisation of Lean.Meta.transform
`charToHex` is an auxiliary function used at `Char.quoteCore` for
converting ASCII control characters into `\x` notation.
Its name was misleading.
Closes#1404
Motivation: it is not very useful anymore, and more importantly it
breaks all the time because it is affected by how many internal ids
are created by Lean.
* doc: Add explanations to MetavarContext
The explanations were taken from Leo's talk at the ICERM
Mathlib porting hackathon.
* Update src/Lean/MetavarContext.lean
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
* add my understanding of what LocalInstances represents
* Update src/Lean/MetavarContext.lean
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Leonardo de Moura <leonardo@microsoft.com>
* doc: Add explanations to MetavarContext
The explanations were taken from Leo's talk at the ICERM
Mathlib porting hackathon.
* doc: Add documentation for Declaration
This is explanations taken from Leo's talk given
at the post ICERM Mathlib porting hackathon.
* Update src/Lean/Declaration.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* Update src/Lean/Declaration.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* Update src/Lean/MetavarContext.lean
Co-authored-by: Scott Morrison <scott@tqft.net>
* fix depth comment
Co-authored-by: Scott Morrison <scott@tqft.net>
We don't try to reuse the cache contents between different `isDefEq`
calls. Thus, we can cache more results and ignore whether the state of
the metavariable context affects them or not.
Closes#1102
see #1248
This commit adds a small hack to fix the term info for the following `do`-elements
```lean
let (x, y) := ...
let (x, y) ← ...
let mut (x, y) ← ...
let some x ← ... | ...
```
We want to be able to update `InfoState` at `AttrM` which is just an
alias for `CoreM`.
I considered defining `AttrM` as `StateRefT InfoState CoreM`, but this
is problematic because we also want to invoke `AttrM` monadic
actions from `MetaM`.
Closes#1350
> Heather suggested changing the calc tactic (not the term) such that if
the final RHS does not defeq match the goal RHS, it returns a final
inequality as a subgoal.
Closes#1342
This commit fixes bug reported by Patrick Massot.
It happened when using `macro_rules` and `elab_rules` for the same
`SyntaxNodeKind`.
It also fixes missing error messages when there is more than one
elaboration functions and there is `abortTactic` exception.
Remark: this commit also changes the evaluation order. Macros are
now tried before elaboration rules. The motivation is that macros are
already applied before elaboration functions in the term elaborator.
Add support for operators that may not have homogeneous instances for
all types. For example, we have `HPow Nat Nat Nat` and `HPow Int Nat Int`,
but we don't have `HPow Int Int Int`.
Note that test for issue #1200 broke.
The bug fixed by this commit was allowing the example to be elaborated
correctly :(
Initially, the type of the discriminant is not available, and
`.none (α:=α)` can only be elaborated when the expected type is of the
form `C ...`. Lean then tries to elaborate the alternatives, learn
that the discriminant should be `Option ?m`, and fails because the
patterns still have metavariables after elaboration. Before the bug
fix, `resumePostpone` was **not** restoring the metavariable context,
and the assingnment would stay there. With this information, Lean
can now elaborate `.none (α:=α)`.
Although the bug had a positive impact in this case, it produced
incorrect behavior in other examples.
The fixed example looks reasonable. Thus, we will not reopen
issue #1200
Motivation: make sure the behavior is consistent with other arithmetic
operators.
This commit also removes the instance
```
instance : HMod (Fin n) Nat (Fin n) where
hMod := Fin.modn
```
because we have a coercion from `Fin n` to `Nat`.
Thus, given `a : Fin n` and `b : Nat`, `a % b` is ambiguous.
We need this refinement for declarations such as
```
def add_one {X} [Trait X] [One (Trait.R X)] [HAdd X (Trait.R X) X] (x : X) : X := x + (One.one : (Trait.R X))
```
from test 948.lean
The old error message said:
```
throwError "invalid `▸` notation,
expected type{indentExpr expectedType}\ndoes contain
equation left-hand-side nor right-hand-side{indentExpr heqType}"
```
The phrase `does contain ... nor ..` seems gramatically incorrect.
What was (probably) intended was `does **not** contain ... nor ...`.
We take the opportunity to clean up the error message and
be clearer that the equality does not contain the expected result type.
In order to guarantee termination of type class synthesis when resolving
coercions, a good rule of thumb is that the instances should not
introduce metavariables (during TC synthesis). For common coercion type
classes this means:
- `Coe T S`, `CoeTail T S`: the variables of `T` must be a subset of those of `S`
- `CoeHead T S`: the variables of `S` must be a subset of those of `T`
If these rules are not followed, we can easily get nontermination. In
this case: `CoeTC Foo Syntax` is reduced to `CoeTC Foo (TSyntax ?m_1)`
using the (dangerous) `Coe (TSyntax k) Syntax` instance, to which we can
then apply the otherwise fine `Coe (TSyntax [k]) (TSyntax (k'::ks))`
coercion infinitely often.
When solving `a.i =?= b.i`, we first reduce `a` and `b` without using
delta reduction. If at least one become a structure, we reduce the
projection. Otherwise, we try to solve `a =?= b`, only reduce `a.i`
and `b.i` if it fails.
This commit fixes issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/deterministic.20timeout/near/287654818
Type class resolution was diverging when trying to synthesize
```lean
HSub (optParam Float 0.0) (optParam Float 1.0) ?m.472
```
and Lean was diverging while unfolding
```lean
instance : OfScientific Float where
ofScientific m s e :=
if s then
let s := 64 - m.log2 -- ensure we have 64 bits of mantissa left after division
let m := (m <<< (3 * e + s)) / 5^e
Float.ofBinaryScientific m (-4 * e - s)
else
Float.ofBinaryScientific (m * 5^e) e
```
was being unfolded.
Anothe potential solution for the problem above is to erase the
`optParam` annotations before performing type class resolution.
Most notable change: `Quote` is now parameterized by the target kind.
Which means that `Name` etc. could actually have different
implementations for quoting into `term` and `level`, if that need ever
arises.
Instead of the previous constraints on the right hand side that only
allowed a permutation of variables as parameters to a function the
new heuristic allows anything to the right of a function as long as
each variable only appears at most once.
They are all in `MetaM`.
These are helper functions for issue #1237. We need to "cleanup" the
local context before trying to compile the match-expression.
see issue #1237
Lean.Meta.transform is created with a series of recursive
visit functions. However these visit functions are useful
on their own outside of transform for traversing expressions.
This commit moves the visit functions outside the main function.
This is used to uniquely identify InteractiveGoals and
InteractiveHypotheses. This makes it easier to do
contextual suggestions: eg the infoview can send a message
saying "the user clicked on subexpression 5 in hypothesis N in goal G"
where N and G are unique identifiers for a goal rather than pretty names
which may be non-unique or indices which may be difficult to compute
(eg in infoview there is a mode where hypotheses are reversed or filtered).
While adding these I also refactored the InteractiveGoal generating function.
I unwrapped a fold in to a for/in loop with mutating variables which is a
little easier to read.
The error message is far from perfect, but it is better than ignoring
the issue and failing later with an even more incomprehensible error
message.
see #1179
- ignore unused variables in dep arrows
- avoid negated options
- make syntax stack generation more performant
- make ignore functions more extensible
- change message severity to `warning`
See discussion at https://github.com/leanprover/vscode-lean4/issues/76
We also use `pp.inaccessibleNames = false` in error messages. In this
setting, an inaccessible name is displayed in the context only if the
target type depends on it.
The derive handler for `DecidableEq` does not currently support proofs
in constructor arguments/structure fields. For example, deriving
`DecidableEq` for `Fin n` will fail, because of the field `isLt`. This
change checks whether the elements being tested are proofs, and if so,
changes the equality proof to just `rfl`.
Functions can now be marked with the `@[rpc]` attribute, which
registers the function as an RpcProcedure that can be used to
communicate with the code editor and infoview.
```
def mutVariableDo2 (list : List Nat) : Nat := Id.run <| do
let mut sum := 0
for _ in list do
sum := sum.add 1 -- first `sum` was not connected, i.e., it was not highlighted when hovering over the second `sum`
pure sum
```
Fixed by adding the identifier's module as an argument to referringTo.
If the ident is RefIdent.const, this is ignored, but if it is
RefIdent.fvar, referringTo limits its search to the ident's module.
Right now, it only supports the following kind of definitions
- Recursive definitions that support smart unfolding.
- Non-recursive definitions where the body is a match-expression. This
kind of definition is only unfolded if the match can be reduced.
At the moment InfoTree has a constructor ofJson but this means that
you can't have a non-leaf ofJson. It would be better to have `ofJson` be a constructor of `Info`.
This is what this PR does.
Then `isClassExpensive?` was being invoked too often. In some
benchmarks the performance hit was substantial. For example,
in the new test `state8.lean`. The runtime on my machine went from 2s
to 0.76s.
We annotate patterns with the corresponding `Syntax` during
elaboration, and do not populate the info tree. Reason: the set of
pattern variables is not known during pattern elaboration.
It was in the context of `withInductiveLocalDecls`. This introduced
unnecessary `_root_` in the info view and hover information.
For example, when hovering over
```lean
inductive Ty where
| int
| bool
| fn (a r : Ty)
```
We would get `Ty.int : _root_.Ty` when hovering over the `int`.
The issue was raised on Zulip. The issue is triggered in
declarations containing overlapping patterns and nested recursive
definitions occurring as the discriminant of `match`-expressions.
Recall that Lean 4 generates conditional equations for declarations
containing overlapping patterns.
To address the issue we had to "fold" `WellFounded.fix` applications
back as recursive applications of the functions being defined.
The new test exposes the issue.
stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.
This commit fixes the last issue exposed by #1074fixes#1074
see #371
This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
| S (s : String)
| I (i : Int)
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a => toString a
| S a => toString a
```
We must search the environment extension first, and then the builtin
table. Otherwise, the builtin declarations do not change when we
modify the files.
closes#1021
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.
Closes#1045
This fix may impact performance. Note that we don't need to flush the
cache if we are "adding" stuff to the environment. We only need to
flush the caches if the change is not monotonic. BTW, most of the
changes are monotonic. I think this is why we did not hit this bug before.
We may also move all these caches to an environment extension. It is
an easy way to make sure we preserve the cache when extending the
environment.
I tried a few benchmarks and did not notice a significant difference.
cc @kha @gebner
fixes#1051
We are considering removing `.` as an alternative for `·` in the
lambda dot notation (e.g., `(·+·)`).
Reasons:
- `.` is not a perfect replacement for `·` (e.g., `(·.insert ·)`)
- `.` is too overloaded: `(f.x)` and `(f .x)` and `(f . x)`. We want to keep the first two.
We don't use the following hack anymore:
- /- HACK: `fvarId` is not in the scope of `mvarId`
- If this generates problems in the future, we should update the metavariable declarations. -/
- assignExprMVar mvarId (mkFVar fvarId)
This hack was corrupting the `InfoTree`.
for regression introduced by the following change
* Auto implicit behavior changed for inductive families. An auto implicit argument occurring in inductive family index is also treated as an index (IF it is not fixed, see next item)
This modification is relevant for fixing regressions on recent changes
to the auto implicit behavior for inductive families.
The following declarations are now accepted:
```lean
inductive HasType : Fin n → Vector Ty n → Ty → Type where
| stop : HasType 0 (ty :: ctx) ty
| pop : HasType k ctx ty → HasType k.succ (u :: ctx) ty
inductive Sublist : List α → List α → Prop
| slnil : Sublist [] []
| cons l₁ l₂ a : Sublist l₁ l₂ → Sublist l₁ (a :: l₂)
| cons2 l₁ l₂ a : Sublist l₁ l₂ → Sublist (a :: l₁) (a :: l₂)
inductive Lst : Type u → Type u
| nil : Lst α
| cons : α → Lst α → Lst α
```
TODO: universe inference for `inductive` should be improved. The
current approach is not good enough when we have auto implicits.
TODO: allow implicit fixed indices that do not depend on indices that
cannot be moved to become parameters.
TODO: convert fixed indices to parameters. Motivation: types such as
```lean
inductive Foo : List α → Type
| mk : Foo []
```
Users should not need to write
```lean
inductive Foo {α} : List α → Type
| mk : Foo []
```
- Wait for all terms to be elaborated before showing folding regions.
May want to change this to support partial results.
- Use .span to extract import statements, rather than mutually
recursive functions.
- Some tiny other bits of cleanup
The new test exposes the problem fixed by this commit.
In the termination proof we have two `sizeOf xs` terms that are not
syntactically identical (only definitional equal) because the
instances are different.
The issue is only going to be properly fixed when we rewrite `csimp`
in Lean. The `csimp` performs transformations that do not preserve
typability, but it also uses the kernel `infer_type` which assumes the
input is type correct. In the new `csimp`, we must have a different
`infer_type` which returns an `Any` type in this kind of situation.
The workaround in this commit simply disables optimizations when
`infer_type` fails. It does not fix all occurrences of this problem,
but the two places that issue #1030 triggered.
closes#1030
We use the idiom `revert; simp; ...; intro` in a few places. Some of
the reverted hypotheses manifest themselves as arrows in the target.
Before this commit, `simp` would lose the binder names and info when
simplifying an arrow, and we would get inaccessible names when
reintroducing them.
They are useful for getting meaningful pattern variable names when the hole
is not an inaccessible pattern. See new test.
We are going to use this feature to address issue 2 at #1018.
It is used by the `noConfusionType` construction for enumeration types,
and we want it to reduce even when the reducibility setting is
`TransparencyMode.reducible` as for other inductive types.
see issue #1016
Reason: avoid unnecessary case-analysis explosion
It is also unnecessary since we only refine the `below` and `F`
arguments over `match`-expressions.
This fixes the last case at issue #998
```
attribute [simp] BinaryHeap.heapifyDown
```
closes#998
Use zeta reduction to create new opportunities of beta-reduction.
This issue fixes on the problems that were affecting the generation of
equation theorems for `Array.heapSort.loop` (see issue: #998).
After this fix, the equation theorem generation fails at `splitMatch`.
In the last dev meeting, we have decided we are not going to use it.
We will release often (every month), and use pull requests and issues
to report changes.
Not only is this more semantically appropriate (see e.g.
`/usr/src/{linux,rust,...}` on Debian), it also prevents .ilean files
from Lake tests (which are symlinked into the build directory as part of
`src/` during development) from ending up in the built-in LEAN_PATH and
being watched & loaded by the server.
On issue #906, `simp` spends a lot of time checking the cache. This
process is time consuming and doesn't allocate memory. Before this
commit, it would take a long time to get the "maximum number of
heartbeats" error message on the example included in this issue.
Closes#906
It was just making it stop simplification at the current branch.
Now, elaboration is interrupted after a few seconds in the example at
issue #906.
see #906
* use `-nostdinc` to make sure system headers don't affect us
* include clang headers with `-isystem`, which suppresses all those warnings
* do not use default sysroot on Windows after all, since that can be a
surprising location
Fixes#922
We want to specialize functions such as
```
def find? {_ : BEq α} {_ : Hashable α} : PersistentHashMap α β → α → Option β
| { root := n, .. }, k => findAux n (hash k |>.toUSize) k
```
This change has no effect on the server behavior. The only difference
is that the filename now shows up in `htop`, `ps`, etc., which makes it much
easier to see what Lean processes are running, and which are using 100%
CPU, etc.
At the time erase_irrelevant is called, we have already eliminated the
`cast`-applications. Therefore non-atomic expressions may no longer
be well-typed (and `infer_type` can fail).
Previously automatically generated delaborators for syntax declared with
the notation (and derived) keywords would silently drop information
during delaboration.
Add an option called pp.tagSymbols which, if set, makes the
delaborator add term information to all symbols it can during
delaboration. This option is disabled per default because it would
break the LSP server's hovering behaviour. It is however useful
when for example automatically generating interactive documentation.
Without this change, enqueuing multiple tasks before the first worker
was started led to only a single worker being created. Now the first
increment and decrement happen under the task manager mutex, so
effectively the worker is never idle until it is out of tasks.
We might also want to replace them with fresh vars to make the hover
completely independent of the context, but this change at least avoids
any hidden information.
# squelch error message about missing nixpkgs channel
NIX_BUILD_SHELL:bash
LSAN_OPTIONS:max_leaks=10
# somehow MinGW clang64 (or cmake?) defaults to `g++` even though it doesn't exist
CXX:c++
steps:
- name:Checkout
uses:actions/checkout@v2
with:
# interferes with lean4-nightly authentication
persist-credentials:false
submodules:true
- name:Install Nix
uses:cachix/install-nix-action@v15
@@ -84,7 +131,8 @@ jobs:
uses:msys2/setup-msys2@v2
with:
msystem:clang64
install:make python mingw-w64-clang-x86_64-cmake mingw-w64-clang-x86_64-clang mingw-w64-clang-x86_64-ccache git zip unzip diffutils binutils tree mingw-w64-clang-x86_64-zstd tar
# `:p` means prefix with appropriate msystem prefix
pacboy:"make python cmake:p clang:p ccache:p gmp:p git zip unzip diffutils binutils tree zstd:p tar"
@@ -74,7 +74,7 @@ Lean provides ways of adding new objects to the environment. The following provi
* ``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 `α`
* ``opaque 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.
@@ -89,8 +89,8 @@ Any of ``def``, ``theorem``, ``axiom``, or ``example`` can take a list of argume
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
opaque c : Nat
opaque d : Nat
axiom cd_eq : c = d
def foo : Nat := 5
@@ -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)
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.
| 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.
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
| (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,42 @@ 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:
```lean
def foo (ns ms : List Nat) (h1 : ns ++ ms ≠ []) (k : Nat -> Char) : Char :=
match h2 : ns ++ ms with
-- in this arm, we have the hypothesis `h2 : ns ++ ms = []`
| [] => absurd h2 h1
-- in this arm, we have the hypothesis `h2 : ns ++ ms = h :: t`
| h :: t => k h
-- '7'
#eval foo [7, 8, 9] [] (by decide) Nat.digitChar
```
.. _structures_and_records:
@@ -684,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 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ᵢ : βᵢ`` :
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)
#checkfoo
#check@foo.mk
#check@foo.rec
#checkFoo
#check@Foo.mk
#check@Foo.rec
#checkfoo.a
#checkfoo.n
#checkfoo.b
#checkFoo.a
#checkFoo.n
#checkFoo.b
#checkbaz
#check@baz.mk
#check@baz.rec
#checkBaz
#check@Baz.mk
#check@Baz.rec
#checkbaz.to_foo
#checkbaz.to_bar
#checkbaz.v
#checkBaz.toFoo
#checkBaz.toBar
#checkBaz.v
def bzz := vec.mk [1, 2, 3] rfl
def bzz := Vec.mk [1, 2, 3] rfl
#checkvec.l bzz
#checkvec.h bzz
#checkVec.l bzz
#checkVec.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
* `interpreter`: full execution trace of the interpreter. Only available in debug builds.
In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message directly to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
In pure contexts or when execution is aborted before the messages are finally printed, one can instead use the term `dbg_trace "msg with {interpolations}"; val` (`;` can also be replaced by a newline), which will print the message to stderr before evaluating `val`. `dbgTraceVal val` can be used as a shorthand for `dbg_trace "{val}"; val`.
Note that if the return value is not actually used, the trace code is silently dropped as well.
In the language server, stderr output is buffered and shown as messages after a command has been elaborated, unless the option `server.stderrAsMessages` is deactivated.
@@ -43,6 +43,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
* it is none of the types described above
* it is not marked `unsafe`
* it has a single constructor with a single parameter of *relevant* type
is represented by the representation of that parameter's type.
For example, `{ x : α // p }`, the `Subtype` structure of a value of type `α` and an irrelevant proof, is represented by the representation of `α`.
@@ -66,33 +67,45 @@ Return values and `@[export]` parameters are always owned at the moment.
## Initialization
When including Lean code as part of a larger program, modules must be *initialized* before accessing any of their declarations.
Module initialization entails
* initialization of all "constants" (nullary functions), including closed terms lifted out of other functions
* execution of all `[init]` functions
* execution of all `[builtinInit]` functions, if the `builtin` parameter of the module initializer has been set
The module initializer is automatically run with the `builtin` flag for executables compiled from Lean code and for "plugins" loaded with `lean --plugin`.
For all other modules imported by `lean`, the initializer is run without `builtin`.
Thus `[init]` functions are run iff their module is imported, regardless of whether they have native code available or not, while `[builtinInit]` functions are only run for native executable or plugins, regardless of whether their module is imported or not.
`lean` uses built-in initializers for e.g. registering basic parsers that should be available even without importing their module (which is necessary for bootstrapping).
The initializer for module `A.B` is called `initialize_A_B` and will automatically initialize any imported modules.
Module initializers are idempotent, but not thread-safe.
Module initializers are idempotent (when run with the same `builtin` flag), but not thread-safe.
Together with initialization of the Lean runtime, you should execute code like the following exactly once before accessing any Lean declarations:
You will notice there is a `stage0` folder. This is for bootstrapping
the compiler development. Generally you do not change any code in
`stage0` manually. It is important that you read [bootstrapping
pipeline](bootstrap.md) so you understand how this works.
If you want to make changes to Lean itself, start by [building Lean](../make/index.html) from a clean checkout to make sure that everything is set up correctly.
After that, read on below to find out how to set up your editor for changing the Lean source code, followed by further sections of the development manual where applicable such as on the [test suite](testing.md) and [commit convention](commit_convention.md).
The dev team uses `elan` to manage which `lean` toolchain to use
locally and `elan` can be used to setup the version of Lean you are
manually building. This means you generally do not use `make
install`. You use `elan` instead.
If you are planning to make any changes that may affect the compilation of Lean itself, e.g. changes to the parser, elaborator, or compiler, you should first read about the [bootstrapping pipeline](bootstrap.md).
You should not edit the `stage0` directory except using the commands described in that section when necessary.
## Development Setup
You can use any of the [supported editors](../setup.md) for editing
the Lean source code. If you set up `elan` as below, opening `src/` as
a *workspace folder* should ensure that stage 0 will be used for file
in that directory.
You can use any of the [supported editors](../setup.md) for editing the Lean source code.
If you set up `elan` as below, opening `src/` as a *workspace folder* should ensure that stage 0 (i.e. the stage that first compiles `src/`) will be used for files in that directory.
## Dev setup using elan
### Dev setup using elan
You can use [`elan`](https://github.com/leanprover/elan) to easily
switch between stages and build configurations based on the current
directory, both for the `lean`, `leanc`, and `leanmake` binaries in your shell's
PATH and inside your editor.
To install elan, you can do so, without installing a default version of Lean, using
To install elan, you can do so, without installing a default version of Lean, using (Unix)
```bash
[Unix]
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none
Inside a `do` block, the pattern `let _ ← <success> | <fail>` will continue with the rest of the block if the match on the left hand side succeeds, but will execute the right hand side and exit the block on failure:
If the type of keys can be totally ordered -- that is, it supports a well-behaved `≤` comparison --
then maps can be implemented with binary search trees (BSTs). Insert and lookup operations on BSTs take time
proportional to the height of the tree. If the tree is balanced, the operations therefore take logarithmic time.
This example is based on a similar example found in the ["Sofware Foundations"](https://softwarefoundations.cis.upenn.edu/vfa-current/SearchTree.html)
book (volume 3).
-/
/-!
We use `Nat` as the key type in our implementation of BSTs,
since it has a convenient total order with lots of theorems and automation available.
We leave as an exercise to the reader the generalization to arbitrary types.
-/
inductiveTree(β:Typev)where
|leaf
|node(left:Treeβ)(key:Nat)(value:β)(right:Treeβ)
derivingRepr
/-!
The function `contains` returns `true` iff the given tree contains the key `k`.
-/
defTree.contains(t:Treeβ)(k:Nat):Bool:=
matchtwith
|leaf=>false
|nodeleftkeyvalueright=>
ifk<keythen
left.containsk
elseifkey<kthen
right.containsk
else
true
/-!
`t.find? k` returns `some v` if `v` is the value bound to key `k` in the tree `t`. It returns `none` otherwise.
-/
defTree.find?(t:Treeβ)(k:Nat):Optionβ:=
matchtwith
|leaf=>none
|nodeleftkeyvalueright=>
ifk<keythen
left.find?k
elseifkey<kthen
right.find?k
else
somevalue
/-!
`t.insert k v` is the map containing all the bindings of `t` along with a binding of `k` to `v`.
-/
defTree.insert(t:Treeβ)(k:Nat)(v:β):Treeβ:=
matchtwith
|leaf=>nodeleafkvleaf
|nodeleftkeyvalueright=>
ifk<keythen
node(left.insertkv)keyvalueright
elseifkey<kthen
nodeleftkeyvalue(right.insertkv)
else
nodeleftkvright
/-!
Let's add a new operation to our tree: converting it to an association list that contains the key--value bindings from the tree stored as pairs.
If that list is sorted by the keys, then any two trees that represent the same map would be converted to the same list.
Here's a function that does so with an in-order traversal of the tree.
-/
defTree.toList(t:Treeβ):List(Nat×β):=
matchtwith
|leaf=>[]
|nodelkvr=>l.toList++[(k,v)]++r.toList
#evalTree.leaf.insert2"two"
|>.insert3"three"
|>.insert1"one"
#evalTree.leaf.insert2"two"
|>.insert3"three"
|>.insert1"one"
|>.toList
/-!
The implemention of `Tree.toList` is inefficient because of how it uses the `++` operator.
On a balanced tree its running time is linearithmic, because it does a linear number of
concatentations at each level of the tree. On an unbalanced tree it's quadratic time.
Here's a tail-recursive implementation than runs in linear time, regardless of whether the tree is balanced:
-/
defTree.toListTR(t:Treeβ):List(Nat×β):=
got[]
where
go(t:Treeβ)(acc:List(Nat×β)):List(Nat×β):=
matchtwith
|leaf=>acc
|nodelkvr=>gol((k,v)::goracc)
/-!
We now prove that `t.toList` and `t.toListTR` return the same list.
The proof is on induction, and as we used the auxiliary function `go`
to define `Tree.toListTR`, we use the auxiliary theorem `go` to prove the theorem.
The proof of the auxiliary theorem is by induction on `t`.
The `generalizing acc` modifier instructs Lean to revert `acc`, apply the
induction theorem for `Tree`s, and then reintroduce `acc` in each case.
By using `generalizing`, we obtain the more general induction hypotheses
- `left_ih : ∀ acc, toListTR.go left acc = toList left ++ acc`
- `right_ih : ∀ acc, toListTR.go right acc = toList right ++ acc`
Recall that the combinator `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal,
concatenating all goals produced by `tac'`. In this theorem, we use it to apply
`simp` and close each subgoal produced by the `induction` tactic.
The `simp` parameters `toListTR.go` and `toList` instruct the simplifier to try to reduce
and/or apply auto generated equation theorems for these two functions.
The parameter `*` intructs the simplifier to use any equation in a goal as rewriting rules.
In this particular case, `simp` uses the induction hypotheses as rewriting rules.
Finally, the parameter `List.append_assoc` intructs the simplifier to use the
`List.append_assoc` theorem as a rewriting rule.
-/
theoremTree.toList_eq_toListTR(t:Treeβ)
:t.toList=t.toListTR:=by
simp[toListTR,got[]]
where
go(t:Treeβ)(acc:List(Nat×β))
:toListTR.gotacc=t.toList++acc:=by
inductiontgeneralizingacc<;>
simp[toListTR.go,toList,*,List.append_assoc]
/-!
The `[csimp]` annotation instructs the Lean code generator to replace
any `Tree.toList` with `Tree.toListTR` when generating code.
-/
@[csimp]theoremTree.toList_eq_toListTR_csimp
:@Tree.toList=@Tree.toListTR:=by
funextβt
applytoList_eq_toListTR
/-!
The implementations of `Tree.find?` and `Tree.insert` assume that values of type tree obey the BST invariant:
for any non-empty node with key `k`, all the values of the `left` subtree are less than `k` and all the values
of the right subtree are greater than `k`. But that invariant is not part of the definition of tree.
So, let's formalize the BST invariant. Here's one way to do so. First, we define a helper `ForallTree`
to express that idea that a predicate holds at every node of a tree:
-/
inductiveForallTree(p:Nat→β→Prop):Treeβ→Prop
|leaf:ForallTreep.leaf
|node:
ForallTreepleft→
pkeyvalue→
ForallTreepright→
ForallTreep(.nodeleftkeyvalueright)
/-!
Second, we define the BST invariant:
An empty tree is a BST.
A non-empty tree is a BST if all its left nodes have a lesser key, its right nodes have a greater key, and the left and right subtrees are themselves BSTs.
-/
inductiveBST:Treeβ→Prop
|leaf:BST.leaf
|node:
ForallTree(funkv=>k<key)left→
ForallTree(funkv=>key<k)right→
BSTleft→BSTright→
BST(.nodeleftkeyvalueright)
/-!
We can use the `macro` command to create helper tactics for organizing our proofs.
The macro `have_eq x y` tries to prove `x = y` using linear arithmetic, and then
immediately uses the new equality to substitute `x` with `y` everywhere in the goal.
The modifier `local` specifies the scope of the macro.
-/
/-- The `have_eq lhs rhs` tactic (tries to) prove that `lhs = rhs`,
@@ -219,10 +219,10 @@ def f2 (a b c : Bool) : Bool :=
#eval (1, 2)
def p : Nat × Bool := (1,
def p : Nat × Bool := (1, false)
section
variables (a b c : Nat) (p : Nat × bool)
variable (a b c : Nat) (p : Nat × bool)
#check (1, 2)
#check p.1 * 2
@@ -232,8 +232,8 @@ end
/- lists -/
section
variables x y z : Nat
variables xs ys zs : list Nat
variable x y z : Nat
variable xs ys zs : list Nat
open list
#check (1 :: xs) ++ (y :: zs) ++ [1,2,3]
@@ -243,7 +243,7 @@ end
/- sets -/
section
variables s t u : set Nat
variable s t u : set Nat
#check ({1, 2, 3} ∩ s) ∪ ({x | x < 7} ∩ t)
end
@@ -276,7 +276,7 @@ Finally, for data types with one constructor, one destruct an element by pattern
.. code-block:: lean
universes u v
variables {α : Type u} {β : Type v}
variable {α : Type u} {β : Type v}
def p : Nat ×ℤ := ⟨1, 2⟩
#check p.fst
@@ -369,7 +369,7 @@ Here is an example:
.. code-block:: lean
variables (a b c d e : Nat)
variable (a b c d e : Nat)
variable h1 : a = b
variable h2 : b = c + 1
variable h3 : c = d
@@ -419,33 +419,31 @@ Every computable definition in Lean is compiled to bytecode at definition time.
.. code-block:: lean
#reduce (λ x, x + 3) 5
#eval (λ x, x + 3) 5
#reduce (fun x => x + 3) 5
#eval (fun x => x + 3) 5
#reduce let x := 5 in x + 3
#eval let x := 5 in x + 3
#reduce let x := 5; x + 3
#eval let x := 5; 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)
#reduce @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
| 0 => 0
| (n+1) => g n + n + 1
#reduce g 5
#eval g 5
#eval g 50000
#eval g 5000
example : (λ x, x + 3) 5 = 8 := rfl
example : (λ x, f x) = f := rfl
example : (fun x => x + 3) 5 = 8 := rfl
example : (fun 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 [Inductive Types](inductive.md).
The goal of [this book](https://leanprover.github.io/functional_programming_in_lean/) is to be an accessible introduction to using Lean 4 as a programming language.
It should be useful both to people who want to use Lean as a general-purpose programming language and to mathematicians who want to develop larger-scale proof automation but do not have a background in functional programming.
It does not assume any background with functional programming, though it's probably not a good first book on programming in general.
New content will be added once per month until it's done.
<pathd="M -807.881999182059,-412 L -847.12242702921,-475.387638592472"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -851.859658804052,-483.04 L -849.997117457574,-472.431939869483 C -848.256110200696,-474.68582647768 -845.988743857725,-476.089450707263 -843.19501842866,-476.642812558231 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Applicative->Pure">
<pathd="M -796.388009621993,-412 L -779.775946795781,-474.343439288465"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -777.458657044673,-483.04 L -783.898561528809,-474.407061321009 C -781.064326160453,-474.686741473815 -778.487567431109,-474.000137103116 -776.168285340778,-472.347248208913 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Applicative->Seq">
<pathd="M -785.682854982818,-412 L -714.799014210374,-476.959367842732"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -708.163811683849,-483.04 L -718.238762116551,-479.232720948158 C -715.699848604043,-477.942360809625 -713.898179816704,-475.97637487584 -712.833755754535,-473.334763146803 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Applicative->SeqLeft">
<pathd="M -774.344312027491,-412 L -642.789872940275,-478.957606209781"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -634.769021305842,-483.04 L -645.495475917531,-482.068829848393 C -643.394672020307,-480.145880525993 -642.185073860242,-477.769331893569 -641.866681437336,-474.93918395112 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Applicative->SeqRight">
<pathd="M -762.225406557428,-411.616331588423 L -552.255039618581,-481.91850535998"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -543.720702607113,-484.775967831244 L -554.473282607084,-485.394048201604 C -552.678367392102,-483.182851583901 -551.831711845061,-480.654159136059 -551.93331596596,-477.807970858076 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Except->Monad">
<pathd="M -620.787981188119,-238 L -711.95378637201,-307.579654923495"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -719.108129922992,-313.04 L -713.585679344792,-303.793241670113 C -712.762726383344,-306.519752175201 -711.144846360676,-308.639557671788 -708.732039276787,-310.152658159875 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="List->Functor">
<pathd="M -892.034814302334,-412 L -868.075682352572,-474.634018472681"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -864.86017701711,-483.04 L -872.168952513098,-475.129134007629 C -869.321012949211,-475.110389633491 -866.830351755932,-474.157647311872 -864.696968933259,-472.270907042774 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Monad->Applicative">
<pathd="M -747.447014155251,-339 L -782.595654197137,-379.260216894652"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -788.514652511416,-386.04 L -784.951224653483,-375.876241743267 C -783.60006650904,-378.383328255499 -781.591241885233,-380.137105533804 -778.924750782062,-381.137573578181 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Monad->Bind">
<pathd="M -725.919943874952,-339 L -693.754264838054,-379.952252619104"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -688.195056125048,-387.030048779297 L -697.517641877363,-381.63659025153 C -694.802827232157,-380.775839095105 -692.705702443952,-379.128666143103 -691.226267512747,-376.695071395525 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="Option->Monad">
<pathd="M -856.761951485149,-238 L -761.177064707358,-307.735551794831"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -753.906381848185,-313.04 L -764.342450894008,-310.377583265001 C -761.962908885902,-308.81268999619 -760.391220528815,-306.658413593472 -759.627385822747,-303.914754056846 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="ReaderM->Monad">
<pathd="M -776.319514851485,-238 L -745.783102116211,-304.853562563497"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -742.043818481848,-313.04 L -749.836994714031,-305.60586224138 C -746.99590766236,-305.407530509328 -744.570296570063,-304.299594617665 -742.560161437139,-302.28205456639 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
</g>
<gid="StateM->Monad">
<pathd="M -695.681478217822,-238 L -726.395530552052,-304.861622913356"fill="none"stroke="#A0A0A0"stroke-width="1"/>
<pathd="M -730.152410671067,-313.04 L -729.612933688448,-302.283189850833 C -727.607141972296,-304.305048080909 -725.183919131808,-305.418197745802 -722.343265166986,-305.622638845513 z"fill="#A0A0A0"stroke="#A0A0A0"stroke-width="1"stroke-linejoin="round"/>
In Lean 3 stdlib, we find many [instances](https://github.com/leanprover/lean/blob/master/library/init/category/reader.lean#L39) of the dreadful `@`+`_` idiom.
It is often used when we the expected type is a function type with implicit arguments,
@@ -83,7 +83,7 @@ def id5 : {α : Type} → α → α :=
#endex2
```
* Sugar for simple functions
## Sugar for simple functions
In Lean 3, we can create simple functions from infix operators by using parentheses. For example, `(+1)` is sugar for `fun x, x + 1`. In Lean 4, we generalize this notation using `·` As a placeholder. Here are a few examples:
@@ -230,11 +230,10 @@ restriction imposed by ordinary type theory. Metadefinitions may also use unsafe
The keyword `meta` has been currently removed from Lean 4. However, we may re-introduce it in the future,
but with a much more limited purpose: marking meta code that should not be included in the executables produced by Lean.
The keywords `axiom` and `constant` are not equivalent in Lean 4. In Lean 4, `constant` is used to define
an opaque definition. Here are two simple examples:
The keyword`constant` has been deleted in Lean 4, and `axiom` should be used instead. In Lean 4, the new command `opaque` is used to define an opaque definition. Here are two simple examples:
```lean
#namespacemeta1
constantx:Nat:=1
opaquex:Nat:=1
-- The following example will not type check since `x` is opaque
-- example : x = 1 := rfl
@@ -244,11 +243,11 @@ constant x : Nat := 1
-- When no value is provided, the elaborator tries to build one automatically for us
-- using the `Inhabited` type class
constanty:Nat
opaquey:Nat
#endmeta1
```
We can instruct Lean to use a foreign function as the implementation for any constant or definition
We can instruct Lean to use a foreign function as the implementation for any definition
using the attribute `@[extern "foreign_function"]`. It is the user's responsibility to ensure the
foreign implementation is correct.
However, a user mistake here will only impact the code generated by Lean, and
@@ -336,3 +335,34 @@ partial def f (x : Nat) : IO Unit := do
#evalf98
#endpartial1
```
## Library changes
These are changes to the library which may trip up Lean 3 users:
-`Option` and `List` are no longer monads. Instead there is `OptionM`. This was done to avoid some performance traps. For example `o₁ <|> o₂` where `o₁ o₂ : Option α` will evaluate both `o₁` and `o₂` even if `o₁` evaluates to `some x`. This can be a problem if `o₂` requires a lot of compute to evaluate. A zulip discussion on this design choice is [here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Option.20do.20notation.20regression.3F).
## Style changes
Coding style changes have also been made:
- Term constants and variables are now `lowerCamelCase` rather than `snake_case`
- Type constants are now `UpperCamelCase`, eg `Nat`, `List`. Type variables are still lower case greek letters. Functors are still lower case latin `(m : Type → Type) [Monad m]`.
- When defining typeclasses, prefer not to use "has". Eg `ToString` or `Add` instead of `HasToString` or `HasAdd`.
- Prefer `return` to `pure` in monad expressions.
- Pipes `<|` are preferred to dollars `$` for function application.
- Declaration bodies should always be indented:
```lean
inductive Hello where
| foo
| bar
structure Point where
x : Nat
y : Nat
def Point.addX : Point → Point → Nat :=
fun { x := a, .. } { x := b, .. } => a + b
```
- In structures and typeclass definitions, prefer `where` to `:=` and don't surround fields with parentheses. (Shown in `Point` above)
@@ -46,9 +46,8 @@ For example, on an AMD Ryzen 9 `make` takes 00:04:55, whereas `make -j 10`
takes 00:01:38. Your results may vary depending on the speed of your hard
drive.
To install the build, see [Dev setup using
elan](../dev/index.md#dev-setup-using-elan).
You should not usually run `make install` after a successful build.
See [Dev setup using elan](../dev/index.md#dev-setup-using-elan) on how to properly set up your editor to use the correct stage depending on the source directory.
@@ -10,7 +10,7 @@ Follow the setup in the link above; to open the Lean shell inside a Lean checkou
$ nix-shell -A nix
```
On top of the local and remote Nix cache, it helps to we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
On top of the local and remote Nix cache, we do still rely on CCache as well to make C/C++ build steps incremental, which are atomic steps from Nix's point of view.
To enable CCache, add the following line to the config file mentioned in the setup:
```bash
extra-sandbox-paths = /nix/var/cache/ccache
@@ -35,7 +35,7 @@ The `stage1.` part in each command is optional:
```bash
nix build .#test # run tests for stage 1
nix build . # build stage 1
nix build # dito
nix build # ditto
```
## Build Process Description
@@ -52,11 +52,14 @@ This is because modules are discovered not from a directory listing anymore but
As in the standard Nix setup.
After adding `src/` as an LSP workspace, it should automatically fall back to using stage 0 in there.
Note that the UX of `emacs/vscode-dev` is quite different from the Make-based setup regarding the compilation of dependencies:
Note that the UX of `{emacs,vscode}-dev` is quite different from the Make-based setup regarding the compilation of dependencies:
there is no mutable directory incrementally filled by the build that we could point the editor at for .olean files.
Instead, `emacs-dev` will gather the individual dependency outputs from the Nix store when checking a file -- and build them on the fly when necessary.
However, it will only ever load changes saved to disk, not ones opened in other buffers.
The absence of a mutable output directory also means that the Lean server will not automatically pick up `.ilean` metadata from newly compiled files.
Instead, you can run `nix run .#link-ilean` to symlink the `.ilean` tree of the stdlib state at that point in time to `src/build/lib`, where the server should automatically find them.
## Other Fun Stuff to Do with Nix
Open Emacs with Lean set up from an arbitrary commit (without even cloning Lean beforehand... if your Nix is new enough):
@@ -86,7 +89,7 @@ nix run .#HEAD-as-stage0.emacs-dev&
```
To run `nix build` on the second stage outside of the second editor, use
# Arithmetic as an embedded domain-specific language
Let's parse another classic grammar, the grammar of arithmetic expressions with
addition, multiplication, integers, and variables. In the process, we'll learn
how to:
- Convert identifiers such as `x` into strings within a macro.
- add the ability to "escape" the macro context from within the macro. This is useful to interpret identifiers with their _original_ meaning (predefined values)
instead of their new meaning within a macro (treat as a symbol).
Let's begin with the simplest thing possible. We'll define an AST, and use operators `+` and `*` to denote
building an arithmetic AST.
Here's the AST that we will be parsing:
```lean,ignore
{{#include metaprogramming-arith.lean:1:5}}
```
We declare a syntax category to describe the grammar that we will be parsing.
See that we control the precedence of `+` and `*` by writing `syntax:50` for addition and `syntax:60` for multiplication,
indicating that multiplication binds tighter than addition (higher the number, tighter the binding).
This allows us to declare _precedence_ when defining new syntax.
```lean,ignore
{{#include metaprogramming-arith.lean:7:13}}
```
Further, if we look at `syntax:60 arith:60 "+" arith:61 : arith`, the
precedence declarations at `arith:60 "+" arith:61` conveys that the left
argument must have precedence at least `60` or greater, and the right argument
must have precedence at least`61` or greater. Note that this forces left
associativity. To understand this, let's compare two hypothetical parses:
This updates the board in the `GameState` with the new tile, and then changes the current player,
providing no output (`Unit` return type).
So finally, you can combine these functions together with `do` notation, and it actually looks quite
clean! You don't need to worry about the side effects. The different monadic functions handle them.
Here's a sample of what your function might look like to play one turn of the game. At the end, it
returns a boolean determining if all the spaces have been filled.
-/
defisGameDone:StateMGameStateBool:=do
return(←findOpen).isEmpty
defnextTurn:StateMGameStateBool:=do
leti←chooseRandomMove
applyMovei
isGameDone
/-!
To give you a quick test harness that runs all moves for both players you can run this:
-/
definitBoard:Board:=Id.rundo
letmutboard:=HashMap.empty
foriin[0:3]do
forjin[0:3]do
lett:TileIndex:=(i,j)
board:=board.inserttTileEmpty
board
defprintBoard(board:Board):IOUnit:=do
letmutrow:ListString:=[]
foriinboard.toListdo
lets:=matchi.2with
|TileEmpty=>""
|TileX=>"X"
|TileO=>"O"
row:=row.append[s]
ifrow.length==3then
IO.printlnrow
row:=[]
defplayGame:StateMGameStateUnit:=do
whiletruedo
letfinished←nextTurn
iffinishedthenreturn
defmain:IOUnit:=do
letgen←IO.stdGenRef.get
let(x,gen'):=randNatgen01
letgs:={
board:=initBoard,
currentPlayer:=ifx=0thenXPlayerelseOPlayer,
generator:=gen'}
let(_,g):=playGame|>.rungs
printBoardg.board
#evalmain
-- [X, X, O]
-- [X, O, O]
-- [O, O, X]
/-!
Note that when you run the above code interactively the random number generator always starts in the
same place. But if you run `lean --run states.lean` then you will see randomness in the result.
## Implementation
It may be helpful to see how the `StateM` monad adds the input state and output state. If you look
at the reduced Type for `nextTurn`:
-/
#reduceStateMGameStateBool
-- GameState → Bool × GameState
/-!
So a function like `nextTurn` that might have just returned a `Bool` has been modified by the
`StateM` monad such that the initial `GameState` is passed in as a new input argument, and the output
value has been changed to the pair `Bool × GameState` so that it can return the pure `Bool` and the
updated `GameState`. This is why the call to `nextTurn` looks like this: `let (_, g) := nextTurn gs`.
This expression `(_, g)` conveniently breaks the pair up into 2 values, it doesn't care what the first
value is (hence the underscore `_`), but it does need the updated state `g` which you can then assign
back to the mutable `gs` variable to use next time around this loop.
It is also interesting to see how much work the `do` and `←` notation are doing for you. To
implement the `nextTurn` function without these you would have to write this, manually plumbing
the state all the way through:
-/
defnextTurnManually:StateMGameStateBool
|state=>
let(i,gs):=chooseRandomMove|>.runstate
let(_,gs'):=applyMovei|>.rungs
let(result,gs''):=isGameDone|>.rungs'
(result,gs'')
/-!
## StateM vs ReaderM
While `ReaderM` functions can use `withReader` to modify the context before calling another function,
`StateM` functions are a little more powerful, let's look at this function again:
```
def nextTurn : StateM GameState Bool := do
let i ← chooseRandomMove
applyMove i
isGameDone
```
In this function `chooseRandomMove` is modifying the state that `applyMove` is getting
and `chooseRandomMove` knows nothing about `applyMove`. So `StateM` functions can have this
kind of downstream effect outside their own scope, whereas, `withReader` cannot do that.
## State, IO and other languages
When thinking about Lean, it is often seen as a restriction that you can't have global variables or
`static` variables like you can with other languages like Python or C++. However, hopefully you see
now this isn't true. You can have a data type with exactly the same functionality as a Python class.
You would simply have many functions that can modify some global state using the `StateM` monad.
The difference is in Lean you simply put a label on these types of functions. You don't allow it to
happen for free anywhere in an uncontrolled fashion because that results in too many sleepless
nights debugging nasty code. You want to know when side effects can potentially happen, because
knowing when they can happen makes your code easier to reason about. In a Python class, many of the
methods won't actually need to modify the global state. But they could, which makes it harder to
debug them. In Lean you can simply make these pure functions, and the compiler will ensure they stay
pure and cannot modify any global state.
IO is the same way. It's not like you can't perform IO in Lean. Instead, you want to label the areas
where you can, to increase your certainty about the areas where you don't need to. When you know part of
your code cannot communicate with the outside world, you can be far more certain of its behavior.
The `StateM` monad is also a more disciplined way of managing side effects. Top level code could
call a `StateM` function multiple times with different independent initial states, even doing that
across multiple tasks in parallel and each of these cannot clobber the state belonging to other
tasks. Monadic code is more reusable than code that uses global variables.
## Summary
That wraps it up for the `StateM` monad! There is one more very useful monad that can be used to do
exception handling which will be covered in the [next section](except.lean.md).
-/
Some files were not shown because too many files have changed in this diff
Show More
Reference in New Issue
Block a user
Blocking a user prevents them from interacting with repositories, such as opening or commenting on pull requests or issues. Learn more about blocking a user.
