帰納型と帰納法: induction¶
自然数やリストのような inductive 型について証明するときは，induction を使います．
自然数 n : Nat に対する帰納法では，zero の場合と succ n の場合を証明します．
cases が単なる場合分けであるのに対して，induction は再帰的なコンストラクタの枝で帰納法の仮定を生成します．
theorem nat_add_assoc_by_induction (a b c : Nat) : (a + b) + c = a + (b + c) := by
induction a with
| zero =>
simp
| succ a ih =>
simp [Nat.succ_add, ih]
帰納法の帰納ステップでは，ih が帰納法の仮定です．
上の例では，ih : (a + b) + c = a + (b + c) を使って，Nat.succ a の場合を示しています．
theorem list_length_map_by_induction {α β : Type} (f : α → β) (xs : List α) :
(xs.map f).length = xs.length := by
induction xs with
| nil =>
rfl
| cons x xs ih =>
simp [ih]
自分で定義した inductive 型に対しても cases や induction を使えます．
次の Even は「偶数である」という命題を帰納的に定義したものです．
Even n は n が偶数であることを表す命題であり，その証明は zero と add_two から作られます．
inductive Even : Nat → Prop where
| zero : Even 0
| add_two {n : Nat} : Even n → Even (n + 2)
example : Even 4 := by
apply Even.add_two
apply Even.add_two
exact Even.zero
example (h : Even 1) : False := by
cases h
帰納的に定義された命題の証明 h : Even n に対しても induction h が使えます．
これは「その証明がどのコンストラクタで作られたか」に関する帰納法です．
cases h は不可能なコンストラクタの枝を自動的に消すため，Even 1 からは矛盾が得られます．
theorem even_plus_two_of_even {n : Nat} (h : Even n) : Even (n + 2) := by
exact Even.add_two h
example (n : Nat) (h : Even n) : Even (n + 2) := by
induction h with
| zero =>
exact Even.add_two Even.zero
| add_two h ih =>
exact Even.add_two ih
演習¶
induction で自然数の加法単位元を証明してください．