タクティク紹介: decide

Seasawher commented 2 weeks ago

rfl と同様に式の証明に使うことができるので，rfl との違いを強調したい

Seasawher commented 2 weeks ago

rfl は反射的な関係を扱うが，decide は決定可能な命題を示す．

/-- 奇数であること．Mathlib にある定義とは別に自前で用意 -/
def Odd (n : Int) : Prop := ∃ t : Int, n = 2 * t + 1

/-- 奇数であることが決定可能であること -/
instance (n : Int) : Decidable (Odd n) := by
  -- n % 2 の計算に帰着させる
  refine decidable_of_iff (n % 2 = 1) ?_
  dsimp [Odd]
  constructor <;> intro h
  · exists (n / 2)
    omega
  · obtain ⟨t, th⟩ := h
    rw [th]
    omega

-- decide で証明できる
example : Odd (7 : Int) := by
  decide

Seasawher commented 2 weeks ago

だから decide は不等式を示すことができるし，「この命題は間違っている」というメッセージを出すこともできる

example : 1 ≠ 2 + 3 := by decide

lean-ja / lean-by-example

タクティク紹介: decide #324