Skip to content

Commit 2bf25b8

Browse files
kisonecatkisonecat
committed
Some more levels
1 parent 2ad12b9 commit 2bf25b8

14 files changed

Lines changed: 256 additions & 78 deletions

‎.i18n/en/Game.pot‎

Lines changed: 38 additions & 28 deletions
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
msgid ""
22
msgstr "Project-Id-Version: Game v4.7.0\n"
33
"Report-Msgid-Bugs-To: \n"
4-
"POT-Creation-Date: Wed Apr 10 15:31:40 2024\n"
4+
"POT-Creation-Date: Wed Jun 18 11:43:39 2025\n"
55
"Last-Translator: \n"
66
"Language-Team: none\n"
77
"Language: en\n"
@@ -20,62 +20,72 @@ msgstr ""
2020
msgid "intermediate goal solved! 🎉"
2121
msgstr ""
2222

23-
#: Game.Levels.DemoWorld.L01_HelloWorld
24-
msgid "Hello World"
23+
#: Game.Levels.AxiomWorld.L01_Addition
24+
msgid "Addition"
2525
msgstr ""
2626

27-
#: Game.Levels.DemoWorld.L01_HelloWorld
27+
#: Game.Levels.AxiomWorld.L01_Addition
28+
msgid "We begin by checking facts about addition."
29+
msgstr ""
30+
31+
#: Game.Levels.AxiomWorld.L01_Addition
32+
msgid "associativity of addition in a ring"
33+
msgstr ""
34+
35+
#: Game.Levels.AxiomWorld.L01_Addition
36+
msgid "commutativity of addition in a ring"
37+
msgstr ""
38+
39+
#: Game.Levels.AxiomWorld.L01_Addition
40+
msgid "But rings do not only have addition: there is also multiplication!"
41+
msgstr ""
42+
43+
#: Game.Levels.AxiomWorld.L02_Multiplication
44+
msgid "Multiplication"
45+
msgstr ""
46+
47+
#: Game.Levels.AxiomWorld.L02_Multiplication
2848
msgid "This text is shown as first message when the level is played.\n"
2949
"You can insert hints in the proof below. They will appear in this side panel\n"
3050
"depending on the proof a user provides."
3151
msgstr ""
3252

33-
#: Game.Levels.DemoWorld.L01_HelloWorld
34-
msgid "You can either start using `«{h}»` or `«{g}»`."
35-
msgstr ""
36-
37-
#: Game.Levels.DemoWorld.L01_HelloWorld
38-
msgid "You should use `«{h}»` now."
53+
#: Game.Levels.AxiomWorld.L02_Multiplication
54+
msgid "associativity of multiplication in a ring"
3955
msgstr ""
4056

41-
#: Game.Levels.DemoWorld.L01_HelloWorld
42-
msgid "You should use `«{g}»` now."
57+
#: Game.Levels.AxiomWorld.L02_Multiplication
58+
msgid "commuativity of multiplication in a ring"
4359
msgstr ""
4460

45-
#: Game.Levels.DemoWorld.L01_HelloWorld
61+
#: Game.Levels.AxiomWorld.L02_Multiplication
4662
msgid "This last message appears if the level is solved."
4763
msgstr ""
4864

49-
#: Game.Levels.DemoWorld
50-
msgid "Demo World"
65+
#: Game.Levels.AxiomWorld
66+
msgid "Axiom World"
5167
msgstr ""
5268

53-
#: Game.Levels.DemoWorld
54-
msgid "This introduction is shown before one enters level 1 of the demo world. Use markdown."
69+
#: Game.Levels.AxiomWorld
70+
msgid "We introduce the ring axioms."
5571
msgstr ""
5672

5773
#: Game
58-
msgid "Hello World Game"
74+
msgid "Ross Game"
5975
msgstr ""
6076

6177
#: Game
62-
msgid "This text appears on the starting page where one selects the world/level to play.\n"
63-
"You can use markdown."
78+
msgid "This is an introduction to Lean for the participants of the Ross Mathematics Program."
6479
msgstr ""
6580

