CoqのFixpointと帰納法を用いた証明

これまでの記事

前回:https://zenn.dev/emma_e_evans/articles/de3c743845c2cf2dd42d

Fixpoint

Fixpointでは再帰的な関数を定義することができます。
前回のnatとPreに対して，n回のPreを適用するnPreという関数を定義してみましょう。

Fixpoint nPre (n:nat) (m:nat): nat :=
 match n, m with
 | O, _ => n
 | l, O => l
 | S l, S k => nPre l k
 end.

帰納法を用いた証明

この関数を使用した次の命題「任意の自然数nに対して，ある自然数mが存在して，nにm回Preを適用すればOになる。」を証明します。この命題を仮にprop2とします。
前回は命題の証明を始める際にDefinitionコマンドを使いましたが，今回はExampleを使います。使い方は全く同じです。

Example prop2: forall n:nat, exists m:nat, nPre n m = O.
Proof.
intros. (* nを仮定に追加 *)
exists (S n). (* mの具体的な値としてS nをとる *)
induction n. (* nに関する帰納法で証明する *)
(* n=Oのとき，nPre O (S O) = Oを証明する *)
reflexivity. 
(* nPre n (S n) = Oが成り立つと仮定して，nPre (S n) (S (S n))が成り立つことを証明する *)
simpl.
apply IHn. (* 仮定を適用 *)
Qed.

上のように帰納法を使いたいときはinductionタクティクスを使えばOKです。

次回はandとorを含む命題の証明をします。