doc: structures

doc/SUMMARY.md

@@ -16,7 +16,12 @@
   - [Namespaces](./namespaces.md)
   - [Implicit Arguments](./implicit.md)
   - [Auto Bound Implicit Arguments](./autobound.md)
-- [Functions](./functions.md)
+- [Declaring New Types](./decltypes.md)
+  - [Enumerated Types](./enum.md)
+  - [Inductive Types](./inductive.md)
+  - [Structures](./struct.md)
+  - [Type classes](./typeclass.md)
+  - [Unification Hints](./unifhint.md)
 - [Builtin Types](./builtintypes.md)
   - [Natural number](./nat.md)
   - [Integer](./int.md)
@@ -29,7 +34,7 @@
   - [Option](./option.md)
   - [Thunk](./thunk.md)
   - [Task and Thread](./task.md)
-- [Type classes](./typeclass.md)
+- [Functions](./functions.md)
 - [The `do` Notation](./do.md)
 - [Tactics](./tactics.md)
 - [String interpolation](./stringinterp.md)

doc/decltypes.md

@@ -0,0 +1,29 @@
+# Declaring New Types
+
+In Lean's library, every concrete type other than the universes and every type constructor other than the dependent function type is
+an instance of a general family of type constructions known as *inductive types*. It is remarkable that it is possible to develop
+complex programs and formalize mathematics based on nothing more than the type universes, dependent function types,
+and inductive types; everything else follows from those.
+
+Intuitively, an inductive type is built up from a specified list of constructors. In Lean, the basic syntax for specifying such a type is as follows:
+```
+inductive NewType where
+  | constructor_1 : ... → NewType
+  | constructor_2 : ... → NewType
+  ...
+  | constructor_n : ... → NewType
+```
+
+The intuition is that each constructor specifies a way of building new objects of ``NewType``, possibly from previously constructed values.
+The type ``NewType`` consists of nothing more than the objects that are constructed in this way.
+
+We will see below that the arguments to the constructors can include objects of type ``NewType``,
+subject to a certain "positivity" constraint, which guarantees that elements of ``NewType`` are built
+from the bottom up. Roughly speaking, each ``...`` can be any function type type constructed from ``NewType``
+and previously defined types, in which ``NewType`` appears, if at all, only as the "target" of the function type.
+
+We will provide a number of examples of inductive types. We will also consider slight generalizations of the scheme above,
+to mutually defined inductive types, and so-called *inductive families*.
+
+Every inductive type comes with constructors, which show how to construct an element of the type, and elimination rules,
+which show how to "use" an element of the type in another construction.

doc/enum.md

