diff --git a/LeanByExample/Tactic/Symm.lean b/LeanByExample/Tactic/Symm.lean new file mode 100644 index 00000000..3f864215 --- /dev/null +++ b/LeanByExample/Tactic/Symm.lean @@ -0,0 +1,78 @@ +/- # symm + +`symm` は、等式や同値性などの対称な関係の向きを反転するタクティクです。 + +たとえばゴールが `b = a` であるとき、`symm` を実行するとゴールは `a = b` に変わります。-/ + +variable {a b c : Nat} + +example (h : a = b) : b = a := by + symm + + -- ゴールが反転する + guard_target =ₛ a = b + + assumption + +/- ## 仮定を反転する + +`symm at h` と書くと、ローカルコンテキストにある仮定 `h` の向きを反転できます。-/ + +example (h : a = b) (ha : a + c = 0) : b + c = 0 := by + symm at h + + -- 仮定の向きが反転する + guard_hyp h : b = a + + rw [h] + assumption + +/- ## 同値関係にも使える + +`symm` は等式だけではなく、命題の同値性 `↔` にも使えます。-/ + +example {P Q : Prop} (h : Q ↔ P) : P ↔ Q := by + symm + + -- ゴールが反転する + guard_target =ₛ Q ↔ P + + assumption + +example {P Q : Prop} (h : P ↔ Q) (hq : Q) : P := by + symm at h + + -- 仮定の向きが反転する + guard_hyp h : Q ↔ P + + rw [h] at hq + assumption + +/- ## カスタマイズ + +一般の二項関係に対して `symm` を使いたい場合は、その関係が対称であることを示す定理に `[symm]` 属性を付与します。-/ + +/-- 2つの自然数の差が高々1であることを表す関係 -/ +def Close (x y : Nat) : Prop := + x ≤ y + 1 ∧ y ≤ x + 1 + +/-- `Close` は対称な関係 -/ +theorem Close.symm {x y : Nat} (h : Close x y) : Close y x := by + exact ⟨h.right, h.left⟩ + +example {x y : Nat} (h : Close x y) : Close y x := by + -- 登録していないと `symm` は使用できない + fail_if_success symm + + exact Close.symm h + +-- `Close` が対称であることを登録する +attribute [symm] Close.symm + +example {x y : Nat} (h : Close x y) : Close y x := by + symm + + -- `Close y x` が `Close x y` に反転する + guard_target =ₛ Close x y + + assumption diff --git a/booksrc/SUMMARY.md b/booksrc/SUMMARY.md index 4dbda57f..1fa5cab9 100644 --- a/booksrc/SUMMARY.md +++ b/booksrc/SUMMARY.md @@ -260,6 +260,7 @@ - [sorry: 証明したことにする](./Tactic/Sorry.md) - [split: if/match 式を分解](./Tactic/Split.md) - [suffices: 十分条件に帰着](./Tactic/Suffices.md) + - [symm: 対称な関係の向きを反転する](./Tactic/Symm.md) - [tauto: トートロジーを示す](./Tactic/Tauto.md) - [trans: 推移律を利用する](./Tactic/Trans.md) - [trivial: 基本的なタクティクを試す](./Tactic/Trivial.md)