Merge branch 'main' into LessOrEqual

Game.lean

@@ -51,9 +51,9 @@ links, and ways to interact with the Lean community.
 "
 
 Info "
-##### Game version: 4.1
+*Game version: 4.1*
 
-#### Recent changes: rewrite of tutorial, addition, multiplication and power world.
+*Recent changes: rewrite of tutorial, addition, multiplication and power world.*
 
 ## Progress saving
 
@@ -103,4 +103,9 @@ Dependency Addition → Multiplication → Power
 --Dependency Multiplication → AdvMultiplication
 --Dependency AdvAddition → EvenOdd → Inequality → StrongInduction
 Dependency Addition → Implication → AdvAddition → LessOrEqual
+-- The game automatically computes connections between worlds based on introduced
+-- tactics and theorems, but for example it cannot detect introduced definitions
+
+-- Dependency Implication → Power -- `Power` uses `≠` which is introduced in `Implication`
+
 MakeGame

Game/Levels/AdvAddition/L02add_right_cancel.lean

@@ -13,8 +13,6 @@ LemmaDoc MyNat.add_right_cancel as "add_right_cancel" in "Add" "
 `add_right_cancel a b n` is the theorem that $a+n=b+n \\implies a=b.$
 "
 
-NewLemma MyNat.add_right_cancel
-
 Introduction
 "`add_right_cancel a b n` is the theorem that $a+n=b+n\\implies a=b$.
 "

Game/Levels/AdvAddition/L03add_left_cancel.lean

@@ -13,8 +13,6 @@ LemmaDoc MyNat.add_left_cancel as "add_left_cancel" in "Add" "
 `add_left_cancel a b n` is the theorem that $n+a=n+b \\implies a=b.$
 "
 
-NewLemma MyNat.add_left_cancel
-
 Introduction
 "`add_left_cancel a b n` is the theorem that $n+a=n+b\\implies a=b$.
 You can prove it by induction on `n` or you can deduce it from `add_right_cancel`.

Game/Levels/AdvAddition/L04add_left_eq_self.lean

@@ -13,8 +13,6 @@ LemmaDoc MyNat.add_left_eq_self as "add_left_eq_self" in "Add" "
 `add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$
 "
 
-NewLemma MyNat.add_left_eq_self
-
 Introduction
 "
 `add_left_eq_self x y` is the theorem that $x + y = y\\implies x=0.$

Game/Levels/AdvAddition/L05add_right_eq_self.lean

@@ -13,8 +13,6 @@ LemmaDoc MyNat.add_right_eq_self as "add_right_eq_self" in "Add" "
 `add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
 "
 
-NewLemma MyNat.add_right_eq_self
-
 Introduction
 "`add_right_eq_self x y` is the theorem that $x + y = x\\implies y=0.$
 Two ways to do it spring to mind; I'll mention them when you've solved it.

Game/Levels/Implication/L04succ_inj.lean

@@ -57,8 +57,9 @@ Statement (x : ℕ) (h : x + 1 = 4) : x = 3 := by
   rw [four_eq_succ_three] at h
   Hint "Now rewrite `succ_eq_add_one` backwards at `h`
   to get the right hand side."
-  Hint (hidden := true) "`rw [← succ_eq_add_one] at h`. Look at the
-  docs for `rw` for an explanation. Type `←` with `\\l`."
+  Hint "You can put a `←` in front of any theorem provided to `rw` to rewrite
+  the other way around. Look at the docs for `rw` for an explanation. Type `←` with `\\l`."
+  Hint (hidden := true) "Concretely: `rw [← succ_eq_add_one] at h`."
   rw [←succ_eq_add_one] at h
   Hint "Now let's `apply` our new theorem. Execute `apply succ_inj at h`
   to change `h` to a proof of `x = 3`."

Game/Levels/Implication/L06intro.lean

@@ -23,7 +23,7 @@ NewTactic intro
 
 
 Introduction