@@ -0,0 +1,190 @@
+# Enumerated Types
+
+The simplest kind of inductive type is simply a type with a finite, enumerated list of elements.
+The following command declares the enumerated type `Weekday`.
+```lean
+inductive Weekday where
+  | sunday    : Weekday
+  | monday    : Weekday
+  | tuesday   : Weekday
+  | wednesday : Weekday
+  | thursday  : Weekday
+  | friday    : Weekday
+  | saturday  : Weekday
+```
+
+The `Weekday` type has 7 constructors/elements. The constructors live in the `Weekday` namespace
+Think of `sunday`, `monday`, …, saturday as being distinct elements of `Weekday`,
+with no other distinguishing properties.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+#check Weekday.sunday   -- Weekday
+#check Weekday.monday   -- Weekday
+```
+
+You can define functions by pattern matching.
+The following function converts a `Weekday` into a natural number.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+def natOfWeekday (d : Weekday) : Nat :=
+  match d with
+  | Weekday.sunday    => 1
+  | Weekday.monday    => 2
+  | Weekday.tuesday   => 3
+  | Weekday.wednesday => 4
+  | Weekday.thursday  => 5
+  | Weekday.friday    => 6
+  | Weekday.saturday  => 7
+
+#eval natOfWeekday Weekday.tuesday -- 3
+```
+
+It is often useful to group definitions related to a type in a namespace with the same name.
+For example, we can put the function above into the ``Weekday`` namespace.
+We are then allowed to use the shorter name when we open the namespace.
+
+In the following example, wedefine functions from ``Weekday`` to ``Weekday`` in the namespace `Weekday`.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+namespace Weekday
+
+def next (d : Weekday) : Weekday :=
+  match d with
+  | sunday    => monday
+  | monday    => tuesday
+  | tuesday   => wednesday
+  | wednesday => thursday
+  | thursday  => friday
+  | friday    => saturday
+  | saturday  => sunday
+
+end Weekday
+```
+It is so common to start a definition with a `match` in Lean, that Lean provides a syntax sugar for it.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+def previous : Weekday -> Weekday
+  | sunday    => saturday
+  | monday    => sunday
+  | tuesday   => monday
+  | wednesday => tuesday
+  | thursday  => wednesday
+  | friday    => thursday
+  | saturday  => friday
+# end Weekday
+```
+We can use the command `#eval` to test our definitions.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+# def next (d : Weekday) : Weekday :=
+#  match d with
+#  | sunday    => monday
+#  | monday    => tuesday
+#  | tuesday   => wednesday
+#  | wednesday => thursday
+#  | thursday  => friday
+#  | friday    => saturday
+#  | saturday  => sunday
+# def previous : Weekday -> Weekday
+#  | sunday    => saturday
+#  | monday    => sunday
+#  | tuesday   => monday
+#  | wednesday => tuesday
+#  | thursday  => wednesday
+#  | friday    => thursday
+#  | saturday  => friday
+def toString : Weekday -> String
+  | sunday    => "Sunday"
+  | monday    => "Monday"
+  | tuesday   => "Tuesday"
+  | wednesday => "Wednesday"
+  | thursday  => "Thursday"
+  | friday    => "Friday"
+  | saturday  => "Saturday"
+
+#eval toString (next sunday)             -- "Monday"
+#eval toString (next tuesday)            -- "Wednesday"
+#eval toString (previous wednesday)      -- "Tuesday"
+#eval toString (next (previous sunday))  -- "Sunday"
+#eval toString (next (previous monday))  -- "Monday"
+-- ..
+# end Weekday
+```
+We can now prove the general theorem that ``next (previous d) = d`` for any weekday ``d``.
+The idea is perform a proof by cases using `match`, and rely on the fact for each constructor both
+sides of the equality reduce to the same term.
+```lean
+# inductive Weekday where
+#  | sunday    : Weekday
+#  | monday    : Weekday
+#  | tuesday   : Weekday
+#  | wednesday : Weekday
+#  | thursday  : Weekday
+#  | friday    : Weekday
+#  | saturday  : Weekday
+# namespace Weekday
+# def next (d : Weekday) : Weekday :=
+#  match d with
+#  | sunday    => monday
+#  | monday    => tuesday
+#  | tuesday   => wednesday
+#  | wednesday => thursday
+#  | thursday  => friday
+#  | friday    => saturday
+#  | saturday  => sunday
+# def previous : Weekday -> Weekday
+#  | sunday    => saturday
+#  | monday    => sunday
+#  | tuesday   => monday
+#  | wednesday => tuesday
+#  | thursday  => wednesday
+#  | friday    => thursday
+#  | saturday  => friday
+theorem nextOfPrevious (d : Weekday) : next (previous d) = d :=
+  match d with
+  | sunday    => rfl
+  | monday    => rfl
+  | tuesday   => rfl
+  | wednesday => rfl
+  | thursday  => rfl
+  | friday    => rfl
+  | saturday  => rfl
+# end Weekday
+```

doc/inductive.md

@@ -0,0 +1,3 @@
+# Inductive Types
+
+TODO

doc/struct.md

@@ -0,0 +1,220 @@
+# Structures
+
+Structure is a special case of inductive datatype. It has only one constructor and is not recursive.
+Similar to the `inductive` command, the `structure` command introduces a namespace with the same name.
+The general form is as follows:
+```
+structure <name> <parameters> <parent-structures> where
+  <constructor-name> :: <fields>
+```
+Most parts are optional. Here is our first example.
+```lean
+structure Point (α : Type u) where
+  x : α
+  y : α
+```
+In the example above, the constructor name is not provided. So, the constructor is named `mk` by Lean.
+Values of type ``Point`` are created using `Point.mk a b` or `{ x := a, y := b : Point α }`. The latter can be
+written as `{ x := a, y := b }` when the expected type is known.
+The fields of a point ``p`` are accessed using ``Point.x p`` and ``Point.y p``. You can also the more compact notation `p.x` and `p.y` as a shorthand
+for `Point.x p` and `Point.y p`.
+```lean
+# structure Point (α : Type u) where
+#  x : α
+#  y : α
+#check Point
+#check Point       -- Type u -> Type u
+#check @Point.mk   -- {α : Type u} → α → α → Point α
+#check @Point.x    -- {α : Type u} → Point α → α
+#check @Point.y    -- {α : Type u} → Point α → α
+
+#check Point.mk 10 20                   -- Point Nat
+#check { x := 10, y := 20 : Point Nat } -- Point Nat
+
+def mkPoint (a : Nat) : Point Nat :=
+  { x := a, y := a }
+
+#eval (Point.mk 10 20).x                   -- 10
+#eval (Point.mk 10 20).y                   -- 20
+#eval { x := 10, y := 20 : Point Nat }.x   -- 10
+#eval { x := 10, y := 20 : Point Nat }.y   -- 20
+
+def addXY (p : Point Nat) : Nat :=
+  p.x + p.y
+
+#eval addXY { x := 10, y := 20 }    -- 30
+```
+In the notation `{ ... }`, if the fields are in different lines, the `,` is optional.
+```lean
+# structure Point (α : Type u) where
+#  x : α
+#  y : α
+def mkPoint (a : Nat) : Point Nat := {
+  x := a
+  y := a
+}
+```
+You can also use `where` instead of `:= { ... }`.
+```lean
+# structure Point (α : Type u) where
+#  x : α
+#  y : α
+def mkPoint (a : Nat) : Point Nat where
+  x := a
+  y := a
+```
+
+Here are some simple theorems about our `Point` type.
+```lean
+# structure Point (α : Type u) where
+#  x : α
+#  y : α
+theorem ex1 (a b : α) : (Point.mk a b).x = a :=
+  rfl
+
+theorem ex2 (a b : α) : (Point.mk a b).y = b :=
+  rfl
+
+theorem ex3 (a b : α) : Point.mk a b = { x := a, y := b } :=
+  rfl
+```
+
+The dot notation is convenient not just for accessing the projections of a structure,
+but also for applying functions defined in a namespace with the same name.
+If ``p`` has type ``Point``, the expression ``p.foo`` is interpreted as ``Point.foo p``,
+assuming that the first argument to ``foo`` has type ``Point``.
+The expression ``p.add q`` is therefore shorthand for ``Point.add p q`` in the example below.
+```lean
+structure Point (α : Type u) where
+  x : α
+  y : α
+
+def Point.add (p q : Point Nat) : Point Nat :=
+  { x := p.x + q.x, y := p.y + q.y }
+
+def p : Point Nat := Point.mk 1 2
+def q : Point Nat := Point.mk 3 4
+
+#eval (p.add q).x  -- 4
+#eval (p.add q).y  -- 6
+```
+
+After we introduce type classes, we show how to define a function like ``add`` so that
+it works generically for elements of ``Point α`` rather than just ``Point Nat``,
+assuming ``α`` has an associated addition operation.
+
+More generally, given an expression ``p.foo x y z``, Lean will insert ``p`` at the first argument to ``foo`` of type ``Point``.
+For example, with the definition of scalar multiplication below, ``p.smul 3`` is interpreted as ``Point.smul 3 p``.
+
+```lean
+structure Point (α : Type u) where
+  x : α
+  y : α
+
+def Point.smul (n : Nat) (p : Point Nat) :=
+  Point.mk (n * p.x) (n * p.y)
+
+def p : Point Nat :=
+  Point.mk 1 2
+
+#eval (p.smul 3).x -- 3
+#eval (p.smul 3).y -- 6
+```
+
+##  Inheritance
+
+We can *extend* existing structures by adding new fields. This feature allow us to simulate a form of *inheritance*.
+
+```lean
+structure Point (α : Type u) where
+  x : α
+  y : α
+
+inductive Color where
+  | red
+  | green
+  | blue
+
+structure ColorPoint (α : Type u) extends Point α where
+  color : Color
+
+#check { x := 10, y := 20, color := Color.red : ColorPoint Nat }
+-- { toPoint := { x := 10, y := 20 }, color := Color.red }
+```
+The output for the `check` command above suggests how Lean encoded inheritance and multiple inheritance.
+Lean uses fields to each parent structure.
+
+```lean
+structure Foo where
+  x : Nat
+  y : Nat
+
+structure Boo where
+  w : Nat
+  z : Nat
+
+structure Bla extends Foo, Boo where
+  bit : Bool
+
+#check Bla.mk -- Foo → Boo → Bool → Bla
+#check Bla.mk { x := 10, y := 20 } { w := 30, z := 40 } true
+#check { x := 10, y := 20, w := 30, z := 40, bit := true : Bla }
+#check { toFoo := { x := 10, y := 20 },
+         toBoo := { w := 30, z := 40 },
+         bit := true : Bla }
+
+theorem ex :
+    Bla.mk { x := x, y := y } { w := w, z := z } b
+    =
+    { x := x, y := y, w := w, z := z, bit := b } :=
+  rfl
+```
+
+## Default field values
+
+You can assign default value to fields when declaring a new structure.
+```lean
+inductive MessageSeverity
+  | error | warning
+
+structure Message where
+  fileName : String
+  pos      : Option Nat      := none
+  severity : MessageSeverity := MessageSeverity.error
+  caption  : String          := ""
+  data     : String
+
+def msg1 : Message :=
+  { fileName := "foo.lean", data := "failed to import file" }
+
+#eval msg1.pos      -- none
+#eval msg1.fileName -- "foo.lean"
+#eval msg1.caption  -- ""
+```
+When extending a structure, you can not only add new fields, but provide new default values for existing fields.
+```lean
+# inductive MessageSeverity
+#  | error | warning
+# structure Message where
+#  fileName : String
+#  pos      : Option Nat      := none
+#  severity : MessageSeverity := MessageSeverity.error
+#  caption  : String          := ""
+#  data     : String
+structure MessageExt extends Message where
+  timestamp : Nat
+  caption   := "extended" -- new default value for field `caption`
+
+def msg2 : MessageExt where
+  fileName  := "bar.lean"
+  data      := "error at initialization"
+  timestamp := 10
+
+#eval msg2.fileName  -- "bar.lean"
+#eval msg2.timestamp -- 10
+#eval msg2.caption   -- "extended"
+```
+
+## Updating structure fields
+
+TODO

doc/typeclass.md

@@ -99,11 +99,11 @@ Let us start with the first step of the program above, declaring an appropriate
 
 ```lean
 # namespace Ex
-class Inhabited (a : Type _) where
+class Inhabited (a : Type u) where
   default : a
 
 #check @Inhabited.default
--- Inhabited.default : {a : Type _} → [self : Inhabited a] → a
+-- Inhabited.default : {a : Type u} → [self : Inhabited a] → a
 # end Ex
 ```
 Note `Inhabited.default` doesn't have any explicit argument.
@@ -220,3 +220,11 @@ instance [Inhabited b] : Inhabited (a -> b) where
   default := fun _ => arbitrary
 ```
 As an exercise, try defining default instances for other types, such as `List` and `Sum` types.
+
+## Local instances
+
+TODO
+
+## Scoped Instances
+
+TODO

doc/unifhint.md

@@ -0,0 +1,5 @@
+# Unification Hints
+
+
+
+TODO