From a80f93554a3d6dd5d08333ff969db5383375c231 Mon Sep 17 00:00:00 2001 From: Seasawher Date: Sat, 5 Oct 2024 02:36:08 +0900 Subject: [PATCH] =?UTF-8?q?Lean=20=E3=81=A8=20Mathlib=20=E3=81=AE=E3=83=90?= =?UTF-8?q?=E3=83=BC=E3=82=B8=E3=83=A7=E3=83=B3=E3=82=92=20`v4.13.0-rc3`?= =?UTF-8?q?=20=E3=81=AB=E6=9B=B4=E6=96=B0?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Examples/Declarative/Opaque.lean | 9 ++++----- Examples/Declarative/Syntax.lean | 4 +++- Examples/Tactic/Induction.lean | 4 ++-- Examples/Tactic/Qify.lean | 5 +++-- Examples/Type/List.lean | 14 ++++++++++++-- lake-manifest.json | 12 ++++++------ lean-toolchain | 2 +- 7 files changed, 31 insertions(+), 19 deletions(-) diff --git a/Examples/Declarative/Opaque.lean b/Examples/Declarative/Opaque.lean index 0335b73a..401faa1b 100644 --- a/Examples/Declarative/Opaque.lean +++ b/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 diff --git a/Examples/Declarative/Syntax.lean b/Examples/Declarative/Syntax.lean index 73557383..3b1e99ea 100644 --- a/Examples/Declarative/Syntax.lean +++ b/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 diff --git a/Examples/Tactic/Induction.lean b/Examples/Tactic/Induction.lean index ea5fee15..dc7b3b6f 100644 --- a/Examples/Tactic/Induction.lean +++ b/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 diff --git a/Examples/Tactic/Qify.lean b/Examples/Tactic/Qify.lean index 06337051..8b18714d 100644 --- a/Examples/Tactic/Qify.lean +++ b/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 diff --git a/Examples/Type/List.lean b/Examples/Type/List.lean index feccdd61..5c1ec33c 100644 --- a/Examples/Type/List.lean +++ b/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 diff --git a/lake-manifest.json b/lake-manifest.json index 2cba5f79..b14bce9b 100644 --- a/lake-manifest.json +++ b/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", diff --git a/lean-toolchain b/lean-toolchain index 89985206..eff86fd6 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.12.0 +leanprover/lean4:v4.13.0-rc3