From 5e43046c841e81a1f757e25e3024ee52e68a3d09 Mon Sep 17 00:00:00 2001
From: Seasawher <tellagoodstory@icloud.com>
Date: Fri, 6 Sep 2024 07:55:49 +0900
Subject: [PATCH] =?UTF-8?q?with=5Freducible=20=E3=81=AE=E4=BD=BF=E7=94=A8?=
 =?UTF-8?q?=E4=BE=8B=20Fixes=20#625?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 Examples/Tactic/WithReducible.lean | 84 ++++++++++++++++++++++++++++++
 src/SUMMARY.md                     |  1 +
 2 files changed, 85 insertions(+)
 create mode 100644 Examples/Tactic/WithReducible.lean

diff --git a/Examples/Tactic/WithReducible.lean b/Examples/Tactic/WithReducible.lean
new file mode 100644
index 00000000..95316cbf
--- /dev/null
+++ b/Examples/Tactic/WithReducible.lean
@@ -0,0 +1,84 @@
+/- # with_reducible
+`with_reducible` は、後に続くタクティクの透過度(transparency)を `reducible` に指定して実行します。
+
+透過度 `reducible` では、`[reducible]` の属性を持つ定義だけが展開されます。
+
+## 用途
+
+`with_reducible` はタクティクを定義するマクロを書く際に有用です。推移律を利用して、不等式を分割するタクティクを定義する例を示しましょう。
+
+まず、不等式の推移律を使う証明の例を示します。
+-/
+
+variable (a b c : Nat)
+
+example (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := by
+  -- b を経由して示す
+  apply Nat.le_trans (m := b) <;> assumption
+
+example (h₁ : a < b) (h₂ : b < c) : a < c := by
+  -- b を経由して示す
+  apply Nat.lt_trans (m := b) <;> assumption
+
+/- 今からすることは、この２つの命題を１つのタクティクで証明できるようにすることです。コードを素直に共通化しようとして次のようにマクロを定義すると上手くいきません。-/
+section --#
+/-- 推移律を扱うタクティク -/
+syntax "my_trans" term : tactic
+
+-- `<` に対するルール
+local macro_rules
+  | `(tactic| my_trans $e) => `(tactic| apply Nat.lt_trans (m := $e))
+
+-- `≤` に対するルール
+local macro_rules
+  | `(tactic| my_trans $e) => `(tactic| apply Nat.le_trans (m := $e))
+
+example (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := by
+  -- 成功
+  my_trans b <;> assumption
+
+example (h₁ : a < b) (h₂ : b < c) : a < c := by
+  -- 失敗
+  my_trans b <;> try assumption
+
+  exact Nat.le_of_succ_le h₂
+
+end --#
+/- マクロ展開のルールとして、Lean は後に定義されたルールを先に適用するので、常に `Nat.le_trans` を先に適用します。ところが `<` は `≤` を使って定義されているため、`<` に対しても `apply Nat.le_trans` が成功してしまいます。その結果、`<` に対して `Nat.lt_trans` を使ってくれないという結果になっています。-/
+
+/-- `<` は `≤` を使って定義されている -/
+example (n m : Nat) : (Nat.lt n m) = (Nat.le n.succ m) := rfl
+
+example (h₁ : a < b) (h₂ : b < c) : a < c := by
+  -- < に対しても Nat.le_trans が成功してしまう
+  apply Nat.le_trans (m := b)
+  · exact h₁
+  · exact Nat.le_of_succ_le h₂
+
+/- `with_reducible` を使用すると、`[reducible]` とマークされていない定義は展開されなくなるので、この挙動を防ぐことができます。 -/
+
+example (h₁ : a < b) (h₂ : b < c) : a < c := by with_reducible
+  -- < に対して Nat.le_trans が成功しなくなった！
+  fail_if_success apply Nat.le_trans (m := b)
+
+  apply Nat.lt_trans (m := b) <;> assumption
+
+section --#
+
+-- `<` に対するルール
+local macro_rules
+  | `(tactic| my_trans $e) => `(tactic| with_reducible apply Nat.lt_trans (m := $e))
+
+-- `≤` に対するルール
+local macro_rules
+  | `(tactic| my_trans $e) => `(tactic| with_reducible apply Nat.le_trans (m := $e))
+
+example (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c := by
+  -- 成功
+  my_trans b <;> assumption
+
+example (h₁ : a < b) (h₂ : b < c) : a < c := by
+  -- 成功
+  my_trans b <;> try assumption
+
+end --#
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 9ec56540..59927285 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -142,6 +142,7 @@
   - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md)
   - [try: 失敗をエラーにしない](./Tactic/Try.md)
   - [unfold: 定義に展開](./Tactic/Unfold.md)
+  - [with_reducible: 透過度指定](./Tactic/WithReducible.md)
   - [wlog: 一般性を失わずに特殊化](./Tactic/Wlog.md)
 
 - [項](./Term/README.md)