6681
#: Game
67-
msgid "Here you can put additional information about the game. It is accessible\n"
68-
"from the starting through the drop-down menu.\n"
69-
"\n"
70-
"For example: Game version, Credits, Link to Github and Zulip, etc.\n"
71-
"\n"
72-
"Use markdown."
82+
msgid "https://github.com/rossprogram/integer-game"
7383
msgstr ""
7484

7585
#: Game
76-
msgid "Game Template"
86+
msgid "Integer Game"
7787
msgstr ""
7888

7989
#: Game
80-
msgid "You should use this game as a template for your own game and add your own levels."
90+
msgid "Learn Lean at the Ross Mathematics Program"
8191
msgstr ""

‎Game.lean‎

Lines changed: 6 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1,26 +1,20 @@
1-
import Game.Levels.DemoWorld
1+
import Game.Levels.AxiomWorld
22

33
-- Here's what we'll put on the title screen
4-
Title "Hello World Game"
4+
Title "Ross Game"
55
Introduction
66
"
7-
This text appears on the starting page where one selects the world/level to play.
8-
You can use markdown.
7+
This is an introduction to Lean for the participants of the Ross Mathematics Program.
98
"
109

1110
Info "
12-
Here you can put additional information about the game. It is accessible
13-
from the starting through the drop-down menu.
14-
15-
For example: Game version, Credits, Link to Github and Zulip, etc.
16-
17-
Use markdown.
11+
https://github.com/rossprogram/integer-game
1812
"
1913

2014
/-! Information to be displayed on the servers landing page. -/
2115
Languages "English"
22-
CaptionShort "Game Template"
23-
CaptionLong "You should use this game as a template for your own game and add your own levels."
16+
CaptionShort "Integer Game"
17+
CaptionLong "Learn Lean at the Ross Mathematics Program"
2418
-- Prerequisites "" -- add this if your game depends on other games
2519
-- CoverImage "images/cover.png"
2620

‎Game/Levels/AxiomWorld.lean‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
import Game.Levels.AxiomWorld.L01_Addition
2+
import Game.Levels.AxiomWorld.L02_Multiplication
3+
import Game.Levels.AxiomWorld.L03_Together
4+
import Game.Levels.AxiomWorld.L04_Distributivity
5+
import Game.Levels.AxiomWorld.L05_Identities
6+
import Game.Levels.AxiomWorld.L06_Inverses
7+
8+
World "AxiomWorld"
9+
Title "Axiom World"
10+
11+
Introduction "
12+
We introduce the ring axioms.
13+
"

‎Game/Levels/AxiomWorld/L01_Addition.lean‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
import Game.Metadata
2+
3+
World "AxiomWorld"
4+
Level 1
5+
6+
Title "Addition"
7+
8+
Introduction "We begin by checking facts about addition."
9+
10+
variable {R : Type}
11+
variable [CommRing R]
12+
13+
/-- associativity of addition in a ring -/
14+
TheoremDoc add_assoc as "add_assoc" in "Ring"
15+
16+
/-- commutativity of addition in a ring -/
17+
TheoremDoc add_comm as "add_comm" in "Ring"
18+
19+
NewTheorem add_assoc add_comm
20+
21+
NewTactic rw
22+
23+
Statement ( x y : R ) : x + y = y + x := by
24+
rw [add_comm]
25+
26+
Conclusion "But rings do not only have addition: there is also multiplication!"

‎Game/Levels/AxiomWorld/L02_Multiplication.lean‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
import Game.Metadata
2+
import Mathlib.Algebra.Ring.Defs
3+
import Mathlib.Tactic.Use
4+
5+
World "AxiomWorld"
6+
Level 2
7+
8+
Title "Multiplication"
9+
10+
variable {R : Type}
11+
variable [CommRing R]
12+
13+
Introduction "This text is shown as first message when the level is played.
14+
You can insert hints in the proof below. They will appear in this side panel
15+
depending on the proof a user provides."
16+
17+
/-- associativity of multiplication in a ring -/
18+
TheoremDoc mul_assoc as "mul_assoc" in "Ring"
19+
20+
/-- commuativity of multiplication in a ring -/
21+
TheoremDoc mul_comm as "mul_comm" in "Ring"
22+
23+
NewTheorem mul_assoc mul_comm
24+
25+
NewTactic rw
26+
27+
Statement ( a b : R ) : a * b = b * a := by
28+
rw [mul_comm]
29+
30+
Conclusion "This last message appears if the level is solved."

