From cbaeb0452cc6197123379b5b11d1eced98ebc4a8 Mon Sep 17 00:00:00 2001 From: Kevin Buzzard Date: Sat, 12 Aug 2023 05:01:29 +0100 Subject: [PATCH] making the full graph --- Game.lean | 18 ++++++----- Game/Levels/AdvAddition.lean | 2 +- Game/Levels/AdvMultiplication.lean | 6 ++-- Game/Levels/AdvProposition.lean | 23 -------------- Game/Levels/EvenOdd.lean | 0 Game/Levels/Function.lean | 41 ------------------------- Game/Levels/Hard.lean | 0 Game/Levels/Multiplication.lean | 14 +++------ Game/Levels/Power.lean | 2 +- Game/Levels/Prime.lean | 0 Game/Levels/Proposition.lean | 48 ------------------------------ Game/Levels/StrongInduction.lean | 0 12 files changed, 19 insertions(+), 135 deletions(-) delete mode 100644 Game/Levels/AdvProposition.lean create mode 100644 Game/Levels/EvenOdd.lean delete mode 100644 Game/Levels/Function.lean create mode 100644 Game/Levels/Hard.lean create mode 100644 Game/Levels/Prime.lean delete mode 100644 Game/Levels/Proposition.lean create mode 100644 Game/Levels/StrongInduction.lean diff --git a/Game.lean b/Game.lean index 189221e..05c355e 100644 --- a/Game.lean +++ b/Game.lean @@ -2,13 +2,17 @@ import GameServer.Commands import Game.Levels.Tutorial import Game.Levels.Addition ---import Game.Levels.Multiplication ---import Game.Levels.Power ---import Game.Levels.Function ---import Game.Levels.Proposition ---import Game.Levels.AdvProposition ---import Game.Levels.AdvAddition ---import Game.Levels.AdvMultiplication +import Game.Levels.Multiplication +import Game.Levels.Power +import Game.Levels.AdvAddition +import Game.Levels.AdvMultiplication +import Game.Levels.EvenOdd +import Game.Levels.Inequality +import Game.Levels.Prime +import Game.Levels.StrongInduction +import Game.Levels.Hard + + --import Game.Levels.Inequality Title "Natural Number Game" diff --git a/Game/Levels/AdvAddition.lean b/Game/Levels/AdvAddition.lean index ad49125..c878c62 100644 --- a/Game/Levels/AdvAddition.lean +++ b/Game/Levels/AdvAddition.lean @@ -1,4 +1,4 @@ -import Game.Levels.AdvAddition.Level_13 +import Game.Levels.Addition World "AdvAddition" diff --git a/Game/Levels/AdvMultiplication.lean b/Game/Levels/AdvMultiplication.lean index 19bc752..fff7644 100644 --- a/Game/Levels/AdvMultiplication.lean +++ b/Game/Levels/AdvMultiplication.lean @@ -1,7 +1,5 @@ -import Game.Levels.AdvMultiplication.Level_1 -import Game.Levels.AdvMultiplication.Level_2 -import Game.Levels.AdvMultiplication.Level_3 -import Game.Levels.AdvMultiplication.Level_4 +import Game.Levels.Multiplication +import Game.Levels.AdvAddition diff --git a/Game/Levels/AdvProposition.lean b/Game/Levels/AdvProposition.lean deleted file mode 100644 index 9af0523..0000000 --- a/Game/Levels/AdvProposition.lean +++ /dev/null @@ -1,23 +0,0 @@ -import Game.Levels.AdvProposition.Level_1 -import Game.Levels.AdvProposition.Level_2 -import Game.Levels.AdvProposition.Level_3 -import Game.Levels.AdvProposition.Level_4 -import Game.Levels.AdvProposition.Level_5 -import Game.Levels.AdvProposition.Level_6 -import Game.Levels.AdvProposition.Level_7 -import Game.Levels.AdvProposition.Level_8 -import Game.Levels.AdvProposition.Level_9 -import Game.Levels.AdvProposition.Level_10 - - - -World "AdvProposition" -Title "Advanced Proposition World" - -Introduction -" -In this world we will learn five key tactics needed to solve all the -levels of the Natural Number Game, namely `constructor`, `rcases`, `left`, `right`, and `exfalso`. -These, and `use` (which we'll get to in Inequality World) are all the -tactics you will need to beat all the levels of the game. -" diff --git a/Game/Levels/EvenOdd.lean b/Game/Levels/EvenOdd.lean new file mode 100644 index 0000000..e69de29 diff --git a/Game/Levels/Function.lean b/Game/Levels/Function.lean deleted file mode 100644 index a296471..0000000 --- a/Game/Levels/Function.lean +++ /dev/null @@ -1,41 +0,0 @@ -import Game.Levels.Function.Level_1 -import Game.Levels.Function.Level_2 -import Game.Levels.Function.Level_3 -import Game.Levels.Function.Level_4 -import Game.Levels.Function.Level_5 -import Game.Levels.Function.Level_6 -import Game.Levels.Function.Level_7 -import Game.Levels.Function.Level_8 -import Game.Levels.Function.Level_9 - - - -World "Function" -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. -" diff --git a/Game/Levels/Hard.lean b/Game/Levels/Hard.lean new file mode 100644 index 0000000..e69de29 diff --git a/Game/Levels/Multiplication.lean b/Game/Levels/Multiplication.lean index c4c4c62..7af20c1 100644 --- a/Game/Levels/Multiplication.lean +++ b/Game/Levels/Multiplication.lean @@ -1,13 +1,4 @@ -import Game.Levels.Multiplication.Level_1 -import Game.Levels.Multiplication.Level_2 -import Game.Levels.Multiplication.Level_3 -import Game.Levels.Multiplication.Level_4 -import Game.Levels.Multiplication.Level_5 -import Game.Levels.Multiplication.Level_6 -import Game.Levels.Multiplication.Level_7 -import Game.Levels.Multiplication.Level_8 -import Game.Levels.Multiplication.Level_9 - +import Game.Levels.Addition World "Multiplication" @@ -15,6 +6,9 @@ Title "Multiplication World" Introduction " + We define multiplication, and prove that the naturals are a commutative semiring. + + In this world you start with the definition of multiplication on `ℕ`. It is defined by recursion, just like addition was. So you get two new axioms: diff --git a/Game/Levels/Power.lean b/Game/Levels/Power.lean index e1b602f..055727e 100644 --- a/Game/Levels/Power.lean +++ b/Game/Levels/Power.lean @@ -1,4 +1,4 @@ -import Game.Levels.Power.Level_8 +import Game.Levels.Multiplication World "Power" diff --git a/Game/Levels/Prime.lean b/Game/Levels/Prime.lean new file mode 100644 index 0000000..e69de29 diff --git a/Game/Levels/Proposition.lean b/Game/Levels/Proposition.lean deleted file mode 100644 index 4baf164..0000000 --- a/Game/Levels/Proposition.lean +++ /dev/null @@ -1,48 +0,0 @@ -import Game.Levels.Proposition.Level_1 -import Game.Levels.Proposition.Level_2 -import Game.Levels.Proposition.Level_3 -import Game.Levels.Proposition.Level_4 -import Game.Levels.Proposition.Level_5 -import Game.Levels.Proposition.Level_6 -import Game.Levels.Proposition.Level_7 -import Game.Levels.Proposition.Level_8 -import Game.Levels.Proposition.Level_9 -- `cc` is not ported - - - -World "Proposition" -Title "Proposition World" - -Introduction -" -A Proposition is a true/false statement, like `2 + 2 = 4` or `2 + 2 = 5`. -Just like we can have concrete sets in Lean like `mynat`, and abstract -sets called things like `X`, we can also have concrete propositions like -`2 + 2 = 5` and abstract propositions called things like `P`. - -Mathematicians are very good at conflating a theorem with its proof. -They might say \"now use theorem 12 and we're done\". What they really -mean is \"now use the proof of theorem 12...\" (i.e. the fact that we proved -it already). Particularly problematic is the fact that mathematicians -use the word Proposition to mean \"a relatively straightforward statement -which is true\" and computer scientists use it to mean \"a statement of -arbitrary complexity, which might be true or false\". Computer scientists -are far more careful about distinguishing between a proposition and a proof. -For example: `x + 0 = x` is a proposition, and `add_zero x` -is its proof. The convention we'll use is capital letters for propositions -and small letters for proofs. - -In this world you will see the local context in the following kind of state: - -``` -Objects: - P : Prop -Assumptions: - p : P -``` - -Here `P` is the true/false statement (the statement of proposition), and `p` is its proof. -It's like `P` being the set and `p` being the element. In fact computer scientists -sometimes think about the following analogy: propositions are like sets, -and their proofs are like their elements. -" diff --git a/Game/Levels/StrongInduction.lean b/Game/Levels/StrongInduction.lean new file mode 100644 index 0000000..e69de29