From 882517f9f48cb37bd21203110df0df1dd6df3523 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Tue, 24 Sep 2024 01:35:41 +0900
Subject: [PATCH] =?UTF-8?q?norm=5Fcast=20=E3=82=BF=E3=82=AF=E3=83=86?=
 =?UTF-8?q?=E3=82=A3=E3=82=AF=E3=82=92=E7=B4=B9=E4=BB=8B=E3=81=99=E3=82=8B?=
 =?UTF-8?q?=20Fixes=20#592?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Tactic/NormCast.lean | 29 +++++++++++++++++++++++++++++
 src/SUMMARY.md                |  1 +
 2 files changed, 30 insertions(+)
 create mode 100644 Examples/Tactic/NormCast.lean

diff --git a/Examples/Tactic/NormCast.lean b/Examples/Tactic/NormCast.lean
new file mode 100644
index 00000000..97798370
--- /dev/null
+++ b/Examples/Tactic/NormCast.lean
@@ -0,0 +1,29 @@
+/- # norm_cast
+
+`norm_cast` は、型キャスト（ある型からある型への変換）と型強制を簡約するタクティクです。
+
+詳細については論文 [「Simplifying Casts and Coercions」](https://arxiv.org/abs/2001.10594) などを参照してください。
+-/
+import Mathlib.Tactic
+
+-- `x, m, n` は自然数とする
+variable (x m n : ℕ)
+
+example (left : (x : ℝ) < ↑m + ↑n) (right : ↑m + ↑n < (x : ℝ) + 1) : False := by
+  -- `linarith` では示すことができない
+  fail_if_success linarith
+
+  -- `omega` でも示すことができない
+  fail_if_success omega
+
+  -- 仮定の `left` と `right` は実数上の不等式だが、
+  -- 自然数上の不等式と解釈できるはずである。
+  -- `norm_cast` はそれを実行してくれる。
+  norm_cast at left right
+
+  -- 仮定が自然数における不等式に変わった！
+  guard_hyp left : x < m + n
+  guard_hyp right : m + n < x + 1
+
+  -- 後は `omega` で示せる
+  omega
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 7c58deff..c88e395e 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -134,6 +134,7 @@
   - [linarith: 線形(不)等式を示す](./Tactic/Linarith.md)
   - [native_decide: 実行による証明](./Tactic/NativeDecide.md)
   - [nlinarith: 非線形な(不)等式を示す](./Tactic/Nlinarith.md)
+  - [norm_cast: 型キャストの簡略化](./Tactic/NormCast.md)
   - [nth_rw: n 番目の項だけ rw](./Tactic/NthRw.md)
   - [obtain: 分解して取り出す](./Tactic/Obtain.md)
   - [omega: 自然数の線形計画を解く](./Tactic/Omega.md)