読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

リストの結合関数 ++ の結合則 l1 ++ (l2 ++ l3) == (l1 ++ l2) ++ l3

リストのappendの結合則は非常に便利だが、証明は簡単だ。こういった性質はテストでは網羅的にチェックできないため、証明という検証方法がプログラムの品質を高める上で非常に有効だと思う。

Require Import List.

Proposition p06 :
  forall {A} (l1 l2 l3: list A), l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3.
Proof.
intros A l1 l2 l3; induction l1; simpl in |- *.
 reflexivity.
 
 rewrite IHl1 in |- *.
 reflexivity.
Qed.