‎Game/Levels/AxiomWorld/L03_Together.lean‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
import Game.Metadata
2+
import Mathlib.Algebra.Ring.Defs
3+
import Mathlib.Tactic.Use
4+
5+
World "AxiomWorld"
6+
Level 3
7+
8+
Title "Together"
9+
10+
variable {R : Type}
11+
variable [CommRing R]
12+
13+
Introduction "Let's invoke multiple axioms to prove something."
14+
15+
Statement ( a b : R ) : a * b + c = c + b * a := by
16+
rw [mul_comm]
17+
rw [add_comm]
18+
19+
Conclusion "Next we'll combine multiplication and addition via distributivity."

‎Game/Levels/AxiomWorld/L04_Distributivity.lean‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
import Game.Metadata
2+
import Mathlib.Algebra.Ring.Defs
3+
import Mathlib.Tactic.Use
4+
5+
World "AxiomWorld"
6+
Level 4
7+
8+
Title "Distributivity"
9+
10+
variable {R : Type}
11+
variable [CommRing R]
12+
13+
Introduction "Addition and multiplication are related via distributivity."
14+
15+
/-- Multiplication distributes over addition on the left -/
16+
TheoremDoc left_distrib as "left_distrib" in "Ring"
17+
/-- Multiplication distributes over addition on the right -/
18+
TheoremDoc right_distrib as "right_distrib" in "Ring"
19+
20+
Statement ( a b : R ) : (a + b) * (a + b) = a * a + b * a + (a * b + b * b) := by
21+
rw [left_distrib]
22+
rw [right_distrib]
23+
rw [right_distrib]
24+
25+
Conclusion "We still need to think about 0 and 1 in rings."

‎Game/Levels/AxiomWorld/L05_Identities.lean‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
import Game.Metadata
2+
3+
World "AxiomWorld"
4+
Level 5
5+
6+
Title "Identities"
7+
8+
variable {R : Type}
9+
variable [CommRing R]
10+
11+
Introduction "Rings include a 0 and a 1 which are additive and multiplicative identities."
12+
13+
/-- 0 is an additive identity on the right -/
14+
TheoremDoc add_zero as "add_zero" in "Ring"
15+
/-- 0 is an additive identity on the left -/
16+
TheoremDoc zero_add as "zero_add" in "Ring"
17+
/-- 1 is an multiplicative identity on the right -/
18+
TheoremDoc mul_one as "mul_one" in "Ring"
19+
/-- 1 is an multiplicative identity on the left -/
20+
TheoremDoc one_mul as "one_mul" in "Ring"
21+
22+
Statement (a : R) : (1 + 1) * a = a + a := by
23+
rw [right_distrib]
24+
rw [one_mul]
25+
26+
Conclusion "We will have to learn how to combine more axioms to prove more interesting statements."

‎Game/Levels/AxiomWorld/L06_Inverses.lean‎

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,25 @@
1+
import Game.Metadata
2+
3+
World "AxiomWorld"
4+
Level 6
5+
6+
Title "Inverses"
7+
8+
variable {R : Type}
9+
variable [CommRing R]
10+
11+
Introduction "Every element of a ring has an additive inverse."
12+
13+
theorem exist_add_inv (a : R) : (∃ (b : R), a + b = 0) := by
14+
use -a
15+
exact add_right_neg a
16+
17+
NewTactic rw
18+
19+
/-- Every element has an additive inverse -/
20+
TheoremDoc exist_add_inv as "exist_add_inv" in "Ring"
21+
22+
Statement (a : R) : ∃ b, (a + a) + b = 0 := by
23+
exact exist_add_inv (a+a)
24+
25+
Conclusion "We will have to learn how to combine more axioms to prove more interesting statements."

‎Game/Levels/DemoWorld.lean‎

Lines changed: 0 additions & 8 deletions
This file was deleted.

0 commit comments

Comments
 (0)