|
2 | 2 |
|
3 | 3 | <br> |
4 | 4 |
|
5 | | ---- |
6 | | - |
7 | | -### types and functions |
| 5 | +### tl; dr |
8 | 6 |
|
9 | 7 | <br> |
10 | 8 |
|
11 | 9 | * there are two primary concepts in lean: functions and types |
12 | 10 | * basic types examples are natural numbers (`Nat`, whole numbers starting from 0), booleans (`Bool`), true or false values, strings |
| 11 | +* functions are defined using the `def` keyword (`def double (n : Nat) : Nat := n + n`) |
13 | 12 | * check types using `#check` |
14 | 13 | * evaluate expressions using `#eval` |
15 | 14 |
|
16 | 15 | <br> |
17 | 16 |
|
18 | 17 | --- |
19 | 18 |
|
20 | | -### function definitions |
| 19 | +### universes |
| 20 | + |
| 21 | +<br> |
| 22 | + |
| 23 | +* the two primary kinds of universes are `Prop` and `Type` |
| 24 | + |
| 25 | +<br> |
| 26 | + |
| 27 | +#### predicative |
| 28 | + |
| 29 | +<br> |
| 30 | + |
| 31 | +* a function that returns a proposition (a statement that can be true or false), or, of type `Prop` |
| 32 | +* for example, defining a predicate `is_empty` for lists: |
| 33 | + |
| 34 | +```lean |
| 35 | +def is_empty {α : Type} (l : List α) : Prop := |
| 36 | + l = [] |
| 37 | +``` |
| 38 | + |
| 39 | +* `...` represents whatever input the predicate takes |
| 40 | +* one can also define propositions inductively (i.e., instead of defining the property with a simple boolean check or an equality, one defines it by giving rules/constructors for when the proposition is true) |
| 41 | + |
| 42 | +<br> |
| 43 | + |
| 44 | +#### `Types` |
| 45 | + |
| 46 | +<br> |
| 47 | + |
| 48 | +* lean4's type theory is built upon a hierarchy of universes, which are types that contain other types (predicative) |
| 49 | +* this is a hierarchy of universes (Type 0, Type 1, Type 2, ...), where Type is an abbreviation for Type 0 |
| 50 | +* these universes contain "data" or computational types. |
| 51 | +* for instance, for a function type `(a : A) → B`, where `A : Type u` and `B : Type v`, the resulting function type itself resides in `Type (max u v)` |
| 52 | + |
| 53 | +<br> |
| 54 | + |
| 55 | +##### inductive types |
| 56 | + |
| 57 | +<br> |
| 58 | + |
| 59 | +* one of the predicative `Type` |
| 60 | +* a way of defining a new type by specifying its constructors. |
| 61 | + * used to define fundamental data structures like natural numbers (Nat), lists (List), and booleans (Bool), user-defined types |
| 62 | + * example for natural numbers, where `succ` is successor (takes a natural number and produces the next one) |
| 63 | + |
| 64 | +```lean |
| 65 | +inductive Nat where |
| 66 | + | zero : Nat |
| 67 | + | succ : Nat → Nat |
| 68 | +``` |
| 69 | + |
| 70 | +<br> |
| 71 | + |
| 72 | +##### inductive predicative types |
21 | 73 |
|
22 | 74 | <br> |
23 | 75 |
|
24 | | -* functions are defined using the `def` keyword: |
| 76 | +* inductive type defined to live in one of the Type universes (must adhere to the predicativity rules of the Type hierarchy) |
| 77 | +* for example, the definition of a polymorphic list, `MyList` lives in the same universe `u` as the type of its elements `α` |
25 | 78 |
|
26 | 79 | ```lean |
27 | | -def double (n : Nat) : Nat := n + n |
| 80 | +inductive MyList (α : Type u) : Type u where |
| 81 | + | nil : MyList α |
| 82 | + | cons : α → MyList α → MyList α |
28 | 83 | ``` |
| 84 | + |
| 85 | +<br> |
| 86 | + |
| 87 | +- universe polymorphism: same definition can be instantiated at different universe levels |
| 88 | +- large elimination: while one can freely define functions that pattern match on a Type-level inductive type to produce a value in any other Type, doing the same with a Prop-level inductive to produce a Type-level value is restricted (proofs in Prop are meant to be logically relevant but computationally erased, while data in Type has computational content) |
| 89 | + |
| 90 | +<br> |
| 91 | + |
| 92 | +--- |
| 93 | + |
| 94 | +#### `Prop` (propositions) |
| 95 | + |
| 96 | +<br> |
| 97 | + |
| 98 | +* impredicative (can quantify over any type, including types in higher universes and even Prop itself) |
| 99 | +* one can define a proposition that makes a statement about all types (for logical connectives -like `And`, `Or` - and quantifiers - `forall`, `exists`) |
0 commit comments