-"We have seen how to `apply` theorems and assumptions of
+"We have seen how to `apply` theorems and assumptions
 of the form `P → Q`. But what if our *goal* is of the form `P → Q`?
 To prove this goal, we need to know how to say \"let's assume `P` and deduce `Q`\"
 in Lean. We do this with the `intro` tactic.

Game/Levels/Implication/L07intro2.lean

@@ -26,8 +26,8 @@ Statement (x : ℕ) : x + 1 = y + 1 → x = y := by
 Conclusion "Here's a completely backwards proof:
 ```
 intro h
-repeat rw [succ_eq_add_one]
 apply succ_inj
+repeat rw [succ_eq_add_one]
 exact h
 ```
 "

Game/Levels/Implication/L09zero_ne_succ.lean

@@ -18,6 +18,8 @@ Here `False` is a generic false statement. This means that
 you can `apply zero_ne_succ at h` if `h` is a proof of `0 = succ n`.
 "
 
+NewLemma MyNat.zero_ne_succ
+
 Introduction "
 As warm-up for `2 + 2 ≠ 5` let's prove `0 ≠ 1`. To do this we need to
 introduce Peano's last axiom `zero_ne_succ n`, a proof that `0 ≠ succ n`.
@@ -28,8 +30,6 @@ LemmaDoc MyNat.zero_ne_one as "zero_ne_one" in "numerals" "
 `zero_ne_one` is a proof of `0 ≠ 1`.
 "
 
-NewLemma MyNat.zero_ne_succ MyNat.zero_ne_one
-
 /-- $0\neq1$. -/
 Statement zero_ne_one : (0 : ℕ) ≠ 1 := by
   Hint "Start with `intro h`."

Game/Levels/Tutorial/L02rw.lean

@@ -109,8 +109,6 @@ If you only want to change the 37th occurrence of `X`
 to `Y` then do `nth_rewrite 37 [h]`.
 "
 
-NewTactic rw
-
 TacticDoc «repeat» "
 ## Summary
 
@@ -126,8 +124,6 @@ into the goal
 `a = b`.
 "
 
-NewHiddenTactic «repeat»
-
 TacticDoc nth_rewrite "
 ## Summary
 
@@ -141,7 +137,8 @@ will change the goal to `2 + succ 1 = 4`. In contrast, `rw [two_eq_succ_one]`
 will change the goal to `succ 1 + succ 1 = 4`.
 "
 
-NewHiddenTactic nth_rewrite
+NewTactic rw
+NewHiddenTactic «repeat» nth_rewrite
 
 Introduction
 "

Game/Levels/Tutorial/L03two_eq_ss0.lean

@@ -22,7 +22,6 @@ defined via two rules:
 It is distinct from the Lean natural numbers `Nat`, which should hopefully
 never leak into the natural number game.*"
 
-NewDefinition MyNat
 
 LemmaDoc MyNat.one_eq_succ_zero as "one_eq_succ_zero" in "numerals"
 "`one_eq_succ_zero` is a proof of `1 = succ 0`."
@@ -36,6 +35,7 @@ LemmaDoc MyNat.three_eq_succ_two as "three_eq_succ_two" in "numerals"
 LemmaDoc MyNat.four_eq_succ_three as "four_eq_succ_three" in "numerals"
 "`four_eq_succ_three` is a proof of `4 = succ 3`."
 
+NewDefinition MyNat
 NewLemma MyNat.one_eq_succ_zero MyNat.two_eq_succ_one MyNat.three_eq_succ_two
   MyNat.four_eq_succ_three
 

Game/Levels/Tutorial/L05add_zero.lean

@@ -43,7 +43,6 @@ as \"one thing\", namely a proof of $\\forall n ∈ ℕ, n + 0 = n$.
 This is just another way of saying that it's a function which
 can eat any number n and will return a proof that `n + 0 = n`."
 
-NewLemma MyNat.add_zero
 
 TacticDoc «repeat» "
 ## Summary
@@ -60,7 +59,7 @@ into the goal
 `a = b`.
 "
 
