NNG levels

server/nng/NNG/Levels/Function.lean

@@ -15,4 +15,27 @@ Title "Function World"
 
 Introduction
 "
+If you have beaten Addition World, then you have got
+quite good at manipulating equalities in Lean using the `rw` tactic.
+But there are plenty of levels later on which will require you
+to manipulate functions, and `rw` is not the tool for you here.
+
+To manipulate functions effectively, we need to learn about a new collection
+of tactics, namely `exact`, `intro`, `have` and `apply`. These tactics
+are specially designed for dealing with functions. Of course we are
+ultimately interested in using these tactics to prove theorems
+about the natural numbers – but in this
+world there is little point in working with specific sets like `mynat`,
+everything works for general sets.
+
+So our notation for this level is: $P$, $Q$, $R$ and so on denote general sets,
+and $h$, $j$, $k$ and so on denote general
+functions between them. What we will learn in this world is how to use functions
+in Lean to push elements from set to set. A word of warning –
+even though there's no harm at all in thinking of $P$ being a set and $p$
+being an element, you will not see Lean using the notation $p\\in P$, because
+internally Lean stores $P$ as a \"Type\" and $p$ as a \"term\", and it uses `p : P`
+to mean \"$p$ is a term of type $P$\", Lean's way of expressing the idea that $p$
+is an element of the set $P$. You have seen this already – Lean has
+been writing `n : ℕ` to mean that $n$ is a natural number.
 "

server/nng/NNG/Levels/Function/Level_1.lean

@@ -5,18 +5,63 @@ import NNG.MyNat.Multiplication
 Game "NNG"
 World "Function"
 Level 1
-Title ""
+Title "the `exact` tactic"
 
 open MyNat
 
 Introduction
 "
+## A new kind of goal.
 
+All through addition world, our goals have been theorems,
+and it was our job to find the proofs.
+**The levels in function world aren't theorems**. This is the only world where
+the levels aren't theorems in fact. In function world the object of a level
+is to create an element of the set in the goal. The goal will look like `Goal: X`
+with $X$ a set and you get rid of the goal by constructing an element of $X$.
+I don't know if you noticed this, but you finished
+essentially every goal of Addition World (and Multiplication World and Power World,
+if you played them) with `rfl`.
+This tactic is no use to us here.
+We are going to have to learn a new way of solving goals – the `exact` tactic.
+
+
+## The `exact` tactic
+
+If you can explicitly see how to make an element of your goal set,
+i.e. you have a formula for it, then you can just write `exact <formula>`
+and this will close the goal.
 "
 
 Statement
 "If $P$ is true, and $P\\implies Q$ is also true, then $Q$ is true."
     (P Q : Prop) (p : P) (h : P → Q) : Q := by
+  Hint
+  "In this situation, we have sets $P$ and $Q$ (but Lean calls them types),
+  and an element $p$ of $P$ (written `p : P`
+  but meaning $p\\in P$). We also have a function $h$ from $P$ to $Q$,
+  and our goal is to construct an
+  element of the set $Q$. It's clear what to do *mathematically* to solve
+  this goal -- we can
+  make an element of $Q$ by applying the function $h$ to
+  the element $p$. But how to do it in Lean? There are at least two ways
+  to explain this idea to Lean,
+  and here we will learn about one of them, namely the method which
+  uses the `exact` tactic.
+
+  Concretely, `h p` is an element of type `Q`, so you can use `exact h p` to use it.
+
+  Note that while in mathematics you might write $h(p)$, in Lean you always avoid brackets
+  for function application: `h p`. Brackets are only used for grouping elements, for
+  example for repeated funciton application, you could write `g (h p)`.
+  "
+  Hint (hidden := true) "
+  **Important note**: Note that `exact h P,` won't work (with a capital $P$);
+  this is a common error I see from beginners.
+  $P$ is not an element of $P$, it's $p$ that is an element of $P$.
+
+  So try `exact h p`.
+  "
   exact h p
 
 NewTactic exact

