greg/NNG
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

making the full graph

Browse Source
This commit is contained in:
Kevin Buzzard
2023-08-12 05:01:29 +01:00
parent 720f3320eb
commit cbaeb0452c
12 changed files with 19 additions and 135 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
Game.lean
View File

@@ -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"

2
Game/Levels/AdvAddition.lean
View File

@@ -1,4 +1,4 @@
import Game.Levels.AdvAddition.Level_13
import Game.Levels.Addition
World "AdvAddition"

6
Game/Levels/AdvMultiplication.lean
View File

@@ -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

23
Game/Levels/AdvProposition.lean
View File

@@ -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.
"

0
Game/Levels/EvenOdd.lean Normal file
View File

41
Game/Levels/Function.lean
View File

@@ -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.
"

0
Game/Levels/Hard.lean Normal file
View File

14
Game/Levels/Multiplication.lean
View File

@@ -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:

2
Game/Levels/Power.lean
View File

@@ -1,4 +1,4 @@
import Game.Levels.Power.Level_8
import Game.Levels.Multiplication
World "Power"

0
Game/Levels/Prime.lean Normal file
View File

48
Game/Levels/Proposition.lean
View File

@@ -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.
"

0
Game/Levels/StrongInduction.lean Normal file
View File