リストのリストをリストにするやつがモナドであることを示しました。

concat_is_monad.v

Require Import List.
Import ListNotations.

Theorem concat_assoc(X: Type):
  forall tttx: list (list (list X)), (concat (concat tttx)) = (concat (map (@concat X) tttx)).
Proof.
  intros.
  induction tttx.
  simpl. reflexivity.
  simpl. rewrite <- IHtttx. apply concat_app.
Qed.

Theorem concat_unit1(X: Type):
  forall tx: (list X), tx = (concat [tx]).
Proof.
  intros.
  destruct tx.
  simpl. reflexivity.
  simpl. rewrite app_nil_r. reflexivity.
Qed.

Theorem concat_unit2(X: Type):
  forall tx: (list X), tx = (concat (map (fun x=>[x]) tx)).
Proof.
  intros.
  induction tx.
  simpl. reflexivity.
  simpl. rewrite <- IHtx. reflexivity.
Qed.