server/nng/NNG/Levels/Function/Level_2.lean

@@ -5,24 +5,53 @@ import NNG.MyNat.Multiplication
 Game "NNG"
 World "Function"
 Level 2
-Title ""
+Title "the intro tactic"
 
 open MyNat
 
 Introduction
 "
-
+Let's make a function. Let's define the function on the natural
+numbers which sends a natural number $n$ to $3n+2$. You
+see that the goal is `ℕ → ℕ`. A mathematician
+might denote this set with some exotic name such as
+$\\operatorname{Hom}(\\mathbb{N},\\mathbb{N})$,
+but computer scientists use notation `X → Y` to denote the set of
+functions from `X` to `Y` and this name definitely has its merits.
+In type theory, `X → Y` is a type (the type of all functions from $X$ to $Y$),
+and `f : X → Y` means that `f` is a term
+of this type, i.e., $f$ is a function from $X$ to $Y$.
+
+To define a function $X\\to Y$ we need to choose an arbitrary
+element $x\\in X$ and then, perhaps using $x$, make an element of $Y$.
+The Lean tactic for \"let $x\\in X$ be arbitrary\" is `intro x`.
 "
 
 Statement
-""
+"We define a function from ℕ to ℕ."
     : ℕ → ℕ := by
+  Hint "To solve this goal,
+  you have to come up with a function from `ℕ`
+  to `ℕ`. Start with
+
+  `intro n`"
   intro n
+  Hint "Our job now is to construct a natural number, which is
+  allowed to depend on $n$. We can do this using `exact` and
+  writing a formula for the function we want to define. For example
+  we imported addition and multiplication at the top of this file,
+  so
+
+  `exact 3*n+2,`
+
+  will close the goal, ultimately defining the function $f(n)=3n+2$."
   exact 3 * n + 2
 
 NewTactic intro
 
 Conclusion
 "
+## Rule of thumb:
 
+If your goal is `P → Q` then `intro p` will make progress.
 "

server/nng/NNG/Levels/Function/Level_3.lean

@@ -5,27 +5,82 @@ import NNG.MyNat.Multiplication
 Game "NNG"
 World "Function"
 Level 3
-Title ""
+Title "the have tactic"
 
 open MyNat
 
 Introduction
 "
+Say you have a whole bunch of sets and functions between them,
+and your goal is to build a certain element of a certain set.
+If it helps, you can build intermediate elements of other sets
+along the way, using the `have` command. `have` is the Lean analogue
+of saying \"let's define an element $q\\in Q$ by...\" in the middle of a calculation.
+It is often not logically necessary, but on the other hand
+it is very convenient, for example it can save on notation, or
+it can break proofs or calculations up into smaller steps.
 
+In the level below, we have an element of $P$ and we want an element
+of $U$; during the proof we will make several intermediate elements
+of some of the other sets involved. The diagram of sets and
+functions looks like this pictorially:
+
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @V{j}VV           \\\\
+  S  @>{k}>> T       @>{l}>> U \\\\
+\\end{CD}
+$$
+
+and so it's clear how to make the element of $U$ from the element of $P$.
 "
 
 Statement
-""
+"Given an element of $P$ we can define an element of $U$."
     (P Q R S T U: Type) (p : P) (h : P → Q) (i : Q → R) (j : Q → T) (k : S → T) (l : T → U) :
     U := by
+  Hint "Indeed, we could solve this level in one move by typing
+
+  `exact l (j (h p))`
+
+  But let us instead stroll more lazily through the level.
+  We can start by using the `have` tactic to make an element of $Q$:
+
+  have q := h p"
+  Branch
+    exact l (j (h p))
   have q := h p
+  Hint "
+  and now we note that $j(q)$ is an element of $T$
+
+  `have t : T := j q`
+
+  (notice how we can explicitly tell Lean
+  what set we thought $t$ was in, with that `: T` thing before the `:=`.
+  This is optional unless Lean can not figure it out by itself.)
+  "
   have t : T := j q