-NewHiddenTactic «repeat»
+NewLemma MyNat.add_zero
 
 Introduction
 "

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"git":
    {"url": "https://github.com/EdAyers/ProofWidgets4",
     "subDir?": null,
-    "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229",
+    "rev": "65bba7286e2395f3163fd0277110578f19b8170f",
     "opts": {},
     "name": "proofwidgets",
-    "inputRev?": "v0.0.13",
+    "inputRev?": "v0.0.16",
     "inherited": true}},
   {"git":
    {"url": "https://github.com/mhuisi/lean4-cli.git",
@@ -20,10 +20,10 @@
   {"git":
    {"url": "https://github.com/leanprover-community/mathlib4",
     "subDir?": null,
-    "rev": "7d308680dc444730e84a86c72357ad9a7aea9c4b",
+    "rev": "f203f2e0caf1d9ea25b7f2e4b8c2afebd2c6967b",
     "opts": {},
     "name": "mathlib",
-    "inputRev?": "7d308680dc444730e84a86c72357ad9a7aea9c4b",
+    "inputRev?": "v4.1.0",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/gebner/quote4",
@@ -44,15 +44,15 @@
   {"git":
    {"url": "https://github.com/leanprover-community/lean4game.git",
     "subDir?": "server",
-    "rev": "6970f10e30f70ecede1042201e9bd1d838ad1934",
+    "rev": "cc4321ff3f7cbf43747114cd56197a1b2bb0c457",
     "opts": {},
     "name": "GameServer",
-    "inputRev?": "6970f10e30f70ecede1042201e9bd1d838ad1934",
+    "inputRev?": "main",
     "inherited": false}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "e8c27f7d90ee71470558efd1bc197fe55068c748",
+    "rev": "67855403d60daf181775fa1ec63b04e70bcc3921",
     "opts": {},
     "name": "std",
     "inputRev?": "main",

lakefile.lean

@@ -8,7 +8,7 @@ def LocalGameServer : Dependency := {
 
 def RemoteGameServer : Dependency := {
   name := `GameServer
-  src := Source.git "https://github.com/leanprover-community/lean4game.git" "6970f10e30f70ecede1042201e9bd1d838ad1934" "server"
+  src := Source.git "https://github.com/leanprover-community/lean4game.git" "main" "server"
 }
 
 /- Choose dependency depending on the environment variable NODE_ENV -/
@@ -19,25 +19,18 @@ open Lean in
   modifyEnv (fun env => Lake.packageDepAttr.ext.addEntry env gameServerName)
    : Elab.Command.CommandElabM Unit)
 
--- require mathlib from git
---   "https://github.com/leanprover-community/mathlib4" @ "88e129706828e01b7622d6635af1ca6667e25bac"
-
--- `Game` fix:
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4" @ "7d308680dc444730e84a86c72357ad9a7aea9c4b"
-
-
+  "https://github.com/leanprover-community/mathlib4" @ "v4.1.0"
 
+-- NOTE: We abuse the `trace.debug` option to toggle messages in VSCode on and
+-- off when calling `lake build`. Ideally there would be a better way using `logInfo` and
+-- an option like `lean4game.verbose`.
 package Game where
-  moreLeanArgs := #[
-    "-Dtactic.hygienic=false",
-    "-Dlinter.unusedVariables=false",
-    "--quiet"]
-  moreServerArgs := #[
-    "-Dtactic.hygienic=false",
-    "-Dlinter.unusedVariables=false",
-    "--quiet"]
-  weakLeanArgs := #["--quiet"]
+  moreLeanArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=false",
+    "-Dtrace.debug=false"]
+  moreServerArgs := #["-Dtactic.hygienic=false", "-Dlinter.unusedVariables.funArgs=true",
+    "-Dtrace.debug=true"]
+  weakLeanArgs := #[]
 
 @[default_target]
 lean_lib Game

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.0.0
+leanprover/lean4:v4.1.0