リストの結合関数 ++ の結合則 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.