Merge pull request #876 from lean-ja/Seasawher/issue592

norm_cast タクティクを紹介する

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

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)