From cd4e3bb949b7764ad802b8f6c3341dfb7581c40d Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 11 Apr 2023 11:14:36 +0200 Subject: [PATCH] NNG levels --- server/nng/NNG/Levels/Function.lean | 23 ++++++++ server/nng/NNG/Levels/Function/Level_1.lean | 47 +++++++++++++++- server/nng/NNG/Levels/Function/Level_2.lean | 35 ++++++++++-- server/nng/NNG/Levels/Function/Level_3.lean | 59 ++++++++++++++++++++- server/nng/NNG/Levels/Function/Level_4.lean | 37 +++++++++++-- server/nng/NNG/Levels/Function/Level_5.lean | 29 +++++++++- server/nng/NNG/Levels/Function/Level_6.lean | 38 ++++++++++++- server/nng/NNG/Levels/Function/Level_7.lean | 15 ++++-- server/nng/NNG/Levels/Function/Level_8.lean | 52 +++++++++++++++++- server/nng/NNG/Levels/Power/Level_1.lean | 7 +-- server/nng/NNG/MyNat/Power.lean | 12 ++--- 11 files changed, 327 insertions(+), 27 deletions(-) diff --git a/server/nng/NNG/Levels/Function.lean b/server/nng/NNG/Levels/Function.lean index 5b7a403..5556be2 100644 --- a/server/nng/NNG/Levels/Function.lean +++ b/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. " \ No newline at end of file diff --git a/server/nng/NNG/Levels/Function/Level_1.lean b/server/nng/NNG/Levels/Function/Level_1.lean index 18aa81f..dec8165 100644 --- a/server/nng/NNG/Levels/Function/Level_1.lean +++ b/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 ` +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 diff --git a/server/nng/NNG/Levels/Function/Level_2.lean b/server/nng/NNG/Levels/Function/Level_2.lean index 1e27341..5c69454 100644 --- a/server/nng/NNG/Levels/Function/Level_2.lean +++ b/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. " diff --git a/server/nng/NNG/Levels/Function/Level_3.lean b/server/nng/NNG/Levels/Function/Level_3.lean index 1dc9c55..9654dd0 100644 --- a/server/nng/NNG/Levels/Function/Level_3.lean +++ b/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. " diff --git a/server/nng/NNG/Levels/Function/Level_4.lean b/server/nng/NNG/Levels/Function/Level_4.lean index ab2a23d..a14542d 100644 --- a/server/nng/NNG/Levels/Function/Level_4.lean +++ b/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 " diff --git a/server/nng/NNG/Levels/Function/Level_5.lean b/server/nng/NNG/Levels/Function/Level_5.lean index 8f00824..5a995e9 100644 --- a/server/nng/NNG/Levels/Function/Level_5.lean +++ b/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 diff --git a/server/nng/NNG/Levels/Function/Level_6.lean b/server/nng/NNG/Levels/Function/Level_6.lean index 7754306..5e97dd9 100644 --- a/server/nng/NNG/Levels/Function/Level_6.lean +++ b/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 diff --git a/server/nng/NNG/Levels/Function/Level_7.lean b/server/nng/NNG/Levels/Function/Level_7.lean index 6cf284b..2c51127 100644 --- a/server/nng/NNG/Levels/Function/Level_7.lean +++ b/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 diff --git a/server/nng/NNG/Levels/Function/Level_8.lean b/server/nng/NNG/Levels/Function/Level_8.lean index f715436..02f4837 100644 --- a/server/nng/NNG/Levels/Function/Level_8.lean +++ b/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 diff --git a/server/nng/NNG/Levels/Power/Level_1.lean b/server/nng/NNG/Levels/Power/Level_1.lean index 6a9192c..c6729a0 100644 --- a/server/nng/NNG/Levels/Power/Level_1.lean +++ b/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 " " + diff --git a/server/nng/NNG/MyNat/Power.lean b/server/nng/NNG/MyNat/Power.lean index a1a0a01..7ade13f 100644 --- a/server/nng/NNG/MyNat/Power.lean +++ b/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