From 249312421dfc0c6e4eb816d0cb5653fa5a51b247 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Sat, 21 Dec 2024 00:11:36 +0900
Subject: [PATCH] =?UTF-8?q?`push=5Fcast`=20=E3=82=92=E7=B4=B9=E4=BB=8B?=
 =?UTF-8?q?=E3=81=99=E3=82=8B=20Fixes=20#1206?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 LeanByExample/Tactic/PushCast.lean | 41 ++++++++++++++++++++++++++++++
 booksrc/SUMMARY.md                 |  1 +
 2 files changed, 42 insertions(+)
 create mode 100644 LeanByExample/Tactic/PushCast.lean

diff --git a/LeanByExample/Tactic/PushCast.lean b/LeanByExample/Tactic/PushCast.lean
new file mode 100644
index 00000000..8e6e197d
--- /dev/null
+++ b/LeanByExample/Tactic/PushCast.lean
@@ -0,0 +1,41 @@
+/- # push_cast
+
+`push_cast` タクティクは、ゴールや仮定に含まれる型強制（型キャスト）を「内側へ押し込む」はたらきをします。
+-/
+import Mathlib.Tactic
+
+example (m n : ℕ) (h : m ≥ n) : n + ((m - n) : ℕ) = (m : ℤ) := by
+  -- 示すべき命題には `m - n : ℕ` を整数 `ℤ` に型キャストしたものが含まれている。
+  guard_target =ₛ ↑n + ↑(m - n) = (m : ℤ)
+
+  -- この状態では整数と自然数の演算が混ざっていてややこしいので、
+  -- `ring` だけで示すことはできない。
+  fail_if_success solve
+  | ring
+
+  -- 自然数の引き算は整数での引き算とは異なる定義がされているが、
+  -- この場合は `h : m ≥ n` という仮定があるので、`m - n : ℤ` と一致する。
+  -- この変換を `push_cast` タクティックで行うことができる。
+  push_cast [h]
+
+  -- 型キャストが「内側に押し込まれ」て、整数の話になった。
+  show ↑n + (↑m - ↑n) = (m : ℤ)
+
+  -- `ring` で示せるようになった！
+  ring
+
+/- [`norm_cast`](./NormCast.md) や [`zify`](./Zify.md) などの型キャスト系のタクティクと併用されることもあります。-/
+
+example (m n : ℕ) (h : n ≥ m) : (n + m) * (n - m) = n * n - m * m := by
+  -- 整数にキャストする
+  zify
+
+  -- 自然数の引き算が含まれているので、`ring` では示せない
+  fail_if_success solve
+  | ring
+
+  -- 仮定 `h : n ≥ m` を使って、`n - m` と `n * n - m * m` を整数にキャストする
+  push_cast [h, show n * n ≥ m * m from by bound]
+
+  -- `ring` で示せるようになった！
+  ring
diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md
index 2268a94f..7d96dbe3 100644
--- a/booksrc/SUMMARY.md
+++ b/booksrc/SUMMARY.md
@@ -166,6 +166,7 @@
   - [omega: 自然数の線形計画を解く](./Tactic/Omega.md)
   - [plausible: 反例を見つける](./Tactic/Plausible.md)
   - [positivity: 正値性を示す](./Tactic/Positivity.md)
+  - [push_cast: 型キャストを内側へ](./Tactic/PushCast.md)
   - [push_neg: ドモルガン](./Tactic/PushNeg.md)
   - [qify: 有理数にキャストする](./Tactic/Qify.md)
   - [rcases: パターン分解](./Tactic/Rcases.md)