diff --git a/Examples.lean b/Examples.lean index e5a7abc1..985f105a 100644 --- a/Examples.lean +++ b/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 diff --git a/Examples/Replace.lean b/Examples/Replace.lean new file mode 100644 index 00000000..fff54e20 --- /dev/null +++ b/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 \ No newline at end of file diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 8083f2af..a051041e 100644 --- a/src/SUMMARY.md +++ b/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) diff --git a/src/replace.md b/src/replace.md new file mode 100644 index 00000000..2f665acf --- /dev/null +++ b/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}} +``` \ No newline at end of file