From 381a729f3e1d9307b047bd42cfa24dba3261b42f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Thu, 29 Feb 2024 17:19:01 +0100 Subject: [PATCH] bump to v4.6.0 --- Game/Levels/Addition/L03add_comm.lean | 2 +- Game/Levels/Addition/L04add_assoc.lean | 2 +- Game/Tactic/ACRfl.lean | 16 ----------- Game/Tactic/Cases.lean | 14 ++++----- Game/Tactic/Induction.lean | 25 +++++++++-------- Game/Tactic/cases_test.lean | 20 ------------- lake-manifest.json | 33 ++++++++++++++-------- lean-toolchain | 2 +- test/cases.lean | 31 ++++++++++++++++---- test/induction.lean | 39 +++++++++++++++----------- 10 files changed, 92 insertions(+), 92 deletions(-) delete mode 100644 Game/Tactic/ACRfl.lean delete mode 100644 Game/Tactic/cases_test.lean diff --git a/Game/Levels/Addition/L03add_comm.lean b/Game/Levels/Addition/L03add_comm.lean index c1122de..43e86ca 100644 --- a/Game/Levels/Addition/L03add_comm.lean +++ b/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 "+" diff --git a/Game/Levels/Addition/L04add_assoc.lean b/Game/Levels/Addition/L04add_assoc.lean index 027e31b..af1c233 100644 --- a/Game/Levels/Addition/L04add_assoc.lean +++ b/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 "+" diff --git a/Game/Tactic/ACRfl.lean b/Game/Tactic/ACRfl.lean deleted file mode 100644 index 88f8e45..0000000 --- a/Game/Tactic/ACRfl.lean +++ /dev/null @@ -1,16 +0,0 @@ - -import Lean - --- Note: to get `ac_rfl` working (which is in core), we just --- need the two instances below in the files where --- `add_assoc` and `add_comm` are proven. --- This file is only for demonstration purpose. - -import Game.Levels.Addition.Level_2 -- defines `MyNat.add_assoc` -import Game.Levels.Addition.Level_4 -- defines `MyNat.add_comm` - -instance : Lean.IsAssociative (α := ℕ) (·+·) := ⟨MyNat.add_assoc⟩ -instance : Lean.IsCommutative (α := ℕ) (·+·) := ⟨MyNat.add_comm⟩ - -example (a b c : ℕ) : c + (b + a) = (a + b) + c := by - ac_rfl diff --git a/Game/Tactic/Cases.lean b/Game/Tactic/Cases.lean index ebd8c0e..a254183 100644 --- a/Game/Tactic/Cases.lean +++ b/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 diff --git a/Game/Tactic/Induction.lean b/Game/Tactic/Induction.lean index 716eb16..49edba0 100644 --- a/Game/Tactic/Induction.lean +++ b/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 diff --git a/Game/Tactic/cases_test.lean b/Game/Tactic/cases_test.lean deleted file mode 100644 index 1314632..0000000 --- a/Game/Tactic/cases_test.lean +++ /dev/null @@ -1,20 +0,0 @@ -import Game.Levels.LessOrEqual - -namespace MyNat - -example (P Q : Prop) (h : P ∨ Q) : False := by - cases h with hp hq - · sorry -- hp : P - · sorry -- hq : Q - -example (a b : ℕ) (h : a ≤ b) : False := by - cases h with c hc - -- hc: b = a + c - sorry - --- not working yet -example (a : ℕ) : a = a := by - cases a with d - -- get MyNat.zero because we used rec not rec' :-( - · sorry - · sorry diff --git a/lake-manifest.json b/lake-manifest.json index 6b40954..dde70c6 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index bd59abf..5026204 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.5.0 +leanprover/lean4:v4.6.0 diff --git a/test/cases.lean b/test/cases.lean index 7aab530..6ed3827 100644 --- a/test/cases.lean +++ b/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 diff --git a/test/induction.lean b/test/induction.lean index ec3c8f0..77d1df6 100644 --- a/test/induction.lean +++ b/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