bump to v4.6.0

Game/Levels/Addition/L03add_comm.lean

@@ -30,6 +30,6 @@ Statement add_comm (a b : ℕ) : a + b = b + a := by
     rfl
 
 -- Adding this instance to make `ac_rfl` work.
-instance : Lean.IsCommutative (α := ℕ) (· + ·) := ⟨add_comm⟩
+instance : Std.Commutative (α := ℕ) (· + ·) := ⟨add_comm⟩
 
 TheoremTab "+"

Game/Levels/Addition/L04add_assoc.lean

@@ -43,7 +43,7 @@ Statement add_assoc (a b c : ℕ) : a + b + c = a + (b + c) := by
     rfl
 
 -- Adding this instance to make `ac_rfl` work.
-instance : Lean.IsAssociative (α := ℕ) (· + ·) := ⟨add_assoc⟩
+instance : Std.Associative (α := ℕ) (· + ·) := ⟨add_assoc⟩
 
 TheoremTab "+"
 

Game/Tactic/Cases.lean

@@ -31,16 +31,14 @@ Usage: `cases n with d` if `n : ℕ`; `cases h with h1 h2` if `h : P ∨ Q`; `ca
 -/
 elab (name := cases) "cases " tgts:(Parser.Tactic.casesTarget,+) usingArg:((" using " ident)?)
     withArg:((" with" (ppSpace colGt binderIdent)+)?) : tactic => do
-  let targets ← elabCasesTargets tgts.1.getSepArgs
+  let (targets, toTag) ← elabCasesTargets tgts.1.getSepArgs
   let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
   g.withContext do
     let elimInfo ← getElimNameInfo usingArg targets (induction := false)
 
-    -- Edit: If `elimInfo.name` is `MyNat.casesOn` we want to use `MyNat.casesOn'` instead.
-    -- TODO: This seems extremely hacky. Especially that we need to get the `elimInfo` twice.
-    -- Please improve this.
-    let elimInfo ← match elimInfo.name with
-    | `MyNat.casesOn =>
+    -- Edit: If `MyNat.casesOn` is used, we want to use `MyNat.casesOn` instead.
+    let elimInfo ← match elimInfo.elimExpr.getAppFn.constName? with
+    | some `MyNat.casesOn =>
       let modifiedUsingArgs : TSyntax Name.anonymous := ⟨
         match usingArg.raw with
         | .node info kind #[] =>
