Failed attempt to construct missing `Repr` instances recursively.
The correct solution is to track the reason for a TC failure.
Or, add support at the TC procedure for generating "missing
instances". That is, when `TC` fails to find global instances for
`Repr Foo`, it tries to invoke the `deriving` handler. It seems a bit crazy.
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.
This feature produced counterintuitive behavior and confused users.
See discussion at #770.
As pointed out by @tydeu, it is not too much work to write `Id.run <|`
before the `do` when we want to use the `do` notation in pure code.
closes#770
# 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 +129,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"
* Try to elaborate `do` notation even if the expected type is not available. We still delay elaboration when the expected type
is not available. This change is particularly useful when writing examples such as
```lean
#eval do
IO.println "hello"
IO.println "world"
```
That is, we don't have to use the idiom `#eval show IO _ from do ...` anymore.
Note that auto monadic lifting is less effective when the expected type is not available.
Monadic polymorphic functions (e.g., `ST.Ref.get`) also require the expected type.
* On Linux, panics now print a backtrace by default, which can be disabled by setting the environment variable `LEAN_BACKTRACE` to `0`.
Other platforms are TBD.
* The `group(·)` `syntax` combinator is now introduced automatically where necessary, such as when using multiple parsers inside `(...)+`.
* Add ["Typed Macros"](https://github.com/leanprover/lean4/pull/1251): syntax trees produced and accepted by syntax antiquotations now remember their syntax kinds, preventing accidental production of ill-formed syntax trees and reducing the need for explicit `:kind` antiquotation annotations. See PR for details.
* Aliases of protected definitions are protected too. Example:
```lean
protected def Nat.double (x : Nat) := 2*x
namespace Ex
export Nat (double) -- Add alias Ex.double for Nat.double
end Ex
open Ex
#check Ex.double -- Ok
#check double -- Error, `Ex.double` is alias for `Nat.double` which is protected
```
* Use `IO.getRandomBytes` to initialize random seed for `IO.rand`. See discussion at [this PR](https://github.com/leanprover/lean4-samples/pull/2).
* Improve dot notation and aliases interaction. See discussion on [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Namespace-based.20overloading.20does.20not.20find.20exports/near/282946185) for additional details.
Example:
```lean
def Set (α : Type) := α → Prop
def Set.union (s₁ s₂ : Set α) : Set α := fun a => s₁ a ∨ s₂ a
def FinSet (n : Nat) := Fin n → Prop
namespace FinSet
export Set (union) -- FinSet.union is now an alias for `Set.union`
end FinSet
example (x y : FinSet 10) : FinSet 10 :=
x.union y -- Works
```
* `ext` and `enter` conv tactics can now go inside let-declarations. Example:
```lean
example (g : Nat → Nat) (y : Nat) (h : let x := y + 1; g (0+x) = x) : g (y + 1) = y + 1 := by
conv at h => enter [x, 1, 1]; rw [Nat.zero_add]
/-
g : Nat → Nat
y : Nat
h : let x := y + 1;
g x = x
⊢ g (y + 1) = y + 1
-/
exact h
```
* Add `zeta` conv tactic to expand let-declarations. Example:
```lean
example (h : let x := y + 1; 0 + x = y) : False := by
conv at h => zeta; rw [Nat.zero_add]
/-
y : Nat
h : y + 1 = y
⊢ False
-/
simp_arith at h
```
* Improve namespace resolution. See issue [#1224](https://github.com/leanprover/lean4/issues/1224). Example:
```lean
import Lean
open Lean Parser Elab
open Tactic -- now opens both `Lean.Parser.Tactic` and `Lean.Elab.Tactic`
```
* Rename `constant` command to `opaque`. See discussion at [Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/What.20is.20.60opaque.60.3F/near/284926171).
* Extend `induction` and `cases` syntax: multiple left-hand-sides in a single alternative. This extension is very similar to the one implemented for `match` expressions. Examples:
```lean
inductive Foo where
| mk1 (x : Nat) | mk2 (x : Nat) | mk3
def f (v : Foo) :=
match v with
| .mk1 x => x + 1
| .mk2 x => 2*x + 1
| .mk3 => 1
theorem f_gt_zero : f v > 0 := by
cases v with
| mk1 x | mk2 x => simp_arith! -- New feature used here!
| mk3 => decide
```
* [`let/if` indentation in `do` blocks in now supported.](https://github.com/leanprover/lean4/issues/1120)
* Update Lake to v3.1.1. See the [v3.1.0 release note](https://github.com/leanprover/lake/releases/tag/v3.1.0) for detailed changes.
* Add unnamed antiquotation `$_` for use in syntax quotation patterns.
* Lean now generates an error if the body of a declaration body contains a universe parameter that does not occur in the declaration type, nor is an explicit parameter.
Examples:
```lean
/-
The following declaration now produces an error because `PUnit` is universe polymorphic,
but the universe parameter does not occur in the function type `Nat → Nat`
-/
def f (n : Nat) : Nat :=
let aux (_ : PUnit) : Nat := n + 1
aux ⟨⟩
/-
The following declaration is accepted because the universe parameter was explicitly provided in the
function signature.
-/
def g.{u} (n : Nat) : Nat :=
let aux (_ : PUnit.{u}) : Nat := n + 1
aux ⟨⟩
```
* Add `subst_vars` tactic.
* [Fix `autoParam` in structure fields lost in multiple inheritance.](https://github.com/leanprover/lean4/issues/1158).
* Add `[eliminator]` attribute. It allows users to specify default recursor/eliminators for the `induction` and `cases` tactics.
It is an alternative for the `using` notation. Example:
(succ_succ : (x y : Nat) → motive x y → motive (x + 1) (y + 1))
(x y : Nat) : motive x y :=
let rec go : (x y : Nat) → motive x y
| 0, 0 => zero_zero
| x+1, 0 => succ_zero x (go x 0)
| 0, y+1 => zero_succ y (go 0 y)
| x+1, y+1 => succ_succ x y (go x y)
go x y
termination_by go x y => (x, y)
def f (x y : Nat) :=
match x, y with
| 0, 0 => 1
| x+1, 0 => f x 0
| 0, y+1 => f 0 y
| x+1, y+1 => f x y
termination_by f x y => (x, y)
example (x y : Nat) : f x y > 0 := by
induction x, y <;> simp [f, *]
```
* Add support for `casesOn` applications to structural and well-founded recursion modules.
This feature is useful when writing definitions using tactics. Example:
```lean
inductive Foo where
| a | b | c
| pair: Foo × Foo → Foo
def Foo.deq (a b : Foo) : Decidable (a = b) := by
cases a <;> cases b
any_goals apply isFalse Foo.noConfusion
any_goals apply isTrue rfl
case pair a b =>
let (a₁, a₂) := a
let (b₁, b₂) := b
exact match deq a₁ b₁, deq a₂ b₂ with
| isTrue h₁, isTrue h₂ => isTrue (by rw [h₁,h₂])
| isFalse h₁, _ => isFalse (fun h => by cases h; cases (h₁ rfl))
| _, isFalse h₂ => isFalse (fun h => by cases h; cases (h₂ rfl))
```
* `Option` is again a monad. The auxiliary type `OptionM` has been removed. See [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084).
* Improve `split` tactic. It used to fail on `match` expressions of the form `match h : e with ...` where `e` is not a free variable.
The failure used to occur during generalization.
* New encoding for `match`-expressions that use the `h :` notation for discriminants. The information is not lost during delaboration,
and it is the foundation for a better `split` tactic. at delaboration time. Example:
```lean
#print Nat.decEq
/-
protected def Nat.decEq : (n m : Nat) → Decidable (n = m) :=
fun n m =>
match h : Nat.beq n m with
| true => isTrue (_ : n = m)
| false => isFalse (_ : ¬n = m)
-/
```
* `exists` tactic is now takes a comma separated list of terms.
* Add `dsimp` and `dsimp!` tactics. They guarantee the result term is definitionally equal, and only apply
`rfl`-theorems.
* Fix binder information for `match` patterns that use definitions tagged with `[matchPattern]` (e.g., `Nat.add`).
We now have proper binder information for the variable `y` in the following example.
```lean
def f (x : Nat) : Nat :=
match x with
| 0 => 1
| y + 1 => y
```
* (Fix) the default value for structure fields may now depend on the structure parameters. Example:
```lean
structure Something (i: Nat) where
n1: Nat := 1
n2: Nat := 1 + i
def s : Something 10 := {}
example : s.n2 = 11 := rfl
```
* Apply `rfl` theorems at the `dsimp` auxiliary method used by `simp`. `dsimp` can be used anywhere in an expression
because it preserves definitional equality.
* Refine auto bound implicit feature. It does not consider anymore unbound variables that have the same
name of a declaration being defined. Example:
```lean
def f : f → Bool := -- Error at second `f`
fun _ => true
inductive Foo : List Foo → Type -- Error at second `Foo`
| x : Foo []
```
Before this refinement, the declarations above would be accepted and the
second `f` and `Foo` would be treated as auto implicit variables. That is,
`f : {f : Sort u} → f → Bool`, and
`Foo : {Foo : Type u} → List Foo → Type`.
* Fix syntax hightlighting for recursive declarations. Example
```lean
inductive List (α : Type u) where
| nil : List α -- `List` is not highlighted as a variable anymore
| cons (head : α) (tail : List α) : List α
def List.map (f : α → β) : List α → List β
| [] => []
| a::as => f a :: map f as -- `map` is not highlighted as a variable anymore
```
* Add `autoUnfold` option to `Lean.Meta.Simp.Config`, and the following macros
When the `autoUnfold` is set to true, `simp` tries to unfold the following kinds of definition
- Recursive definitions defined by structural recursion.
- Non-recursive definitions where the body is a `match`-expression. This
kind of definition is only unfolded if the `match` can be reduced.
Example:
```lean
def append (as bs : List α) : List α :=
match as with
| [] => bs
| a :: as => a :: append as bs
theorem append_nil (as : List α) : append as [] = as := by
induction as <;> simp_all!
theorem append_assoc (as bs cs : List α) : append (append as bs) cs = append as (append bs cs) := by
induction as <;> simp_all!
```
* Add `save` tactic for creating checkpoints more conveniently. Example:
```lean
example : <some-proposition> := by
tac_1
tac_2
save
tac_3
...
```
is equivalent to
```lean
example : <some-proposition> := by
checkpoint
tac_1
tac_2
tac_3
...
```
* Remove support for `{}` annotation from inductive datatype contructors. This annotation was barely used, and we can control the binder information for parameter bindings using the new inductive family indices to parameter promotion. Example: the following declaration using `{}`
```lean
inductive LE' (n : Nat) : Nat → Prop where
| refl {} : LE' n n -- Want `n` to be explicit
| succ : LE' n m → LE' n (m+1)
```
can now be written as
```lean
inductive LE' : Nat → Nat → Prop where
| refl (n : Nat) : LE' n n
| succ : LE' n m → LE' n (m+1)
```
In both cases, the inductive family has one parameter and one index.
Recall that the actual number of parameters can be retrieved using the command `#print`.
* Remove support for `{}` annotation in the `structure` command.
* Several improvements to LSP server. Examples: "jump to definition" in mutually recursive sections, fixed incorrect hover information in "match"-expression patterns, "jump to definition" for pattern variables, fixed auto-completion in function headers, etc.
* In `macro ... xs:p* ...` and similar macro bindings of combinators, `xs` now has the correct type `Array Syntax`
* Identifiers in syntax patterns now ignore macro scopes during matching.
* Improve binder names for constructor auto implicit parameters. Example, given the inductive datatype
```lean
inductive Member : α → List α → Type u
| head : Member a (a::as)
| tail : Member a bs → Member a (b::bs)
```
before:
```lean
#check @Member.head
-- @Member.head : {x : Type u_1} → {a : x} → {as : List x} → Member a (a :: as)
```
now:
```lean
#check @Member.head
-- @Member.head : {α : Type u_1} → {a : α} → {as : List α} → Member a (a :: as)
```
* Improve error message when constructor parameter universe level is too big.
* Add support for `for h : i in [start:stop] do .. ` where `h : i ∈ [start:stop]`. This feature is useful for proving
termination of functions such as:
```lean
inductive Expr where
| app (f : String) (args : Array Expr)
def Expr.size (e : Expr) : Nat := Id.run do
match e with
| app f args =>
let mut sz := 1
for h : i in [: args.size] do
-- h.upper : i < args.size
sz := sz + size (args.get ⟨i, h.upper⟩)
return sz
```
* Add tactic `case'`. It is similar to `case`, but does not admit the goal on failure.
For example, the new tactic is useful when writing tactic scripts where we need to use `case'`
at `first | ... | ...`, and we want to take the next alternative when `case'` fails.
* "Cleanup" local context before elaborating a `match` alternative right-hand-side. Examples:
```lean
example (x : Nat) : Nat :=
match g x with
| (a, b) => _ -- Local context does not contain the auxiliary `_discr := g x` anymore
example (x : Nat × Nat) (h : x.1 > 0) : f x > 0 := by
match x with
| (a, b) => _ -- Local context does not contain the `h✝ : x.fst > 0` anymore
```
* Improve `let`-pattern (and `have`-pattern) macro expansion. In the following example,
```lean
example (x : Nat × Nat) : f x > 0 := by
let (a, b) := x
done
```
The resulting goal is now `... |- f (a, b) > 0` instead of `... |- f x > 0`.
* Add cross-compiled [aarch64 Linux](https://github.com/leanprover/lean4/pull/1066) and [aarch64 macOS](https://github.com/leanprover/lean4/pull/1076) releases.
* [Add tutorial-like examples to our documentation](https://github.com/leanprover/lean4/tree/master/doc/examples), rendered using LeanInk+Alectryon.
v4.0.0-m4 (23 March 2022)
---------
* `simp` now takes user-defined simp-attributes. You can define a new `simp` attribute by creating a file (e.g., `MySimp.lean`) containing
```lean
import Lean
open Lean.Meta
initialize my_ext : SimpExtension ← registerSimpAttr `my_simp "my own simp attribute"
```
If you don't neet to acces `my_ext`, you can also use the macro
```lean
import Lean
register_simp_attr my_simp "my own simp attribute"
```
Recall that the new `simp` attribute is not active in the Lean file where it was defined.
Here is a small example using the new feature.
```lean
import MySimp
def f (x : Nat) := x + 2
def g (x : Nat) := x + 1
@[my_simp] theorem f_eq : f x = x + 2 := rfl
@[my_simp] theorem g_eq : g x = x + 1 := rfl
example : f x + g x = 2*x + 3 := by
simp_arith [my_simp]
```
* Extend `match` syntax: multiple left-hand-sides in a single alternative. Example:
```lean
def fib : Nat → Nat
| 0 | 1 => 1
| n+2 => fib n + fib (n+1)
```
This feature was discussed at [issue 371](https://github.com/leanprover/lean4/issues/371). It was implemented 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
```
* Improve `#eval` command. Now, when it fails to synthesize a `Lean.MetaEval` instance for the result type, it reduces the type and tries again. The following example now works without additional annotations
```lean
def Foo := List Nat
def test (x : Nat) : Foo :=
[x, x+1, x+2]
#eval test 4
```
* `rw` tactic can now apply auto-generated equation theorems for a given definition. Example:
```lean
example (a : Nat) (h : n = 1) : [a].length = n := by
rw [List.length]
trace_state -- .. |- [].length + 1 = n
rw [List.length]
trace_state -- .. |- 0 + 1 = n
rw [h]
```
* [Fuzzy matching for auto completion](https://github.com/leanprover/lean4/pull/1023)
* Extend dot-notation `x.field` for arrow types. If type of `x` is an arrow, we look up for `Function.field`.
For example, given `f : Nat → Nat` and `g : Nat → Nat`, `f.comp g` is now notation for `Function.comp f g`.
* The new `.<identifier>` notation is now also accepted where a function type is expected.
```lean
example (xs : List Nat) : List Nat := .map .succ xs
example (xs : List α) : Std.RBTree α ord := xs.foldl .insert ∅
```
* [Add code folding support to the language server](https://github.com/leanprover/lean4/pull/1014).
* Support notation `let <pattern> := <expr> | <else-case>` in `do` blocks.
* Remove support for "auto" `pure`. In the [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/for.2C.20unexpected.20need.20for.20type.20ascription/near/269083574), the consensus seemed to be that "auto" `pure` is more confusing than it's worth.
* Remove restriction in `congr` theorems that all function arguments on the left-hand-side must be free variables. For example, the following theorem is now a valid `congr` theorem.
```lean
@[congr]
theorem dep_congr [DecidableEq ι] {p : ι → Set α} [∀ i, Inhabited (p i)] :
∀ {i j} (h : i = j) (x : p i) (y : α) (hx : x = y), Pi.single (f := (p ·)) i x = Pi.single (f := (p ·)) j ⟨y, hx ▸ h ▸ x.2⟩ :=
* Improve elaboration postponement heuristic when expected type is a metavariable. Lean now reduces the expected type before performing the test.
* [Remove deprecated leanpkg](https://github.com/leanprover/lean4/pull/985) in favor of [Lake](https://github.com/leanprover/lake) now bundled with Lean.
* Various improvements to go-to-definition & find-all-references accuracy.
* Auto generated congruence lemmas with support for casts on proofs and `Decidable` instances (see [whishlist](https://github.com/leanprover/lean4/issues/988)).
* Notation for providing the motive for `match` expressions has changed.
before:
```lean
match x, rfl : (y : Nat) → x = y → Nat with
| 0, h => ...
| x+1, h => ...
```
now:
```lean
match (motive := (y : Nat) → x = y → Nat) x, rfl with
| 0, h => ...
| x+1, h => ...
```
With this change, the notation for giving names to equality proofs in `match`-expressions is not whitespace sensitive anymore. That is,
we can now write
```lean
match h : sort.swap a b with
| (r₁, r₂) => ... -- `h : sort.swap a b = (r₁, r₂)`
```
* `(generalizing := true)` is the default behavior for `match` expressions even if the expected type is not a proposition. In the following example, we used to have to include `(generalizing := true)` manually.
```lean
inductive Fam : Type → Type 1 where
| any : Fam α
| nat : Nat → Fam Nat
example (a : α) (x : Fam α) : α :=
match x with
| Fam.any => a
| Fam.nat n => n
```
* We now use `PSum` (instead of `Sum`) when compiling mutually recursive definitions using well-founded recursion.
* Better support for parametric well-founded relations. See [issue #1017](https://github.com/leanprover/lean4/issues/1017). This change affects the low-level `termination_by'` hint because the fixed prefix of the function parameters in not "packed" anymore when constructing the well-founded relation type. For example, in the following definition, `as` is part of the fixed prefix, and is not packed anymore. In previous versions, the `termination_by'` term would be written as `measure fun ⟨as, i, _⟩ => as.size - i`
```lean
def sum (as : Array Nat) (i : Nat) (s : Nat) : Nat :=
if h : i < as.size then
sum as (i+1) (s + as.get ⟨i, h⟩)
else
s
termination_by' measure fun ⟨i, _⟩ => as.size - i
```
* Add `while <cond> do <do-block>`, `repeat <do-block>`, and `repeat <do-block> until <cond>` macros for `do`-block. These macros are based on `partial` definitions, and consequently are useful only for writing programs we don't want to prove anything about.
* Add `arith` option to `Simp.Config`, the macro `simp_arith` expands to `simp (config := { arith := true })`. Only `Nat` and linear arithmetic is currently supported. Example:
```lean
example : 0 < 1 + x ∧ x + y + 2 ≥ y + 1 := by
simp_arith
```
* Add `fail <string>?` tactic that always fail.
* Add support for acyclicity at dependent elimination. See [issue #1022](https://github.com/leanprover/lean4/issues/1022).
* Add `trace <string>` tactic for debugging purposes.
* Add nontrivial `SizeOf` instance for types `Unit → α`, and add support for them in the auto-generated `SizeOf` instances for user-defined inductive types. For example, given the inductive datatype
```lean
inductive LazyList (α : Type u) where
| nil : LazyList α
| cons (hd : α) (tl : LazyList α) : LazyList α
| delayed (t : Thunk (LazyList α)) : LazyList α
```
we now have `sizeOf (LazyList.delayed t) = 1 + sizeOf t` instead of `sizeOf (LazyList.delayed t) = 2`.
* Add support for guessing (very) simple well-founded relations when proving termination. For example, the following function does not require a `termination_by` annotation anymore.
* Add support for `for h : x in xs do ...` notation where `h : x ∈ xs`. This is mainly useful for showing termination.
* 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). For example
```lean
inductive HasType : Index n → Vector Ty n → Ty → Type where
```
is now interpreted as
```lean
inductive HasType : {n : Nat} → Index n → Vector Ty n → Ty → Type where
```
* To make the previous feature more convenient to use, we promote a fixed prefix of inductive family indices to parameters. For example, the following declaration is now accepted by Lean
```lean
inductive Lst : Type u → Type u
| nil : Lst α
| cons : α → Lst α → Lst α
```
and `α` in `Lst α` is a parameter. The actual number of parameters can be inspected using the command `#print Lst`. This feature also makes sure we still accept the declaration
```lean
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₂)
```
* Added auto implicit "chaining". Unassigned metavariables occurring in the auto implicit types now become new auto implicit locals. Consider the following example:
```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
```
`ctx` is an auto implicit local in the two constructors, and it has type `ctx : Vector Ty ?m`. Without auto implicit "chaining", the metavariable `?m` will remain unassigned. The new feature creates yet another implicit local `n : Nat` and assigns `n` to `?m`. So, the declaration above is shorthand for
```lean
inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where
| pop : {n : Nat} → {k : Fin n} → {ctx : Vector Ty n} → {ty : Ty} → HasType k ctx ty → HasType k.succ (u :: ctx) ty
```
* Eliminate auxiliary type annotations (e.g, `autoParam` and `optParam`) from recursor minor premises and projection declarations. Consider the following example
```lean
structure A :=
x : Nat
h : x = 1 := by trivial
example (a : A) : a.x = 1 := by
have aux := a.h
-- `aux` has now type `a.x = 1` instead of `autoParam (a.x = 1) auto✝`
exact aux
example (a : A) : a.x = 1 := by
cases a with
| mk x h =>
-- `h` has now type `x = 1` instead of `autoParam (x = 1) auto✝`
assumption
```
* We now accept overloaded notation in patterns, but we require the set of pattern variables in each alternative to be the same. Example:
* New notation `.<identifier>` based on Swift. The namespace is inferred from the expected type. See [issue #944](https://github.com/leanprover/lean4/issues/944). Examples:
```lean
def f (x : Nat) : Except String Nat :=
if x > 0 then
.ok x
else
.error "x is zero"
namespace Lean.Elab
open Lsp
def identOf : Info → Option (RefIdent × Bool)
| .ofTermInfo ti => match ti.expr with
| .const n .. => some (.const n, ti.isBinder)
| .fvar id .. => some (.fvar id, ti.isBinder)
| _ => none
| .ofFieldInfo fi => some (.const fi.projName, false)
@@ -675,6 +675,20 @@ When a ``match`` has only one line, the vertical bar may be left out. In that ca
def bar₄ (p : Nat × Nat) : Nat :=
let ⟨m, n⟩ := p in 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`
* `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.
@@ -66,33 +66,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
@@ -276,8 +276,8 @@ def sum (xs : Array Nat) : IO Nat := do
-- x: 3
-- 6
-- We can write pure code using the `do` DSL too.
defsum'(xs:ArrayNat):Nat:=do
-- We can write pure code using the `Id.run <| do` DSL too.
defsum'(xs:ArrayNat):Nat:=Id.run<|do
letmuts:=0
forxinxsdo
s:=s+x
@@ -348,6 +348,46 @@ TODO: describe `forIn`
TODO
## Returning early from a failed match
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=>l.go((k,v)::r.goacc)
/-!
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,7 +219,7 @@ 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)
@@ -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.
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:
1. Open VS Code and install the `lean4` extension.
1. Launch VS Code and install the `lean4` extension.

1. Create a new file with the extension `.lean` and add the following code:
```lean
import Leanpkg
1. Create a new file using "File > New Text File" (`Ctrl+N`). Click the `Select a language` prompt, type in `lean4`, and hit ENTER. You should see the following popup:

Click the "Install Lean using Elan" button. You should see some progress output like this:
#eval Leanpkg.leanVersionString
```
You should get a syntax-highlighted file with a "Lean Infoview" on the right that tells you the installed Lean version when placing your cursor on the last line.
info: syncing channel updates for 'nightly'
info: latest update on nightly, lean version nightly-2021-12-05
info: downloading component 'lean'
```
1. While it is installing, you can paste the following Lean program into the new file:
```lean
#eval Lean.versionString
```
When the installation has finished, the Lean Language Server should start automatically and you should get syntax-highlighting and a "Lean Infoview" popping up on the right. You will see the output of the `#eval` statement when
you place your cursor at the end of the statement.

1. You are set up! Try opening a Lean folder containing a package file `leanpkg.toml`. You can create your own packages using `leanpkg init` on the command line.
Packages **have** to be opened using "File > Open Folder..." for imports to work.
Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`).
You are set up!
## Create a Lean Project
You can now create a Lean project in a new folder. Run `lake init foo` from "View > Terminal" to create a package, followed by `lake build` to get an executable version of your Lean program.
On Linux/macOS, you first have to follow the instructions printed by the Lean installation or log out and in again for the Lean executables to be available in you terminal.
Note: Packages **have** to be opened using "File > Open Folder..." for imports to work.
Saved changes are visible in other files after running "Lean 4: Refresh File Dependencies" (`Ctrl+Shift+X`).
## Troubleshooting
**The InfoView says "Waiting for Lean server to start..." forever.**
Check that the VS Code Terminal is not showing some installation errors from `elan`.
If that doesn't work, try also running the VS Code command `Developer: Reload Window`.
Platforms built & tested by our CI, available as nightly & stable releases via elan (see above)
* x86-64 Linux with glibc 2.27+
* x86-64 macOS 10.15+
* x86-64 Windows 10+
### Tier 2
Platforms cross-compiled but not tested by our CI, available as nightly & stable releases
Releases may be silently broken due to the lack of automated testing.
Issue reports and fixes are welcome.
* aarch64 Linux with glibc 2.27+
* aarch64 (M1) macOS
<!--
### Tier 3
Platforms that are known to work from manual testing, but do not come with CI or official releases
-->
# Setting Up Lean
There are currently two ways to set up a Lean 4 development environment:
@@ -21,25 +47,29 @@ $ elan default leanprover/lean4:nightly
$ elan override set leanprover/lean4:stable
```
### `leanpkg`
### `lake`
Lean 4 comes with a basic package manager, `leanpkg`.
Use `leanpkg init Foo` to initialize a Lean package `Foo` in the current directory, and `leanpkg build` to typecheck and build it as well as all its dependencies; call `leanpkg help` to learn about further commands.
The general directory structure of a package `Foo` is
Lean 4 comes with a package manager named `lake`.
Use `lake init foo` to initialize a Lean package `foo` in the current directory, and `lake build` to typecheck and build it as well as all its dependencies. Use `lake help` to learn about further commands.
The general directory structure of a package `foo` is
```sh
leanpkg.toml# package configuration
Foo.lean # main file, import via `import Foo`
lakefile.lean# package configuration
lean-toolchain # specifies the lean version to use
Foo.lean # main file, import via `import Foo`
Foo/
A.lean # further files, import via e.g. `import Foo.A`
A/... # further nesting
build/ # `leanpkg` output directory
A.lean # further files, import via e.g. `import Foo.A`
A/...# further nesting
build/ # `lake` build output directory
```
After running `lake build` you will see a binary named `./build/bin/foo` and when you run it you should see the output:
```
Hello, world!
```
Note however that producing native binaries and libraries (`leanpkg build bin/lb`) currently depends on `make` and an external C compiler for recursive compilation.
It has been tested on Windows by installing these tools using [MSYS2](https://www.msys2.org/), but [MinGW](http://www.mingw.org/) or WSL should work, too.
### Editing
Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4/tree/master/lean4-mode/README.md), [VS Code](https://github.com/leanprover-community/vscode-lean4), and possibly other editors.
Lean implements the [Language Server Protocol](https://microsoft.github.io/language-server-protocol/) that can be used for interactive development in [Emacs](https://github.com/leanprover/lean4-mode), [VS Code](https://github.com/leanprover-community/vscode-lean4), and possibly other editors.
Changes must be saved to be visible in other files, which must then be invalidated using an editor command (see links above).
@@ -77,7 +107,7 @@ From a Lean shell, run
$ nix flake new mypkg -t github:leanprover/lean4
```
to create a new Lean package in directory `mypkg` using the latest commit of Lean 4.
Such packages follow the same directory layout as described in the basic setup above, except for a `leanpkg.toml`/`lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
Such packages follow the same directory layout as described in the basic setup above, except for a `lakefile.lean` replaced by a `flake.nix` file set up so you can run Nix commands on it, for example:
## 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
-- example on parsing arith language via macros
inductive Arith : Type where
| add : Arith → Arith → Arith -- e + f
| mul : Arith → Arith → Arith -- e * f
| int : Int → Arith -- constant
| symbol : String → Arith -- variable
```
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.
@@ -76,7 +76,7 @@ you can declare an (anonymous) instance stating that if `a` has addition, then `
has addition:
```lean
instance[Adda]:Add(Arraya)where
addxy:=Array.zipWithxy(.+.)
addxy:=Array.zipWithxy(·+·)
#evalAdd.add#[1,2]#[3,4]
-- #[4, 6]
@@ -157,31 +157,6 @@ export Inhabited (default)
-- true
# end Ex
```
Sometimes we want to think of the default element of a type as being an *arbitrary* element, whose specific value should not play a role in our proofs.
For that purpose, we can write ``arbitrary`` instead of ``default``. We define ``arbitrary`` as an *opaque* constant.
Opaque constants are never unfolded by the type checker.
The theorem `defNatEq0` type checks because the type checker can unfold `(default : Nat)` and reduce it to `0`. This is not the case in the theorem `arbitraryNatEq0` because `arbitrary` is an opaque constant.
## Chaining Instances
@@ -194,7 +169,7 @@ This causes class inference to chain through instances recursively, backtracking
For example, the following definition shows that if two types ``a`` and ``b`` are inhabited, then so is their product:
```lean
instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
default := (arbitrary, arbitrary)
default := (default, default)
```
With this added to the earlier instance declarations, type class instance can infer, for example, a default element of ``Nat × Bool``:
```lean
@@ -205,19 +180,19 @@ With this added to the earlier instance declarations, type class instance can in
# default := true
# instance : Inhabited Nat where
# default := 0
# constant arbitrary [Inhabited a] : a :=
# opaque default [Inhabited a] : a :=
# Inhabited.default
instance [Inhabited a] [Inhabited b] : Inhabited (a × b) where
default := (arbitrary, arbitrary)
default := (default, default)
#eval (arbitrary : Nat × Bool)
#eval (default : Nat × Bool)
-- (0, true)
# end Ex
```
Similarly, we can inhabit type function with suitable constant functions:
```lean
instance [Inhabited b] : Inhabited (a -> b) where
default := fun _ => arbitrary
default := fun _ => default
```
As an exercise, try defining default instances for other types, such as `List` and `Sum` types.
@@ -229,7 +204,7 @@ and is useful for triggering the type class resolution procedure when the expect
def foo : Inhabited (Nat × Nat) :=
inferInstance
theorem ex : foo.default = (arbitrary, arbitrary) :=
theorem ex : foo.default = (default, default) :=
rfl
```
You can use the command `#print` to inspect how simple `inferInstance` is.
"Cycle between some possible indentation points (in reverse order).
See `lean4-eri-indent' for a description of how the indentation points
are calculated."
(interactive)
(lean4-eri-indentt))
(provide'lean4-eri)
;;; lean4-eri.el ends here
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.