+  Hint "
+  Now we could even define $u$ to be $l(t)$:
+
+  `have u : U := l t`
+  "
   have u : U := l t
+  Hint "…and then finish the level with `exact u`."
   exact u
 
 NewTactic «have»
 
 Conclusion
 "
+If you solved the level using `have`, then you might have observed
+that before the final step the context got quite messy by all the intermediate
+variables we introduced. You can click \"Toggle Editor\" and then move the cursor
+around to see the proof you created.
 
+The context was already bad enough to start with, and we added three more
+terms to it. In level 4 we will learn about the `apply` tactic
+which solves the level using another technique, without leaving
+so much junk behind.
 "

server/nng/NNG/Levels/Function/Level_4.lean

@@ -5,17 +5,30 @@ import NNG.MyNat.Multiplication
 Game "NNG"
 World "Function"
 Level 4
-Title ""
+Title "the `apply` tactic"
 
 open MyNat
 
 Introduction
-"
+"Let's do the same level again:
+
+$$
+\\begin{CD}
+  P  @>{h}>> Q       @>{i}>> R \\\\
+  @.         @V{j}VV           \\\\
+  S  @>{k}>> T       @>{l}>> U \\\\
+\\end{CD}
+$$
 
+We are given $p \\in P$ and our goal is to find an element of $U$, or
+in other words to find a path through the maze that links $P$ to $U$.
+In level 3 we solved this by using `have`s to move forward, from $P$
+to $Q$ to $T$ to $U$. Using the `apply` tactic we can instead construct
+the path backwards, moving from $U$ to $T$ to $Q$ to $P$.
 "
 
 Statement
-""
+"Given an element of $P$ we can define an element of $U$."
     (P Q R S T U: Type)
 (p : P)
 (h : P → Q)
@@ -24,12 +37,30 @@ Statement
 (k : S → T)
 (l : T → U) : U :=
 by
+  Hint "Our goal is to construct an element of the set $U$. But $l:T\\to U$ is
+  a function, so it would suffice to construct an element of $T$. Tell
+  Lean this by starting the proof below with
+
+  `apply l`"
   apply l
+  Hint "Notice that our assumptions don't change but *the goal changes*
+  from `Goal: U` to `Goal: T`.
+
+  Keep `apply`ing functions until your goal is `P`, and try not
+  to get lost!"
+  Branch
+    apply k
+    Hint "Looks like you got lost. \"Undo\" the last step."
   apply j
   apply h
+  Hint " Now solve this goal
+  with `exact p`. Note: you will need to learn the difference between
+  `exact p` (which works) and `exact P` (which doesn't, because $P$ is
+  not an element of $P$)."
   exact p
 
 NewTactic apply
+DisabledTactic «have»
 
 Conclusion
 "

server/nng/NNG/Levels/Function/Level_5.lean

@@ -5,20 +5,45 @@ import NNG.MyNat.Multiplication
 Game "NNG"
 World "Function"
 Level 5
-Title ""
+Title "P → (Q → P)"
 
 open MyNat
 
 Introduction
 "
+In this level, our goal is to construct a function, like in level 2.
 
+```
+P → (Q → P)
+```
+
+So $P$ and $Q$ are sets, and our goal is to construct a function
+which takes an element of $P$ and outputs a function from $Q$ to $P$.
+We don't know anything at all about the sets $P$ and $Q$, so initially
+this seems like a bit of a tall order. But let's give it a go.
 "
 
 Statement
-""
+"We define an element of $\\operatorname{Hom}(P,\\operatorname{Hom}(Q,P))$."
     (P Q : Type) : P → (Q → P) := by
+  Hint "Our goal is `P → X` for some set $X=\\operatorname\{Hom}(Q,P)$, and if our
+  goal is to construct a function then we almost always want to use the
+  `intro` tactic from level 2, Lean's version of \"let $p\\in P$ be arbitrary.\"
+  So let's start with
+
+  `intro p`"
   intro p
