More levels

Author: kisonecat

.i18n/en/Game.pot

@@ -1,7 +1,7 @@
 msgid ""
 msgstr "Project-Id-Version: Game v4.7.0\n"
 "Report-Msgid-Bugs-To: \n"
-"POT-Creation-Date: Wed Jun 18 12:03:04 2025\n"
+"POT-Creation-Date: Wed Jun 18 21:45:45 2025\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -131,7 +131,7 @@ msgid "Every element of a ring has an additive inverse."
 msgstr ""
 
 #: Game.Levels.AxiomWorld.L06_Inverses
-msgid "exact provides a term that completes the goal"
+msgid "close a goal by matching it against the conclusion of a given expression"
 msgstr ""
 
 #: Game.Levels.AxiomWorld.L06_Inverses
@@ -150,6 +150,54 @@ msgstr ""
 msgid "We introduce the ring axioms."
 msgstr ""
 
+#: Game.Levels.RingWorld.L01
+msgid "Implications"
+msgstr ""
+
+#: Game.Levels.RingWorld.L01
+msgid "We learn how to use the intro tactic."
+msgstr ""
+
+#: Game.Levels.RingWorld.L01
+msgid ""
+msgstr ""
+
+#: Game.Levels.RingWorld.L01
+msgid "We can use intro to prove conditional statements."
+msgstr ""
+
+#: Game.Levels.RingWorld.L02
+msgid "Substitution"
+msgstr ""
+
+#: Game.Levels.RingWorld.L02
+msgid "One of our rules of logic is substitution."
+msgstr ""
+
+#: Game.Levels.RingWorld.L02
+msgid ""
+msgstr ""
+
+#: Game.Levels.RingWorld.L03
+msgid "add_right_cancel"
+msgstr ""
+
+#: Game.Levels.RingWorld.L03
+msgid "Using the axioms, we prove that cancellation is possible."
+msgstr ""
+
+#: Game.Levels.RingWorld.L03
+msgid "You have just proved `add_right_cancel`"
+msgstr ""
+
+#: Game.Levels.RingWorld
+msgid "Ring World"
+msgstr ""
+
+#: Game.Levels.RingWorld
+msgid "We use the ring axioms to prove various facts about rings."
+msgstr ""
+
 #: Game
 msgid "Ross Game"
 msgstr ""

Game.lean

@@ -1,4 +1,5 @@
 import Game.Levels.AxiomWorld
+import Game.Levels.RingWorld
 
 -- Here's what we'll put on the title screen
 Title "Ross Game"

Game/Levels/AxiomWorld/L06_Inverses.lean

@@ -10,21 +10,15 @@ variable [CommRing R]
 
 Introduction "Every element of a ring has an additive inverse."
 
-theorem exist_add_inv (a : R) : (∃ (b : R), a + b = 0) := by
-  use -a
-  exact add_right_neg a
-
-/-- exact provides a term that completes the goal -/
-TacticDoc exact
-
-NewTactic exact
+/-- close a goal by matching it against the conclusion of a given expression -/
+TacticDoc apply
+NewTactic apply
 
 /-- Every element has an additive inverse -/
 TheoremDoc exist_add_inv as "exist_add_inv" in "Ring"
-
 NewTheorem exist_add_inv
 
 Statement (a : R) : ∃ b, (a + a) + b = 0 := by
-  exact exist_add_inv (a+a)
+  apply exist_add_inv
 
 Conclusion "We will have to learn how to combine more axioms to prove more interesting statements."

Game/Levels/RingWorld.lean

@@ -0,0 +1,11 @@
+import Game.Levels.RingWorld.L01
+import Game.Levels.RingWorld.L02
+import Game.Levels.RingWorld.L03
+import Game.Levels.RingWorld.L04
+
+World "RingWorld"
+Title "Ring World"
+
+Introduction "
+We use the ring axioms to prove various facts about rings.
+"

Game/Levels/RingWorld/L01.lean

@@ -0,0 +1,21 @@
+import Game.Metadata
+
+World "RingWorld"
+Level 1
+
+Title "Implications"
+
+Introduction "We learn how to use the intro tactic."
+
+variable {R : Type}
+variable [CommRing R]
+
+TacticDoc intro
+NewTactic intro
+
+Statement ( x y : R ) : x = y + y → x + x = y + y + y + y := by
+  intro h
+  rw [h]
+  rw [←add_assoc]
+
+Conclusion "We can use intro to prove conditional statements."

Game/Levels/RingWorld/L02.lean

@@ -0,0 +1,20 @@
+import Game.Metadata
+
+World "RingWorld"
+Level 2
+
+Title "Substitution"
+
+Introduction "One of our rules of logic is substitution."
+
+variable {R : Type}
+variable [CommRing R]
+
+NewTactic rfl
+
+Statement ( a b b' : R ) : b = b' → a + b = a + b' := by
+  intro h
+  have : a + b = a + b := by rfl
+  rw [h]
+
+Conclusion ""

Game/Levels/RingWorld/L03.lean

@@ -0,0 +1,27 @@
+import Game.Metadata
+
+World "RingWorld"
+Level 3
+
+Title "add_right_cancel"
+
+Introduction "Using the axioms, we prove that cancellation is possible."
+
+variable {R : Type}
+variable [CommRing R]
+
+NewTactic rcases congr «have»
+
+Statement ( a b b' : R ) : b + a = b' + a → b = b' := by
+  intro h
+  rcases exist_add_inv a
+  have : b + (a + w) = b' + (a + w) := by
+    rw [←add_assoc]
+    rw [←add_assoc]
+    congr
+  rw [h_1] at this
+  rw [add_zero] at this
+  rw [add_zero] at this
+  apply this
+
+Conclusion "You have just proved `add_right_cancel`"

Game/Levels/RingWorld/L04.lean

@@ -0,0 +1,25 @@
+import Game.Metadata
+
+World "RingWorld"
+Level 4
+
+Title "zero times anything"
+
+Introduction "Using the axioms, we prove zero times anything vanishes."
+
+variable {R : Type}
+variable [CommRing R]
+
+NewTheorem add_left_cancel add_right_cancel
+
+NewTactic swap exact
+
+Statement ( a : R ) : 0 * a = 0 := by
+  apply add_left_cancel
+  swap
+  exact (0 * a)
+  rw [add_zero]
+  rw [←right_distrib]
+  rw [add_zero]
+
+Conclusion "You have just proved `zero_mul`"

Game/Metadata.lean

@@ -6,8 +6,6 @@ import Mathlib.Algebra.Ring.Defs
 variable {R : Type}
 variable [CommRing R]
 
-namespace Mathlib.Algebra.Ring
-
 theorem exist_add_inv (a : R) : (∃ (b : R), a + b = 0) := by
   use -a
   exact add_right_neg a