diff options
Diffstat (limited to 'plt')
| -rw-r--r-- | plt/lean.md | 169 |
1 files changed, 169 insertions, 0 deletions
diff --git a/plt/lean.md b/plt/lean.md new file mode 100644 index 0000000..41bf622 --- /dev/null +++ b/plt/lean.md @@ -0,0 +1,169 @@ +--- +layout: plt +title: An Unofficial Lean Reference +--- + +# a lean 4 reference + +Lean is a combination programming language and theorem prover. It's a pretty neat language! + +## table of contents + +- Documentation +- Core Lean +- Evaluation +- Assignment +- Data Types + - `structure` + - `inductive` + - `class` + - `List` and `Array` + - `Nat`, `Fin`, and `USize` +- Iteration +- Classes +- Coersion +- Modules +- Monads +- Macros + +## Documentation + +First: where is the documentation? + +The primary source of documentation is the [Lean API docs](https://leanprover-community.github.io/mathlib4_docs/). Despite the URL, they cover more than just mathlib - also generating docs from the (heavily commented) standard library and compiler code base. Lean does not have a comprehensive reference manual, but these docs are as close as it gets. + +The secondary source of documentation is the [Lean Zulip](https://leanprover.zulipchat.com/). Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, indexable<sup>`[1]`</sup> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and extremely knowledgeable people: with both channels for compiler development and new-to-Lean questions alike. + +There is additionally the [official documentation page](https://lean-lang.org/documentation/) and the [unofficial documentation page](https://leanprover-community.github.io/learn.html), which together catalogue most all of the other learning resources available for Lean. + +There are several books written for Lean. Depending on what you want to do, [*Theorem Proving in Lean*](https://leanprover.github.io/theorem_proving_in_lean4/introduction.html) or [*Functional Programming in Lean*](https://leanprover.github.io/functional_programming_in_lean/introduction.html) are alternately recommended. There are also a good deal more, which I have not read: +- [*Mathematics in Lean*](https://leanprover-community.github.io/mathematics_in_lean/) +- [*The Mechanics of Proof*](https://hrmacbeth.github.io/math2001/) +- [*The Hitchhiker's Guide to Logical Verification*](https://browncs1951x.github.io/static/files/hitchhikersguide.pdf) +- [*Metaprogramming in Lean*](https://leanprover-community.github.io/lean4-metaprogramming-book/) + +Finally, there is [the Lean manual](https://lean-lang.org/lean4/doc/). It is *very* much a work in progress, and contains plenty of blank pages: but, I've found some sections helpful on occasion. + +`[1]`: Though, it doesn't seem to be indexed by Google. + +## Prelude + +Second: what is *in* the language, really? Is there a syntactic reference? + +The short answer is no, there is not a syntax reference, and if there existed one it wouldn't be very helpful. Lean has an extremely powerful metaprogramming system: and the majority of *syntax* in Lean is user-defined. + +The best way to find out what you're looking at is to use VS Code's right-click "Go to Declaration" feature. On a type, it'll drop you at its declaration. On a term, it'll drop you on its definition. On a *syntactic element*, it will either drop you into the core Lean codebase, or, more likely, onto a *macro syntax rule*. (If you are not writing Lean in VS Code, by the way, you should be. Lean has *extremely* good tooling that is primarily based around VS Code. Emacs is the only other option but is much less maintained.) + +However. To my best understanding, the syntactic forms are as follows: +- types: `:` + - [`structure`] [`inductive`] `coinductive` [`class`] `instance` + - `where` `instance` `extends` `deriving` +- values: + - `""` `''` `«»` `[]` `#[]` `{}` `()` `fun` `λ` + - `--` `/- -/` `/-- -/` `/-! -/` + - `×` `⊕` + - numbers `0b` `0x` ... +- assignment: `:=` + - `def` `abbrev` + - `let` `let rec` `let mut` + - `macro` `macro_rules` `notation` `syntax` +- control flow: `if`/`then`/`else` `match`/`with` +- iteration: + - `for`/`in`/`do` `while`/`do` `repeat` + - `return` `continue` `break` +- exceptions: `try` `catch` `finally` +- monads: `<-` [`do`] (also `failure` `pure`) +- modules: + - `namespace`/`end` `section`/`end` + - `open`/`in` `import` + - `hiding` `renaming` `exposing` + - `export` `private` `protected` ... +- modifiers: `@[...]` `partial` `noncomputable` `nonrec` +- debugging: `assert!` `dbg_trace` +- proof: + - `axiom` `theorem` `lemma` + - `show` `from` `have` `by` `at` `this` + - `suffices` `calc` `admit` +- holes: `sorry` `stop` +- evaluation: `#eval` `#check` `#check_failure` `#reduce` `#print` + +[`structure`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html +[`inductive`]: https://leanprover.github.io/functional_programming_in_lean/getting-to-know/datatypes-and-patterns.html +[`class`]: https://leanprover.github.io/functional_programming_in_lean/type-classes/polymorphism.html + +[`do`]: https://lean-lang.org/lean4/doc/do.html + +This list is unlikely to be comprehensive. + +The standard data types included in core Lean are the following: +- unit: [`Unit`] +- booleans: [`Bool`] +- numbers: + - [`Nat`], [`Int`], [`Fin n`] + - [`USize`], [`UInt8`], [`UInt16`], [`UInt32`], [`UInt64`], [`BitVec`] +- strings: [`Char`], [`String`], [`Substring`] +- lists: [`List α`], [`Array α`], [`Subarray`] (see also: [`Batteries.Vector α n`]) + - [`ByteArray`], [`FloatArray`] (these may be optimized out in the future) +- errors: [`Option α`], [`Except ε α`] +- data: [`Prod α β`], [`Sum α β`] (see also: `structure`, `inductive`) +- types: [`Empty`], [`Nonempty`], [`Type`/`Prop`/`Type u`/`Sort u`] +- proof: + - [`And α β`], [`Or α β`], [`Iff α β`], [`True`], [`False`] + - [`Eq α β`], [`Equivalence`] + - [`Exists`] (where is `Forall`?) + +[`Unit`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Unit +[`Bool`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Bool +[`Nat`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nat +[`Int`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/Int/Basic.html +[`Fin n`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Fin +[`USize`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#USize +[`UInt8`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt8 +[`UInt16`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt16 +[`UInt32`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt32 +[`UInt64`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#UInt64 +[`BitVec`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/BitVec/Basic.html +[`Char`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Char +[`String`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#String +[`Substring`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Substring +[`List α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#List +[`Array α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Array +[`Subarray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Subarray +[`Batteries.Vector α n`]: https://leanprover-community.github.io/mathlib4_docs/Batteries/Data/Vector/Basic.html +[`ByteArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/ByteArray/Basic.html +[`FloatArray`]: https://leanprover-community.github.io/mathlib4_docs/Init/Data/FloatArray/Basic.html +[`Option α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Option +[`Except ε α`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Except +[`Prod α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Prod +[`Sum α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Sum +[`Empty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Empty +[`Nonempty`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Nonempty +[`Type`/`Prop`/`Type u`/`Sort u`]: https://leanprover-community.github.io/mathlib4_docs/foundational_types.html +[`And α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#And +[`Or α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Or +[`Iff α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Iff +[`True`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#True +[`False`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#False +[`Eq α β`]: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Eq +[`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence +[`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists + +## Iteration + +Lean has three main syntactic constructs for iteration: `for`, `while`, and `repeat`. They all function pretty much as you would expect and ultimately desugar to lambdas and (tail) recursion. + +However: Lean is a purely functional language, as much as it does a good job at hiding it. In the default (pure) context, variable mutation is not allowed. Neither is IO, nor any sort of side effects. And `for`/`while`/`repeat` <span title="Okay, okay, they return PUnit. You know what I meant :-P">do not return to a value<sup>*</sup>.</span> + +Iteration is thus *useless* in the pure context! We can iterate, for sure, but there may never be any *observable* changes. As such, Lean does not allow `for`/`while`/`repeat` within pure functions. This can be the cause of some strange type errors. Ensure you are only iterating in a monadic `do` context. + +It should be noted that the `do` in `for <item> in <iter> do` and `while <cond> do` are part of the `for`/`while` declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though. + +### implementing iterators: `ForIn` and `Stream` + +`for` desugars to an appliction of the `ForIn.forIn` method, so that data structures can implement individually what exactly iteration means for them. + +The iteration implemented by `ForIn` is called "internal iteration", which means it is a higher order function where you give the body of the loop to it to run on the elements yielded by the iterator in order. This is in contrast to "external iteration" (in the style of Rust), where the iterator has a function returning the next value of the iterator. + +Lean also has an external iteration typeclass, called `Stream`, but it is not used as much. `Stream` provides a `.next?` method that returns an `Option (value × stream)` + +One reason to prefer internal iteration is that it is easier to verify termination. This is something Lean cares very much about. But, internal iteration is a less flexible model than external iteration. You can't quite just convert an internal iterator to an external iterator. So there are some downsides. |