From 836f8f6078da68e870c12a73f1863ec52144b1b0 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 4 Aug 2023 17:14:49 +0200 Subject: [PATCH] import Mathlib.Tactic everywhere --- Game/Levels/AdvMultiplication/Level_3.lean | 4 ++-- Game/Levels/Inequality/Level_1.lean | 8 +++++--- Game/Levels/Tutorial/Level_4.lean | 6 +++++- Game/Metadata.lean | 8 +++++--- Game/MyNat/Definition.lean | 2 +- Game/Tactic/Induction.lean | 7 ++++++- Game/Tactic/Rfl.lean | 2 +- Game/Tactic/Rw.lean | 3 ++- lake-manifest.json | 20 +++++++++++++------- lakefile.lean | 8 +++++++- lean-toolchain | 2 +- 11 files changed, 48 insertions(+), 22 deletions(-) diff --git a/Game/Levels/AdvMultiplication/Level_3.lean b/Game/Levels/AdvMultiplication/Level_3.lean index 859dc02..7e6e30f 100644 --- a/Game/Levels/AdvMultiplication/Level_3.lean +++ b/Game/Levels/AdvMultiplication/Level_3.lean @@ -23,10 +23,10 @@ Statement intro hab rcases hab with hab | hab rw [hab] - rw [zero_mul] + rw [MyNat.zero_mul] rfl rw [hab] - rw [mul_zero] + rw [MyNat.mul_zero] rfl diff --git a/Game/Levels/Inequality/Level_1.lean b/Game/Levels/Inequality/Level_1.lean index a8cd434..f9295bf 100644 --- a/Game/Levels/Inequality/Level_1.lean +++ b/Game/Levels/Inequality/Level_1.lean @@ -33,7 +33,9 @@ If you have written `rw le_iff_exists_add` below, then just put two minus signs before it and comment it out. See that the proof still compiles. " -axiom add_comm (a b : ℕ) : a + b = b + a +#check le_iff_exists_add + +axiom TMP.add_comm (a b : ℕ) : a + b = b + a Statement --one_add_le_self "If $x$ is a natural number, then $x\\le 1+x$. @@ -43,7 +45,7 @@ Statement --one_add_le_self The goal below is to prove $x\\le 1+x$ for any natural number $x$. First let's turn the goal explicitly into an existence problem with `rw [le_iff_exists_add]`." - rw [le_iff_exists_add] + rw [MyNat.le_iff_exists_add] Hint " Clearly this statement now is true, and the proof is that $c=1$ will work (we also @@ -63,7 +65,7 @@ Statement --one_add_le_self -- which is a powerful AI which will solve any equality in algebra which can -- be proved using the standard rules of addition and multiplication. Now -- look at your proof. We're going to remove a line. - rw [add_comm] + rw [TMP.add_comm] rfl NewTactic use -- ring diff --git a/Game/Levels/Tutorial/Level_4.lean b/Game/Levels/Tutorial/Level_4.lean index 8a2ddeb..06d1634 100644 --- a/Game/Levels/Tutorial/Level_4.lean +++ b/Game/Levels/Tutorial/Level_4.lean @@ -41,6 +41,8 @@ If you ever see `… + succ …` in your goal, you should be able to use `rw [add_succ]` to make progress. " +attribute [simp] MyNat.add_zero + LemmaDoc MyNat.add_succ as "add_succ" in "Add" "One of the two axioms defining addition. It says `n + (succ m) = succ (n + m)`." @@ -58,13 +60,15 @@ Statement Hint (hidden := true) "Explicitely, type `rw [add_zero]`!" Branch simp? -- TODO - rw [add_zero] + rw [MyNat.add_zero] Hint (hidden := true) "Finally both sides are identical." rfl NewLemma MyNat.add_succ MyNat.add_zero NewDefinition Add +#check add_zero + Conclusion " You have finished tutorial world! If you're happy, let's move onto Addition World, diff --git a/Game/Metadata.lean b/Game/Metadata.lean index e633759..71b6066 100644 --- a/Game/Metadata.lean +++ b/Game/Metadata.lean @@ -5,12 +5,14 @@ import Game.MyNat.Definition import Game.Doc.Definitions import Game.Doc.Tactics +import Mathlib.Tactic + import Game.Tactic.Induction import Game.Tactic.Rfl import Game.Tactic.Rw -import Std.Tactic.RCases -import Game.Tactic.Have -import Game.Tactic.LeftRight +-- import Std.Tactic.RCases +-- import Game.Tactic.Have +-- import Game.Tactic.LeftRight -- TODO: Why does this not work here?? -- We do not want `simp` to be able to do anything unless we unlock it manually. diff --git a/Game/MyNat/Definition.lean b/Game/MyNat/Definition.lean index bd68ddf..1f75466 100644 --- a/Game/MyNat/Definition.lean +++ b/Game/MyNat/Definition.lean @@ -5,7 +5,7 @@ inductive MyNat where -- deriving BEq, DecidableEq, Inhabited @[inherit_doc] -notation "ℕ" => MyNat +notation (name := MyNatNotation) (priority := 1000000) "ℕ" => MyNat -- Note: as long as we do not import `Mathlib.Init.Data.Nat.Notation` this is fine. namespace MyNat diff --git a/Game/Tactic/Induction.lean b/Game/Tactic/Induction.lean index 19efd91..8380d59 100644 --- a/Game/Tactic/Induction.lean +++ b/Game/Tactic/Induction.lean @@ -1,7 +1,12 @@ -import Game.Tactic.LeanExprBasic import Lean.Elab.Tactic.Basic +import Lean.Elab.Tactic.Induction +import Std.Tactic.OpenPrivate +import Std.Data.List.Basic import Game.MyNat.Definition +import Mathlib.Lean.Expr.Basic + + namespace MyNat /-! diff --git a/Game/Tactic/Rfl.lean b/Game/Tactic/Rfl.lean index c1b68ec..63691dc 100644 --- a/Game/Tactic/Rfl.lean +++ b/Game/Tactic/Rfl.lean @@ -1,4 +1,4 @@ -import Game.Tactic.LeanExprBasic +import Lean.Meta.Tactic.Refl import Lean.Elab.Tactic.Basic /-! # `rfl` tactic diff --git a/Game/Tactic/Rw.lean b/Game/Tactic/Rw.lean index 7e6523e..4d28555 100644 --- a/Game/Tactic/Rw.lean +++ b/Game/Tactic/Rw.lean @@ -1,5 +1,6 @@ -import Game.Tactic.LeanExprBasic +import Mathlib.Lean.Expr.Basic import Lean.Elab.Tactic.Basic +-- import Lean.Elab.Tactic.Rewrite /-! # Modified `rw` diff --git a/lake-manifest.json b/lake-manifest.json index b321af9..1e591d0 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -4,25 +4,31 @@ [{"git": {"url": "https://github.com/EdAyers/ProofWidgets4", "subDir?": null, - "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8", + "rev": "a0c2cd0ac3245a0dade4f925bcfa97e06dd84229", "name": "proofwidgets", - "inputRev?": "v0.0.11"}}, + "inputRev?": "v0.0.13"}}, + {"git": + {"url": "https://github.com/mhuisi/lean4-cli.git", + "subDir?": null, + "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e", + "name": "Cli", + "inputRev?": "nightly"}}, {"git": {"url": "https://github.com/leanprover-community/mathlib4", "subDir?": null, - "rev": "88e129706828e01b7622d6635af1ca6667e25bac", + "rev": "b04c509ef69fc7939b5f67715a635e15743dbe3c", "name": "mathlib", - "inputRev?": "88e129706828e01b7622d6635af1ca6667e25bac"}}, + "inputRev?": "b04c509ef69fc7939b5f67715a635e15743dbe3c"}}, {"git": {"url": "https://github.com/gebner/quote4", "subDir?": null, - "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420", + "rev": "81cc13c524a68d0072561dbac276cd61b65872a6", "name": "Qq", "inputRev?": "master"}}, {"git": {"url": "https://github.com/JLimperg/aesop", "subDir?": null, - "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c", + "rev": "354432d437fb37738ed93ac6988669d78a870ed0", "name": "aesop", "inputRev?": "master"}}, {"git": @@ -34,6 +40,6 @@ {"git": {"url": "https://github.com/leanprover/std4", "subDir?": null, - "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936", + "rev": "e3c2be331da9ddeef7f82ca363f072a68d7210b3", "name": "std", "inputRev?": "main"}}]} diff --git a/lakefile.lean b/lakefile.lean index fc62b92..9dd9e62 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -19,8 +19,14 @@ 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" @ "88e129706828e01b7622d6635af1ca6667e25bac" + "https://github.com/leanprover-community/mathlib4" @ "b04c509ef69fc7939b5f67715a635e15743dbe3c" + + package Game where moreLeanArgs := #["-Dtactic.hygienic=false"] diff --git a/lean-toolchain b/lean-toolchain index fd602c4..dc4c3b8 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2023-06-20 +leanprover/lean4:nightly-2023-08-03