+  Hint "
+  We now have an arbitrary element $p\\in P$ and we are supposed to be constructing
+  a function $Q\to P$. Well, how about the constant function, which
+  sends everything to $p$?
+  This will work. So let $q\\in Q$ be arbitrary:
+
+  `intro q`"
   intro q
+  Hint "and then let's output `p`.
+
+  `exact p`"
   exact p
 
 Conclusion

server/nng/NNG/Levels/Function/Level_6.lean

@@ -4,21 +4,55 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Function"
 Level 6
-Title ""
+Title "(P → (Q → R)) → ((P → Q) → (P → R))"
 
 open MyNat
 
 Introduction
 "
+You can solve this level completely just using `intro`, `apply` and `exact`,
+but if you want to argue forwards instead of backwards then don't forget
+that you can do things like
 
+`have j : Q → R := f p`
+
+if `f : P → (Q → R)` and `p : P`. Remember the trick with the colon in `have`:
+we could just write `have j := f p,` but this way we can be sure that `j` is
+what we actually expect it to be.
+
+I recommend that you start with `intro f` rather than `intro p`
+because even though the goal starts `P → ...`, the brackets mean that
+the goal is not a function from `P` to anything, it's a function from
+`P → (Q → R)` to something. In fact you can save time by starting
+with `intros f h p`, which introduces three variables at once, although you'd
+better then look at your tactic state to check that you called all those new
+terms sensible things.
+
+After all the intros, you find that your your goal is `Goal: R`…
 "
 
 Statement
-""
+"Whatever the sets $P$ and $Q$ and $R$ are, we
+make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,\\operatorname{Hom}(Q,R)),
+\\operatorname{Hom}(\\operatorname{Hom}(P,Q),\\operatorname{Hom}(P,R)))$."
     (P Q R : Type) : (P → (Q → R)) → ((P → Q) → (P → R)) := by
   intro f
   intro h
   intro p
+  Hint "
+  If you try `have j : {Q} → {R} := {f} {p}`
+  now then you can `apply j`.
+
+  Alternatively you can `apply ({f} {p})` directly.
+
+  What happens if you just try `apply {f}`?
+  "
+  Branch
+    apply f
+    Hint "Can you figure out what just happened? This is a little
+    `apply` easter egg. Why is it mathematically valid?"
+    Hint (hidden := true) "Note that there are two goals now, first you need to
+    provide an element in ${P}$ which you did not provide before."
   have j : Q → R := f p
   apply j
   apply h

server/nng/NNG/Levels/Function/Level_7.lean

@@ -4,17 +4,26 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Function"
 Level 7
-Title ""
+Title "(P → Q) → ((Q → F) → (P → F))"
 
 open MyNat
 
 Introduction
 "
-
+Have you noticed that, in stark contrast to earlier worlds,
+we are not amassing a large collection of useful theorems?
+We really are just constructing abstract levels with sets and
+functions, and then solving them and never using the results
+ever again. Here's another one, which should hopefully be
+very easy for you now. Advanced mathematician viewers will
+know it as contravariance of $\\operatorname{Hom}(\\cdot,F)$
+functor.
 "
 
 Statement
-""
+"Whatever the sets $P$ and $Q$ and $F$ are, we 
+make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
+\\operatorname{Hom}(\\operatorname{Hom}(Q,F),\\operatorname{Hom}(P,F)))$."
     (P Q F : Type) : (P → Q) → ((Q → F) → (P → F)) := by
   intro f
   intro h

server/nng/NNG/Levels/Function/Level_8.lean

@@ -4,19 +4,67 @@ import NNG.MyNat.Addition
 Game "NNG"
 World "Function"
 Level 8
-Title ""
+Title "(P → Q) → ((Q → empty) → (P → empty))"
 
 open MyNat
 
 Introduction
 "
+Level 8 is the same as level 7, except we have replaced the
+set $F$ with the empty set $\\emptyset$. The same proof will work (after all, our
+previous proof worked for all sets, and the empty set is a set).
+But note that if you start with `intro f, intro h, intro p,`
+(which can incidentally be shortened to `intros f h p`),
+then the local context looks like this:
 
