単純化: `simp`，`simpa`，`<;>`¶

simp は，定義展開，既知の単純化補題，仮定を使った書き換えを組み合わせて，ゴールを単純化します．日常的に最もよく使う tactic の 1 つです． simp は登録された [simp] 補題を，原則として式が単純になる向きに使います．任意の定理を総当たりで使う tactic ではないので，使ってほしい定義や補題は simp [name] の形で明示します．

example (n : Nat) : n + 0 = n := by
  simp

example (xs : List Nat) : xs ++ [] = xs := by
  simp

追加で使いたい定義や補題を simp [name] の形で渡せます．

def addZeroTwice (n : Nat) : Nat :=
  n + 0 + 0

example (n : Nat) : addZeroTwice n = n := by
  simp [addZeroTwice]

仮定の中を単純化するときは simp at h と書けます． simp at * と書くと，ローカルコンテキストとゴール全体を対象にできますが，証明が読みにくくなる場合もあります．

example (n m : Nat) (h : n + 0 = m) : n = m := by
  simp at h
  exact h

simpa using h は，h の型と現在のゴールを単純化して一致させます．最後の一手として非常に便利です．内部的には「h を使う前後で simp する」と考えると読みやすいです．

example (n m : Nat) (h : n + 0 = m) : n = m := by
  simpa using h

simp_all は，ゴールとローカルコンテキストの仮定をまとめて単純化します．仮定が多いときに有効です．

example (n m : Nat) (h : n = m) : n + 1 = m + 1 := by
  simp_all

<;> は tactic を連結する notation です． tac1 <;> tac2 と書くと，まず tac1 を実行し，その結果生じたすべてのゴールに tac2 を実行します．同じ後処理を複数のゴールにまとめて適用したいときに使います．

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor <;> assumption

example (a b : Nat) : a + b = b + a ∧ a + 0 = a := by
  constructor <;> simp [Nat.add_comm]

上の 1 つ目は，次の証明を短く書いたものです．

example (P Q : Prop) (hP : P) (hQ : Q) : P ∧ Q := by
  constructor
  · assumption
  · assumption

便利ですが，複雑な証明で乱用すると各ゴールに何が起きたか読みにくくなります．最初は明示的に箇条書きで証明し，繰り返しが明らかなときだけ <;> でまとめるのが無難です．

演習¶

simp で証明できる命題を，まず手動で証明し，その後 simp や simpa で短くしてください．

example (n : Nat) : n + 0 = n := by
  -- まず `induction`，次に `simpa` で試す．
  sorry

単純化: simp，simpa，<;>¶

演習¶

単純化: `simp`，`simpa`，`<;>`¶