replace 追加

Examples.lean

@@ -22,6 +22,7 @@ import Examples.Linarith
 import Examples.Nlinarith
 import Examples.Refine
 import Examples.Rel
+import Examples.Replace
 import Examples.Rfl.Refl
 import Examples.Rfl.Rfl
 import Examples.Ring

Examples/Replace.lean

@@ -0,0 +1,33 @@
+import Mathlib.Algebra.Parity
+import Mathlib.Tactic.NthRewrite
+import Mathlib.Tactic.Ring
+
+-- ANCHOR: first
+example : ∀ (n : Int), Even (5 * n) → Even n := by
+  intro n hn
+
+  -- `Even (5 * n)` という仮定を分解
+  obtain ⟨ k, hk ⟩ := hn
+
+  -- 以下がローカルコンテキストに追加される
+  guard_hyp hk: 5 * n = k + k
+
+  -- `k + k` という形が使いづらいので，`2 * k` に置き換える
+  replace hk : 5 * n = 2 * k := by
+    rw [hk]
+    ring
+
+  -- `hk` の内容が変化している
+  guard_hyp hk: 5 * n = 2 * k
+
+  -- 計算をする
+  have := by
+    calc n
+      _ = 5 * n - 4 * n := by ring
+      _ = 2 * k - 4 * n := by rw [hk]
+      _ = 2 * (k - 2 * n) := by ring
+
+  exists k - 2 * n
+  nth_rewrite 1 [this]
+  ring
+-- ANCHOR: first

src/SUMMARY.md

@@ -32,6 +32,7 @@
 - [push_neg: ドモルガン](./push_neg.md)
 - [refine: プレースホルダを使う](./refine.md)
 - [rel: 不等式を使う](./rel.md)
+- [replace: 補題の入れ替え](./replace.md)
 - [rfl: 関係の反射性を示す](./rfl.md)
 - [ring: 環の等式を示す](./ring.md)
 - [rw: 同値変形](./rw.md)

src/replace.md

@@ -0,0 +1,13 @@
+# replace
+
+needs: `import Std.Tactic.Replace`
+
+`replace` は [have](./have.md) と同じく補題を入手するためのタクティクですが，`have` とは異なりローカルコンテキストにすでにある命題を置き換えることができます．
+
+`have` を使った場合，ローカルコンテキストにすでに `h : P` がある状態で，再び `h` という名前で別の命題を示すと，古い方の `h` はアクセス不能になって `†` が付いた状態になってしまいます．
+
+`replace` であれば，古い方が新しい方に置き換えられ，`†` の付いた命題は出現しません．
+
+```lean
+{{#include ../Examples/Replace.lean:first}}
+```