+```
+P Q : Type,
+f : P → Q,
+h : Q → empty,
+p : P
+⊢ empty
+```
+
+and your job is to construct an element of the empty set!
+This on the face of it seems hard, but what is going on is that
+our hypotheses (we have an element of $P$, and functions $P\\to Q$
+and $Q\\to\\emptyset$) are themselves contradictory, so
+I guess we are doing some kind of proof by contradiction at this point? However,
+if your next line is `apply h` then all of a sudden the goal
+seems like it might be possible again. If this is confusing, note
+that the proof of the previous world worked for all sets $F$, so in particular
+it worked for the empty set, you just probably weren't really thinking about
+this case explicitly beforehand. [Technical note to constructivists: I know
+that we are not doing a proof by contradiction. But how else do you explain
+to a classical mathematician that their goal is to prove something false
+and this is OK because their hypotheses don't add up?]
 "
 
 Statement
-""
+"Whatever the sets $P$ and $Q$ are, we
+make an element of $\\operatorname{Hom}(\\operatorname{Hom}(P,Q),
+\\operatorname{Hom}(\\operatorname{Hom}(Q,\\emptyset),\\operatorname{Hom}(P,\\emptyset)))$."
     (P Q : Type) : (P → Q) → ((Q → Empty) → (P → Empty)) := by
   intros f h p
+  Hint "
+  Note that now your job is to construct an element of the empty set!
+  This on the face of it seems hard, but what is going on is that
+  our hypotheses (we have an element of $P$, and functions $P\\to Q$
+  and $Q\\to\\emptyset$) are themselves contradictory, so
+  I guess we are doing some kind of proof by contradiction at this point? However,
+  if your next line is 
+
+  `apply {h}`
+
+  then all of a sudden the goal
+  seems like it might be possible again. If this is confusing, note
+  that the proof of the previous world worked for all sets $F$, so in particular
+  it worked for the empty set, you just probably weren't really thinking about
+  this case explicitly beforehand. [Technical note to constructivists: I know
+  that we are not doing a proof by contradiction. But how else do you explain
+  to a classical mathematician that their goal is to prove something false
+  and this is OK because their hypotheses don't add up?]
+  "
   apply h
   apply f
   exact p

server/nng/NNG/Levels/Power/Level_1.lean

@@ -1,5 +1,5 @@
 import NNG.Metadata
-import NNG.MyNat.Addition
+--import NNG.MyNat.Power
 
 Game "NNG"
 World "Power"
@@ -14,11 +14,12 @@ Introduction
 "
 
 Statement
-""
-    : true := by
+"$0 ^ 0 = 1$"
+    : true := by -- (0 : ℕ) ^ (0 : ℕ) = 1 := by
   trivial
 
 Conclusion
 "
 
 "
+

server/nng/NNG/MyNat/Power.lean

@@ -1,21 +1,21 @@
-import NNG.MyNat.Definition
+import NNG.MyNat.Multiplication
 namespace MyNat
 open MyNat
 
-def pow : MyNat → MyNat → MyNat
+def pow : ℕ → ℕ → ℕ
 | _, zero => one
 | m, (succ n) => pow m n * m
 
-instance : Pow MyNat MyNat where
+instance : Pow ℕ ℕ where
   pow := pow
 
 -- notation a ^ b := pow a b
 
-example : (1 : MyNat) ^ (1 : MyNat) = 1 := rfl
+example : (1 : ℕ) ^ (1 : ℕ) = 1 := rfl
 
-lemma pow_zero (m : MyNat) : m ^ (0 : MyNat) = 1 := rfl
+lemma pow_zero (m : ℕ) : m ^ (0 : ℕ) = 1 := rfl
 
-lemma pow_succ (m n : MyNat) : m ^ (succ n) = m ^ n * m := rfl
+lemma pow_succ (m n : ℕ) : m ^ (succ n) = m ^ n * m := rfl
 
 end MyNat