Lean と Mathlib のバージョンを v4.13.0-rc3 に更新

Examples/Declarative/Opaque.lean

@@ -36,11 +36,10 @@ opaque opaque_greet : String := "hello world!"
 
 -- 等しいことの証明が rfl ではできない
 /--
-error: The rfl tactic failed. Possible reasons:
-- The goal is not a reflexive relation (neither `=` nor a relation with a @[refl] lemma).
-- The arguments of the relation are not equal.
-Try using the reflexivity lemma for your relation explicitly, e.g. `exact Eq.refl _` or
-`exact HEq.rfl` etc.
+error: tactic 'rfl' failed, the left-hand side
+  opaque_greet
+is not definitionally equal to the right-hand side
+  greet
 ⊢ opaque_greet = greet
 -/
 #guard_msgs in example : opaque_greet = greet := by rfl

Examples/Declarative/Syntax.lean

@@ -46,11 +46,13 @@ local syntax term " = " term " as " term : term
 local macro_rules
   | `(term| $a = $b as $c) => `(@Eq (α := $c) $a $b)
 
+set_option pp.mvars false --#
+
 -- `Nat` と `Prop` を足すことはできないというエラーメッセージ。
 -- `1 + (1 = 2)` だと認識されてしまっているようだ。
 /--
 warning: failed to synthesize
-  HAdd Nat Prop ?m.1897
+  HAdd Nat Prop ?_
 Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (warning) in

Examples/Tactic/Induction.lean

@@ -43,7 +43,7 @@ theorem sum_exp (n : Nat) : sum n = n * (n + 1) / 2 := by
   match n with
 
   -- `n = 0` の場合
-  | 0 => rfl
+  | 0 => simp [sum]
 
   -- `0` から `n` までの自然数で成り立つと仮定する
   | n + 1 =>
@@ -62,7 +62,7 @@ theorem sample : True := by
   have h : ∀ n, sum n = n * (n + 1) / 2 := by
     intro n
     match n with
-    | 0 => rfl
+    | 0 => simp [sum]
     | n + 1 =>
       -- h 自身を参照することができない
       fail_if_success have ih := h n

Examples/Tactic/Qify.lean

@@ -16,7 +16,7 @@ example (h : x ≥ 1) : 2 * x ≥ 2 := by
   show (2 : ℚ) ≤ 2 * x
 
   calc
-    (2 : ℚ) = 2 * 1 := by rfl
+    (2 : ℚ) = 2 * 1 := by simp
     _ ≤ 2 * (x : ℚ) := by gcongr
 
 /- より自然な例として、次の例も挙げておきます。-/
@@ -39,7 +39,8 @@ theorem sumPoly_succ {n : Nat} : sumPoly (n + 1) = (n + 1) + sumPoly n := by
   ring
 
 @[simp]
-theorem sumPoly_zero : sumPoly 0 = 0 := by rfl
+theorem sumPoly_zero : sumPoly 0 = 0 := by
+  simp [sumPoly]
 
 /-- `sumPoly` の値は常に自然数で、`sum` と一致する -/
 theorem sum_eq_sumPoly {n : Nat} : sum n = sumPoly n := by

Examples/Type/List.lean

@@ -147,7 +147,12 @@ def List.sum : List Nat → Nat
   | n :: ns => n + sum ns
 
 /-- List.sum は List.foldr で表すことができる -/
-example : List.foldr (· + ·) 0 = List.sum := by rfl
+example : List.foldr (· + ·) 0 = List.sum := by
+  -- 再帰的な定義を分解する
+  delta List.foldr List.sum
+
+  -- 両者は等しい
+  rfl
 
 /-- 末尾再帰にした総和関数 -/
 def List.sumTR (l : List Nat) : Nat :=
@@ -159,4 +164,9 @@ where
   | x, n :: ns => aux (x + n) ns
 
 /-- List.sumTR は List.foldl で表すことができる -/
-example : List.foldl (· + ·) 0 = List.sumTR := by rfl
+example : List.foldl (· + ·) 0 = List.sumTR := by
+  -- 再帰的な定義を分解する
+  delta List.foldl List.sumTR List.sumTR.aux
+
+  -- 両者は等しい
+  rfl

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "ee574d84585a9e08845bb984b8f60a14e4c86920",
+   "rev": "9329da681507102b3242600efe9f79e57ae85f42",
    "name": "«mk-exercise»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "a6f34a4da30b8284ab295da918022b51b68f7e13",
+   "rev": "d07724c3f70b6df81b49535095a35151c4a5e42c",
    "name": "mdgen",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "4756e0fc48acce0cc808df0ad149de5973240df6",
+   "rev": "13f9b00769bdac2c0041406a6c2524a361e8d660",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ff420521a0c098891f4f44ecda9dd7ff57b50bad",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e285a7ade149c551c17a4b24f127e1ef782e4bb1",
+   "rev": "63a7d4a353f48f6c5f1bc19d0f018b0513cb370a",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -95,7 +95,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "655d653bfd6eb4968829ce8e2b5e4ed0419f6f05",
+   "rev": "5ddd0ae2d57a887d36d8c99db785285cbf154439",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.12.0
+leanprover/lean4:v4.13.0-rc3