meow

1 files changed, 99 insertions, 43 deletions

diff --git a/plt/lean.md b/plt/lean.md
index a7d0b86..a38e64d 100644
--- a/plt/lean.md
+++ b/plt/lean.md
@@ -13,12 +13,13 @@ I found it hard to get started with, however. This guide is an attempt at remedy
 
 - [Documentation](#documentation)
 - [Prelude](#prelude)
-- Evaluation
-- Assignment
+- Basics
+- [Assignment](#assignment)
+- Functions
 - Data Types
-  - [Structural Types](#structural-types)
+  - [Structures](#structures)
   - [Products](#products)
-  - Inductive Types
+  - Inductives
   - [Sums](#sums)
   - [Booleans](#booleans)
   - [Numbers](#numbers)
@@ -40,11 +41,12 @@ I found it hard to get started with, however. This guide is an attempt at remedy
 
 First: where is the documentation?
 
-The primary source of documentation is the [Lean source code documentation][Main Docs]. Despite the URL, it covers 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 primary source of documentation is the [Lean source code documentation][Main Docs]. Despite the URL, it covers 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, and so these docs are as close as it gets.
 
-The secondary source of documentation is the [Lean Zulip]. Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderfully nice and very knowledgeable people: with both channels for compiler development and new-to-Lean questions alike.
+The secondary source of documentation is the [Lean Zulip]. Zulip is a tool that is for chat software what Stack Exchange was for forums: it turns them into a searchable, <span title="Though, it doesn't seem to be indexed by Google.">indexable</span> *knowledge database*. The Lean Zulip in particular is host to a wide variety of wonderful and very knowledgeable people: with channels for both 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 also several books written for Lean. Depending on what you want to do, *[Functional Programming in Lean]* or *[Theorem Proving in Lean]* are alternately recommended. There are a good deal more, which I have not read:
 - *[Mathematics in Lean]*
 - *[The Mechanics of Proof]*
@@ -70,6 +72,10 @@ 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.
 
 However. To my best understanding, the syntactic forms are as follows:
+
+<details>
+<summary>expand</summary>
+
 - types: `:`
   - [`structure`] [`inductive`] <span title="Coinductive types do not actually exist yet.">`coinductive`</span> [`class`] `instance`
   - `where` `instance` `extends` `deriving`
@@ -110,9 +116,15 @@ However. To my best understanding, the syntactic forms are as follows:
 
 [`do`]: https://lean-lang.org/lean4/doc/do.html
 
+</details>
+
 This list is unlikely to be comprehensive.
 
 The standard data types included in core Lean are the following:
+
+<details>
+<summary>expand</summary>
+
 - unit: [`Unit`]
 - booleans: [`Bool`]
 - numbers: [`Nat`] [`Int`] [`Fin n`]
@@ -123,7 +135,7 @@ The standard data types included in core Lean are the following:
   - (see also: [`Batteries.Vector α n`])
 - errors: [`Option α`] [`Except ε α`]
 - data: [`Prod α β`] [`Sum α β`]
-  - (see also: `structure` `inductive`)
+  - (see also: [`structure`] [`inductive`])
 - types: [`Empty`] [`Nonempty`] [`Type`/`Prop`/`Type u`/`Sort u`]
 - proof:
   - [`And α β`] [`Or α β`] [`Iff α β`] [`True`] [`False`]
@@ -166,17 +178,56 @@ The standard data types included in core Lean are the following:
 [`Equivalence`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Equivalence
 [`Exists`]: https://leanprover-community.github.io/mathlib4_docs/Init/Core.html#Exists
 
-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*.
+</details>
+
+
+## Basics
 
-(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.)
+Lean is a functional programming language. todo
+
+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*.
 
-## Evaluation
+(If you are not writing Lean in VS Code, 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.)
 
 ## Assignment
 
+There are several ways to declare variables and functions:
+- `def` introduces a *named* definition.
+- `let` defines a *local* binding.
+  - `let rec` declares a *local recursive* binding.
+  - `let mut` defines a *mutable* binding.
+- `abbrev` defines a transparent alias.
+
+All of these may take parameters.
+
+```haskell
+def hello := "Hello"
+def world : String :=
+  let world := "world"
+  let world := world.push '!'
+  world
+
+def inc (n : Nat) : Nat := n + 1
+def dec n := n - 1
+
+abbrev Byte := UInt8
+```
+
+The walrus operator `:=` is used for assignment, as `=` is used for *querying* equality. It follows the name of a `def`, `let`, or `abbrev` declaration. A type annotation can optionally precede `:=`. In most cases, they are not necessary - Lean has good type inference. The `←` operator is occasionally also used for assignment, in a similar fashion to `:=`. Its semantics are complex and covered in the section on monads.
+
+The primary distinction between `def` and `let` is that `let` allows *shadowing*: a future invocation of `let` may overwrite previous `let` bindings. `let` is thus useful for variables, while `def` is more useful for constants and functions that may be exported. `def` is additionally self-referential by default, though there are some asterisks, while `let` requires the use of `let rec`. The `let mut` declaration, it should be noted, is syntactic sugar over the State monad, which we will discuss later.
+
+The `abbrev` declaration creates a direct alias between the left and right hand sides of the declaration. Lean will gratuitously unfold these during overload resolution or when reducing or querying equality.
+
+All definitions may only be used after their declaration. A function thus cannot refer to a function declared after it, nor a structure to a not-yet declared structure. This prevents the declaration of mutually-entangled structures (and functions) and simplifies analysis.
+
+See also: [FPIL:Functions and Definitions](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/functions-and-definitions.html)
+
+## Functions
+
 ## Data Types
 
-### Structural Types
+### Structures
 
 The `structure` type is analogous to structs in other languages. It behaves much as one would expect.
 
@@ -191,17 +242,19 @@ let header : Header := {
   height := 1080
   alpha := true
 }
+```
+
+Structures may be declared with the `structure ... where` syntax. Just like functions, multiple fields of the same type may be grouped together, and default values are supported. An individual field with a default value may be omitted in the constructor. A field of a function may or may not be wrapped in parentheses, but parentheses are required for multiple fields of the same type.
+
+Structures may be constructed with braces. The braces are syntactic sugar for an underlying `Name.mk` constructor. Their fields take the form `field := value`, separated either by newlines or by commas. If `value` is a variable of the same name as `field`, the `field :=` portion may be omitted. The brace constructors are *structural*: the order in which fields are declared does not matter, only their name does.
 
+```haskell
 def increment_height (header : Header) : Header :=
   let {width, height, alpha, linear} := header
   let height := height + 1
   {width, height, alpha, linear}
 ```
 
-Structures may be declared with the `structure ... where` syntax. Just like functions, multiple fields of the same type may be grouped together, and default values are supported. An individual field with a default value may be omitted in the constructor. A field of a function may or may not be wrapped in parentheses, but parentheses are required for multiple fields of the same type.
-
-Structures may be constructed with braces. The braces are syntactic sugar for an underlying `Name.mk` constructor. Their fields take the form `field := value`, separated either by newlines or by commas. If `value` is a variable of the same name as `field`, the `field :=` portion may be omitted. The brace constructors are *structural*: the order in which fields are declared does not matter, only their name does.
-
 Structures may be destructured either by pattern matching or with dot notation for field access. Pattern matching may be done via `match` or inline via `let` with the `{}` syntax.
 
 They cannot be mutated: Lean is functional and so there is no explicit syntax for updating a field. `header.width ← ...` does nothing, even if `header` is declared to be mutable. Instead, the entire `header` structure must be updated at once. This can be a pain on large structures, so Lean provides the `with` keyword for succiently (re-)constructing a structure with only a few fields changed. The `increment_height` function above can thus be compactly declared as the following:
@@ -219,16 +272,17 @@ structure Color where
   (r g b a : UInt8)
 
 structure Pixel extends Point, Color
-  -- implicit fields:
-  -- (x y : Int)
-  -- (r g b a : UInt8)
+
+let pixel : Pixel := {
+  x := 2000, y := 1000
+  r := 255, g := 255, b := 255, a := 255
+}
 ```
 
 Structures may also parametrize over terms or other types. todo
 
 Be warned - the `where` in a `structure` declaration is mandatory. Leaving off the `where` will result in a (valid!) structure with *zero* fields, that is instead *parametrized* over what were intended to be the fields. This can lead to strange type errors.
 
-
 See also: [FPIL:Structures](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/structures.html), [FPIL:Structures and Inheritance](https://leanprover.github.io/functional_programming_in_lean/functor-applicative-monad/inheritance.html), [Manual:Structures](https://lean-lang.org/lean4/doc/struct.html)
 
 ### Products
@@ -249,13 +303,13 @@ let image : Image := (header, #[])
 
 Lean also provides the compact `α × β` notation as syntactic sugar for `Prod α β`. With Lean's rules around function application, tuples of arbitrary arity can be written `α × β × γ × ...`, which is equivalent to `α × (β × (γ × ...))` (and `Prod α Prod β Prod γ ...`).
 
-While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also provides tuple-like notation for constructing them: `(a, b, ...)`. This is overloaded to function for products of arbitrary arity. Similar to tuples elsewhere, the `.fst` and `.snd` destructors have aliases to `.1` and `.2`, respectively - however, there do not exist aliases for the rest of the natural numbers.
+While products can be constructed with `Prod.mk a b` or `{ fst := a, snd := b }`, there is also tuple-like notation for constructing them: `(a, b, ...)`. This is overloaded to function for products of arbitrary arity. Similar to tuples elsewhere, the `.fst` and `.snd` destructors have aliases to `.1` and `.2`, respectively - however, there do not exist aliases for the rest of the natural numbers.
 
 The name `Prod` comes from type theory (and category theory more broadly). Structures are a special case of what is more generally called a "product": a vast generalization of the idea of taking a "pair" of something. The design of the `Prod` type aligns significantly closer to the specific formal notion of a "product type" in type theory than `structure` does, making it additionally quite useful for mathematicians.
 
 See also: [FPIL:Polymorphism#Prod](https://leanprover.github.io/functional_programming_in_lean/getting-to-know/polymorphism.html#prod)
 
-### Inductive Types
+### Inductives
 
 ### Sums
 
@@ -290,9 +344,9 @@ if let {r, g, b} := a then
 
 ### Numbers
 
-Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], and [`Fin n`].
+Lean provides a variety of representations of numbers. The main three are [`Nat`], [`Int`], & [`Fin`][`Fin n`].
 
-`Nat` is an arbitrary-sized number type. It is defined as the following:
+[`Nat`] is an arbitrary-sized number type. It is defined as the following:
 ```haskell
 -- Zero is a natural number.
 -- The successor of a natural number is a natural number.
@@ -301,7 +355,7 @@ inductive Nat where
   | succ (n : Nat)
 ```
 
-Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equivalent to their `Nat.succ (Nat.succ ...)` counterparts. Special compiler support allows for representing `Nats` in a reasonable / efficient fashion: numbers smaller than `2^63` are stored directly, while numbers larger than `2^63 - 1` use an arbitrary precision BigInt library.
+Lean recognizes numeric literals (`0`, `1`, `2`...) as numeric constructors, equivalent to their `Nat.succ (Nat.succ ...)` counterparts. Special compiler support allows for representing `Nats` in a reasonable / efficient fashion: numbers smaller than `2^63` are stored directly, while numbers larger than `2^63 - 1` use an [arbitrary precision BigInt library](https://gmplib.org/manual/).
 
 It should be noted that Lean treats operations on `Nat` that would produce a negative number **as producing zero**. For example, `#check 4 - 5` prints `4 - 5 : Nat`, and `#eval 4 - 5` prints `0`.
 
@@ -315,7 +369,7 @@ inductive Int where
   | negSucc (n : Nat) -- (-∞ : -1]
 ```
 
-[`Fin n`] is a natural number guaranteed to be *smaller* than `n`: i.e. `i ∈ ℕ : 0 ≤ i < n`. The underlying representation is `val : Nat` and a proof that the `val < n`.
+[`Fin n`] is a natural number guaranteed to be *smaller* than `n`. The underlying representation is `val : Nat` and a proof that `val < n`.
 ```haskell
 -- If i : Fin n, then i.val : Nat is the described number.
 -- It can also be written as i.1 or just i when the target type is known.
@@ -344,13 +398,15 @@ The expected basic mathematical operations are defined on all numbers. Their sem
 - bitwise: `&&&`, `|||`, `^^^`, `~~~`
 - shifts: `<<<`, `>>>`
 
-Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods.
+Numbers regularly need to be explicitly converted between different representations. This may be done via various `.toType` and `.ofType` methods. More on conversion can be found in the Classes section.
+
+See also: [Manual:Naturals](https://lean-lang.org/lean4/doc/nat.html)
 
 ### Lists
 
 Lean provides for several representations of list-like data structures.
 
-[`List α`] is the standard representation. It is represented as a linked list, and defined as the following:
+[`List α`] is the standard representation. It is represented as a linked list, and defined as follows:
 ```haskell
 inductive List (α : Type u) where
   | nil
@@ -359,18 +415,18 @@ inductive List (α : Type u) where
 
 `List.nil` or more commonly `[]` represents the empty list. `List.cons a l` or `a :: l` (for some `a : α`, `l : List α`) are used for list concatenation. `[a, b, c, ...]` syntax can also be used for construction of lists. Various functions and classes are defined for and on lists.
 
-[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. Arrays are significantly more performant than Lists: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", all updates will be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. As such, you usually want to use `Array`.
+[`Array α`] is isomorphic to `List α`. It is represented as a dynamic array. Arrays are significantly more performant than Lists: not only are they more efficient at everything except insertation and deletion, but so long as arrays are used "linearly", Lean will optimize all updates to be *destructive* - which provides comparable performance to mutable arrays in imperative programming languages. As such, **you usually want to use `Array`**.
 
-However: currently `Arrays` are represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.
+However: currently `Arrays` are always represented as an array of *pointers* in memory, for ABI reasons. This is an obvious performance pitfall for small types and liable to change in the (near) future. But for now, Lean provides special [`ByteArray`] / [`FloatArray`] types that are treated like `Array UInt8` and `Array Float` respectively, but represented as real unboxed byte/float arrays.
 
-`Array` has a different syntax for its constructor: `#[a, b, c]`. It does overload `a :: l`.
+`Array` has different syntax for its constructor: `#[a, b, c]`. It also does not implement `List.cons a l` or `a :: l`. Instead, it uses `Array.push l a`, with elements added to the *end* of the array.
 
-The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence.
+The [`Batteries.Vector α n`] type is not in `Std`, but worth a mention. It is a *statically sized array*: represented under the hood by `Array`, but guaranteed to not change size throughout its existence. It behaves much the same as `Array`, though without `push`.
 
-All lists provide some postfix `foo[i]` syntax for accessing arbitrary array elements.
-- `foo[i]` takes an `i : Fin n`, where `n < foo.size`. If this cannot be proven it fails to compile.
-- `foo[i]?` returns an `Option α`.
-- `foo[i]!` returns an `α` or panics.
+All lists provide some postfix `list[i]` syntax for accessing arbitrary array elements.
+- `list[i]` takes an `i : Fin n`, for `n < list.size`. If this cannot be proven it fails to compile.
+- `list[i]?` returns an `Option α`.
+- `list[i]!` returns an `α` or panics.
 
 See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_programming_in_lean/getting-to-know/polymorphism.html#linked-lists), [Manual:Arrays](https://lean-lang.org/lean4/doc/array.html)
 
@@ -378,7 +434,7 @@ See also: [FPIL:Polymorphism#Linked Lists](https://lean-lang.org/functional_prog
 
 The [`String`] type represents a UTF-8 encoded string. It is treated as a `List Char`, but represented as a packed `ByteArray`. Strings are constructed via `""`.
 
-The [`Char`] type represents a "Unicode scalar value": that is, a codepoint. The underlying value is represented (presumably) in UTF-32 as a `UInt32`. Chars are constructed via `''`.
+The [`Char`] type represents a "Unicode scalar value": that is, a codepoint. The underlying value is represented (presumably) in UTF-32 as a `UInt32`. Chars are constructed via `''`. They are ordered, and can be compared using `=`, `<`, `≤`, `>`, and `≥`.
 
 String manipulation can be inefficient. The [`Substring`] type provides an immutable *view* into some subslice of a `String`.
 
@@ -417,11 +473,11 @@ inductive Except (ε : Type) (α : Type) where
 
 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` return only the Unit value, providing no information.
+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 other side effects. And `for`/`while`/`repeat` may only return the Unit value.
 
 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/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.
+(It should be noted that the `do` in `for/in/do` and `while/do` are part of their declaration syntax, and are unrelated to the `do` keyword. Morally, they're the same `do`, though.)
 
 #### implementing iterators: `ForIn` and `Stream`
 
@@ -441,10 +497,10 @@ It is probably possible to do external iteration via the State monad. I would li
 
 The standard reference is [Metaprogramming in Lean](https://leanprover-community.github.io/lean4-metaprogramming-book/).
 
-I will make no attempt to describe Lean's system in detail. I do plan to provide a high-level overview.
-
 ## Proof
 
-A text for type theorists is [Theorem Proving in Lean].
-A text for mathematicians is [Mathematics in Lean].
-A text for those new to mathematics is [The Mechanics of Proof].
+The standard reference for type theorists is [Theorem Proving in Lean].
+
+The standard reference for mathematicians is [Mathematics in Lean].
+
+A guide for those new to mathematics entirely is [The Mechanics of Proof].