@@ -62,7 +60,9 @@ elab (name := cases) "cases " tgts:(Parser.Tactic.casesTarget,+) usingArg:((" us
       ElimApp.setMotiveArg g motive.mvarId! targetsNew
       g.assign result.elimApp
       let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
-         (numEqs := targets.size) (toClear := targetsNew)
+         (numEqs := targets.size) (toClear := targetsNew) (toTag := toTag)
       setGoals <| subgoals.toList ++ gs
 
+
+
 end MyNat

Game/Tactic/Induction.lean

@@ -17,6 +17,10 @@ to support the lean3-style `with` keyword.
 This is mainly copied and modified from the mathlib-tactic `induction'`.
 -/
 
+/--
+Custom induction principial for the tactics `induction`.
+Used to show `0` instead of `MyNat.zero` in the base case.
+-/
 def rec' {P : ℕ → Prop} (zero : P 0)
     (succ : (n : ℕ) → (n_ih : P n) → P (succ n)) (t : ℕ) : P t := by
   induction t with
@@ -44,15 +48,14 @@ elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.casesTarget,+)
     usingArg:((" using " ident)?)
     withArg:((" with" (ppSpace colGt binderIdent)+)?)
     genArg:((" generalizing" (ppSpace colGt ident)+)?) : tactic => do
-  let targets ← elabCasesTargets tgts.1.getSepArgs
+  let (targets, toTag) ← elabCasesTargets tgts.1.getSepArgs
   let g :: gs ← getUnsolvedGoals | throwNoGoalsToBeSolved
   g.withContext do
     let elimInfo ← getElimNameInfo usingArg targets (induction := true)
-    -- Edit: If `elimInfo.name` is `MyNat.rec` we want to use `MyNat.rec'` instead.
-    -- TODO: This seems extremely hacky. Especially that we need to get the `elimInfo` twice.
-    -- Please improve this.
-    let elimInfo ← match elimInfo.name with
-    | `MyNat.rec =>
+
+    -- Edit: If `MyNat.rec` is used, we want to use `MyNat.rec'` instead.
+    let elimInfo ← match elimInfo.elimExpr.getAppFn.constName? with
+    | some `MyNat.rec =>
       let modifiedUsingArgs : TSyntax Name.anonymous := ⟨
         match usingArg.raw with
         | .node info kind #[] =>
@@ -72,11 +75,11 @@ elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.casesTarget,+)
       let mut s ← getFVarSetToGeneralize targets forbidden
       for v in genArgs do
         if forbidden.contains v then
-          throwError ("variable cannot be generalized " ++
-            "because target depends on it{indentExpr (mkFVar v)}")
+          throwError "variable cannot be generalized \
+            because target depends on it{indentExpr (mkFVar v)}"
         if s.contains v then
-          throwError ("unnecessary 'generalizing' argument, " ++
-            "variable '{mkFVar v}' is generalized automatically")
+          throwError "unnecessary 'generalizing' argument, \
+            variable '{mkFVar v}' is generalized automatically"
         s := s.insert v
       let (fvarIds, g) ← g.revert (← sortFVarIds s.toArray)
       g.withContext do
@@ -85,5 +88,5 @@ elab (name := MyNat.induction) "induction " tgts:(Parser.Tactic.casesTarget,+)
         ElimApp.setMotiveArg g elimArgs[elimInfo.motivePos]!.mvarId! targetFVarIds
         g.assign result.elimApp
         let subgoals ← ElimApp.evalNames elimInfo result.alts withArg
-          (numGeneralized := fvarIds.size) (toClear := targetFVarIds)
+          (generalized := fvarIds) (toClear := targetFVarIds) (toTag := toTag)
         setGoals <| (subgoals ++ result.others).toList ++ gs

lake-manifest.json

@@ -4,25 +4,34 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "08ec2584b1892869e3a5f4122b029989bcb4ca79",
+   "rev": "a7543d1a6934d52086971f510e482d743fe30cf3",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/hhu-adam/lean-i18n.git",
+   "type": "git",
+   "subDir": null,
+   "rev": "c5b84feffb28dbd5b1ac74b3bf63271296fabfa5",
+   "name": "i18n",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/lean4game.git",
    "type": "git",
    "subDir": "server",
-   "rev": "3b660c518505b8f677224e3e36d1940d20ccb4bc",
+   "rev": "68f84a3426684914f834342854bf4963ba2d8d57",
    "name": "GameServer",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "1c88406514a636d241903e2e288d21dc6d861e01",
+   "rev": "fd760831487e6835944e7eeed505522c9dd47563",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,19 +40,19 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "cebd10ba6d22457e364ba03320cfd9fc7511e520",
+   "rev": "c51fa8ea4de8b203f64929cba19d139e555f9f6b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.6.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "8dd18350791c85c0fc9adbd6254c94a81d260d35",
+   "rev": "16cae05860b208925f54e5581ec5fd264823440c",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.25",
+   "inputRev": "v0.0.29",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +67,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "8079d2d1d0e073bde42eab159c24f4c2d0d3a871",
+   "rev": "64d082eeaad1a8e6bbb7c23b7a16b85a1715a02f",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,10 +76,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "feec58a7ee9185f92abddcf7631643b53181a7d3",
+   "rev": "7ca43cbd6aa34058a1afad8e47190af3ec1f9bdb",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.5.0",
+   "inputRev": "v4.6.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "Game",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.5.0
+leanprover/lean4:v4.6.0

test/cases.lean

@@ -5,17 +5,36 @@ namespace MyNat
 
 example (P Q : Prop) (h : P ∨ Q) : False := by
   cases h with hp hq
-  · sorry -- hp : P
-  · sorry -- hq : Q
+  · /-
+    case inl
+    P Q : Prop
+    hp : P
+    ⊢ False
+    -/
+    sorry
+  · /-
+    case inr
+    P Q : Prop
+    hq : Q
+    ⊢ False
+    -/
+    sorry
 
 example (a b : ℕ) (h : a ≤ b) : False := by
   cases h with c hc
-  -- hc: b = a + c
+  /-
+  case intro
+  a b c : ℕ
+  hc : b = a + c
+  ⊢ False
+  -/
   sorry
 
--- not working yet
 example (a : ℕ) : a = a := by
   cases a with d
-  -- get MyNat.zero because we used rec not rec' :-(
-  · sorry
+  · /-
+    case zero
+    ⊢ 0 = 0
+    -/
+    sorry
   · sorry

test/induction.lean

@@ -5,24 +5,29 @@ import Mathlib.Tactic
 
 example (a b : ℕ) : a + b = a → b = 0 := by
   induction b with d hd
-  -- looks great
-  -- base case
-  /-
-  a : ℕ
-  ⊢ a + 0 = a → 0 = 0
-  -/
-  sorry; sorry
+  · /-
+    a : ℕ
+    ⊢ a + 0 = a → 0 = 0
+    -/
+    sorry
+  · sorry
 
 example (a b c : ℕ) (g : c = 0) : a + b = a → b = 0 := by
   intro h -- h : a + b = a
   induction b with d hd generalizing g
-  -- aargh
-  -- base case
-  /-
-  a b: ℕ
-  h✝ : a + b = a
-  h : a + 0 = a
-  ⊢ 0 = 0
-  -/
-  -- Why does b still exist in the base case? And why does h✝ exist at all?
-  sorry; sorry
+  · /-
+    a b: ℕ
+    h✝ : a + b = a
+    h : a + 0 = a
+    ⊢ 0 = 0
+    -/
+    sorry
+  · /-
+    case succ
+    a c d : ℕ
+    hd : c = 0 → a + d = a → d = 0
+    g : c = 0
+    h : a + MyNat.succ d = a
+    ⊢ MyNat.succ d = 0
+    -/
+    sorry