Strong induction / lt world first draft

.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: Fri Mar 14 17:06:47 2025\n"
+"POT-Creation-Date: Thu Mar 20 09:28:24 2025\n"
 "Last-Translator: \n"
 "Language-Team: none\n"
 "Language: en\n"
@@ -2801,8 +2801,7 @@ msgid "Now you need to figure out which number to `use`. See if you can take it
 msgstr ""
 
 #: Game.Levels.LessOrEqual.L04le_trans
-msgid "A passing mathematician remarks that with reflexivity and transitivity out of the way,\n"
-"you have proved that `≤` is a *preorder* on `ℕ`."
+msgid "A passing mathematician remarks that with reflexivity and transitivity out of the way, you have proved that `≤` is a *preorder* on `ℕ`."
 msgstr ""
 
 #: Game.Levels.LessOrEqual.L05le_zero
@@ -3095,6 +3094,356 @@ msgid "In this world we define `a ≤ b` and prove standard facts\n"
 "Click on \"Start\" to proceed."
 msgstr ""
 
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "Successor are equal iff originals are equal"
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "## Summary\n"
+"\n"
+"The `constructor` tactic can be used to split a compound goal into its \n"
+"parts.\n"
+"\n"
+"## Example\n"
+"If you have a goal of the form `p ↔ q`, and you execute\n"
+"`constructor`, then you will replace `p ↔ q` with two goals, first\n"
+"`p →  q` and then `q`→ p`.\n"
+"\n"
+"\n"
+"## Example\n"
+"If you have a goal of the form `p ∧ q`, and you execute\n"
+"`constructor`, then you will get replace `p ∧ q` with two goals,\n"
+"first `p` and then `q`."
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "In this level we introduce a tactic that will be useful\n"
+"in this world, the `constructor` tactic.  For two proposition `p` and\n"
+"`q`, `p ↔ q`, consists of two statements (1) the Modus Ponens: `p → q`\n"
+"and (2) the reversed Modus Ponens: `q → p`.  If you have a goal of the\n"
+"form `p ↔ q`, then the `constructor` tactic will split this goal into\n"
+"these two sub-goals.\n"
+"\n"
+"We practice using this tactic in this level."
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "`succ_eq_succ_iff a b` is a proof that `succ a = succ b ↔ a = b`.  In words,\n"
+"  equal numbers have equal successors and vice versa."
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "If `a b` are natural numbers, then `succ a = succ b ↔ a = b`"
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "The goal is an iff statement so use `constructor`."
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "The `succ_inj` theorem is useful here."
+msgstr ""
+
+#: Game.Levels.LessThan.L01_succ_eq_succ_iff
+msgid "The `constructor` tactic also works on goals of the form `P\n"
+"∧ Q`, for two propositions `P` and `Q`.\n"
+"\n"
+"Now you know how to construct an iff statement from two implications,\n"
+"in the next level how to use the `rw` tactic with `↔` statements."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "Practice with `rw`"
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "In this level, you will get practice using the `rw`\n"
+"tactic with iff statements.  Before this level, you used `rw` to\n"
+"substitute *equations* into the goal or into other expressions.  The `rw` tactic\n"
+"can be used to rewrite equivalent *propositions* into each other in the same way."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "Equal numbers have equal successors of successors and vice versa."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "To strip of one pair of `succ`'s, you can use `rw [succ_eq_succ_iff]`."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "Now strip off the next pair of `succ`'s."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "We have something of the form `p ↔ p`, which can be solved with `rfl`."
+msgstr ""
+
+#: Game.Levels.LessThan.L02_succ_succ_eq_succ_succ_iff
+msgid "A different proof\n"
+"```\n"
+"  rw [succ_eq_succ_iff]\n"
+"  exact (succ_eq_succ_iff a b)\n"
+"```"
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "lt_succ_self"
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "`a < b` is *notation* for `succ a ≤ b`, and `succ a ≤ b` in turn\n"
+"is *notation* for `∃ c : b = succ a + c`.  This mean that if you have\n"
+"a *goal* of the for `a < b`, you can make progress with the `use\n"
+"tactice`, and if you have a *hypothesis* (h : a < b) you can make\n"
+"progress with `cases h with c hc`."
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "In this level we define a new relation, `<`, on the\n"
+"natural numbers,  For `a b`, two natural number, we have\n"
+"`a < b` if (and only if) `succ a ≤ b`.\n"
+"\n"
+"Remember that that `succ a ≤\n"
+"b` is notation for \"there exists `c` such that `b = succ a +\n"
+"c`\".  As such, we can make progress on goals of the form `a < b` by\n"
+"`use`ing the number which is morally `b - succ a` (i.e. `use (b - succ\n"
+"a)`).\n"
+"\n"
+"Of course we haven't defined subtraction yet so deciphering which\n"
+"expression is morally equal to this difference will be your task.\n"
+"\n"
+"We start by showing every number is less than its sucessor."
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "`lt_succ_self a` is a proof that `a < succ a`"
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "If `a` is a natural number, then `a < succ a`"
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "Remember that `lhs < rhs` is defined as `succ lhs ≤ rhs`.  How\n"
+"would you show this for the cases when `lhs = a` and `rhs = succ\n"
+"a`?"
+msgstr ""
+
+#: Game.Levels.LessThan.L03_lt_succ_self
+msgid "Nice job.  In the next level you will show that the\n"
+"relations \"less than:`<`\"  and \"less than or equal:`≤`\" make linguistic\n"
+"as well as mathematical sense."
+msgstr ""
+
+#: Game.Levels.LessThan.L04_le_iff_lt_or_eq
+msgid "le_iff_lt_or_eq"
+msgstr ""
+
+#: Game.Levels.LessThan.L04_le_iff_lt_or_eq
+msgid "`le_iff_lt_or_eq a b `is a proof that `a ≤ b` iff `a < b' or a = b'."
+msgstr ""
+
+#: Game.Levels.LessThan.L04_le_iff_lt_or_eq
+msgid "This level shows that `a ≤ b ↔ (a < b) ∨ (a = b)`.  In\n"
+"spoken form (\"`a` is less than or equal to `b` iff `a` is less than or\n"
+"equal to `b`\"); this is a tautology, so it is a worthwhile exercise to\n"
+"check that our mathematical definitions also make linguistic sense."
+msgstr ""
+
+#: Game.Levels.LessThan.L04_le_iff_lt_or_eq
+msgid "If `a` and `b` are  natural numbers, then `a ≤ b` iff (`a < b` or `a = b`)."
+msgstr ""
+
+#: Game.Levels.LessThan.L04_le_iff_lt_or_eq
+msgid "Nice job. In the `≤`-world you showed that for all natural\n"
+"numbers a, we have `0 ≤ a`. In the next level, you will show that zero\n"
+"is not greater than any natural number."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "not_lt_zero"
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "`not_lt_zero a`is a proof that `¬(a < 0)`."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "In this level, we show that there is no natural number less than zero."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "If `a` is a natural number the ¬(a < 0)."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "Use `cases` to split up `«{h0}»`."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "One of main tools is the fact that zero is not the successor\n"
+"of a natural number, (`zero_ne_succ` or `succ_ne_zero`). Try to use\n"
+"one of those here."
+msgstr ""
+
+#: Game.Levels.LessThan.L05_not_lt_zero
+msgid "Nice job.  In the next level you will show that our\n"
+"definition of `<`, is equivalent to Lean's default way of defining it.\n"
+"Click \"Next\" to continue."
+msgstr ""
+
+#: Game.Levels.LessThan.L06_lt_iff_le_not_le
+msgid "lt_iff_le_not_le"
+msgstr ""
+
+#: Game.Levels.LessThan.L06_lt_iff_le_not_le
+msgid "`lt_iff_le_not_le a b` is a proof that  `a < b ↔ (a ≤ b) ∧ ¬(b ≤ a)`."
+msgstr ""
+
+#: Game.Levels.LessThan.L06_lt_iff_le_not_le
+msgid "There are many equivalent ways we could have defined the\n"
+"`<` relation.  The one that we chose allows the proofs in this world\n"
+"to be simpler, but isn't the default way that Lean would have defined\n"
+"it.  In this level, we show that our definition is equivalent to\n"
+"Lean's default definition of `<`."
+msgstr ""
+
+#: Game.Levels.LessThan.L06_lt_iff_le_not_le
+msgid "If `a` and `b` are natural numbers, then `a < b` iff `a ≤ b` and `¬(b ≤ a)`."
+msgstr ""
+
+#: Game.Levels.LessThan.L06_lt_iff_le_not_le
+msgid "The mathematician who passed by after the transitiviy\n"
+"level of `≤` world, remarks that you have shown that the natural\n"
+"numbers equipped with our choice for the definition of `<`, is a *preorder*,\n"
+"a *Partial order* and a *Linear order*."
+msgstr ""
+
+#: Game.Levels.LessThan.L07_lt_succ_iff_le
+msgid "lt_succ_iff_le"
+msgstr ""
+
+#: Game.Levels.LessThan.L07_lt_succ_iff_le
+msgid "`lt_succ_iff_le m n `is a proof that `m < succ n ↔ m ≤ n`"
+msgstr ""
+
+#: Game.Levels.LessThan.L07_lt_succ_iff_le
+msgid "You are building up to fight the final boss of this\n"
+"world, the strong induction principle.  Your task in this level is to\n"
+"show that `m < succ n ↔ m ≤ n`.  The proof is straightforward so you\n"
+"probably don't need any hints."
+msgstr ""
+
+#: Game.Levels.LessThan.L07_lt_succ_iff_le
+msgid "If `m` and `n` are natural numbers, then `lt_succ_iff_le m n` is a proof\n"
+"that `m < succ n ↔ m ≤ n`."
+msgstr ""
+
+#: Game.Levels.LessThan.L07_lt_succ_iff_le
+msgid "Nice job, you are almost to the final boss.  Click\n"
+"\"Next\" to continue."
+msgstr ""
+
+#: Game.Levels.LessThan.L08_not_lt_and_lt_succ
+msgid "not_lt_and_lt_succ"
+msgstr ""
+
+#: Game.Levels.LessThan.L08_not_lt_and_lt_succ
+msgid "`not_lt_and_lt_succ m n` is a proof that no number is both stricly\n"
+"greater than another number and strictly less than the other\n"
+"number's successor."
+msgstr ""
+
+#: Game.Levels.LessThan.L08_not_lt_and_lt_succ
+msgid "You don't need this level to fight the final boss, but\n"
+"it is good training.  This level shows that there is no natural number\n"
+"that is both greater than a number `n` and less than `n + 1`.  This is\n"
+"not true for the rational numbers nor the real numbers.  It is true\n"
+"for integers, though.  Speaking loosely, the natural numbers and the\n"
+"integers are *chunky*."
+msgstr ""
+
+#: Game.Levels.LessThan.L08_not_lt_and_lt_succ
+msgid "If `m` and `n` are natural numbers, then `¬( (n < m) ∧ (m < succ n))`."
+msgstr ""
+
+#: Game.Levels.LessThan.L08_not_lt_and_lt_succ
+msgid "You are now ready to fight the final boss.  Click \"Next\"\n"
+"to face it."
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "Strong Induction Principle"
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "'strong_induction P h` is a proof that `∀ z : ℕ, P z`."
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "Welcome to the boss level.  Your task is to prove a\n"
+"variant of basic induction called *strong induction*.  Remember that\n"
+"in basic induction, you prove that a predicate `P` is true for all\n"
+"natural numbers `n`.  You do this by showing `P 0`: a proof of the predicate\n"
+"for `k = 0`, and then by showing that for all `k`, `P k → P (succ k)`.\n"
+"\n"
+"The strong induction show show that that a predicate `P` is true for\n"
+"all natural numbers `n`.  It does this with a weaker \"inductive\n"
+"hypothesis\". For `n` the strong inductive hypotheses is a proof that\n"
+"for all `m < n, P m` implies `P n`.\n"
+"\n"
+"Your task in this level, and the boss of this world, is to use the\n"
+"basic induction to prove the principle of strong induction.\n"
+"\n"
+"As an exercise, try to do this on paper before doing it\n"
+"on the computer.  The idea of the proof isn't esoteric, but it is easy\n"
+"to convince yourself that an invalid proof is actually\n"
+"valid."
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "As a warm up, try to prove the statment for `z = 0`, `z = 1`,\n"
+"and `z = 2` first.  This should give you an idea that you need to\n"
+"introduce an auxillary statement.  There is a hidden hint if you are\n"
+"still stuck."
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "You are likely in a dead end.  The inductive hypothesis gives\n"
+"you `P «{k}»`, but to use `«{h0}»`, you need `∀ m < succ «{k}», P m`, something\n"
+"you don't have.  You may want to restart from the beginning."
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "Finish the following statement\n"
+"`have h1 : ∀ a: ℕ, ∀ y : ℕ, y < a → P y := by`"
+msgstr ""
+
+#: Game.Levels.LessThan.L09_strong_induction
+msgid "Congratulations.  You have finished the `<` level.  Click\n"
+"\"Leave World\" to go back to the overworld."
+msgstr ""
+
+#: Game.Levels.LessThan
+msgid "< World"
+msgstr ""
+
+#: Game.Levels.LessThan
+msgid "In this world we define `a < b` and prove standard\n"
+"facts about it.  The final boss of this level is to prove the strong\n"
+"induction principle.\n"
+"\n"
+"In this level we will define the proposition `a < b` as `succ a ≤ b`.\n"
+"We will define \"less than\" in terms of \"less than or equal\".  At\n"
+"first glance, this may seem like a circular definition but it is not.\n"
+"\n"
+"Before we prove this and other facts about \"less than\", we need to\n"
+"introduce two new tactics.\n"
+"\n"
+"Click on \"Start\" to proceed."
+msgstr ""
+
 #: Game.Levels.AdvMultiplication.L01mul_le_mul_right
 msgid "mul_le_mul_right"
 msgstr ""

Game.lean

@@ -11,6 +11,7 @@ import Game.Levels.Power
 import Game.Levels.Implication
 import Game.Levels.AdvAddition
 import Game.Levels.LessOrEqual
+import Game.Levels.LessThan
 import Game.Levels.AdvMultiplication
 --import Game.Levels.EvenOdd
 --import Game.Levels.Prime

Game/Levels/Addition/L04add_assoc.lean

@@ -1,6 +1,5 @@
 import Game.Levels.Addition.L03add_comm
 
-
 World "Addition"
 Level 4
 Title "add_assoc (associativity of addition)"

Game/Levels/LessOrEqual/L04le_trans.lean

@@ -43,6 +43,5 @@ Statement le_trans (x y z : ℕ) (hxy : x ≤ y) (hyz : y ≤ z) : x ≤ z := by
 TheoremTab "≤"
 
 Conclusion "
-A passing mathematician remarks that with reflexivity and transitivity out of the way,
-you have proved that `≤` is a *preorder* on `ℕ`.
+A passing mathematician remarks that with reflexivity and transitivity out of the way, you have proved that `≤` is a *preorder* on `ℕ`.
 "