【Lean4】simp

simp

定義や基本的な等式を使って、式を自動的に簡単にする

Plaintext

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

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

定義を指定して展開することもできる

Plaintext

def double (n : ℕ) : ℕ :=
  n + n

example : double 0 = 0 := by
  simp [double]

/-
simp [double]は
１．doubleを展開する
２．0 + 0を簡約する
という処理を行う
-/

def double (n : ℕ) : ℕ :=
  n + n

example : double 0 = 0 := by
  simp [double]

/-
simp [double]は
１．doubleを展開する
２．0 + 0を簡約する
という処理を行う
-/