implementations.cons_list

Require Import
 List
 abstract_algebra interfaces.monads.

Implicit Arguments app [[A]].

Section contents.
  Context A `{Setoid A}.

  Global Instance list_eq: Equiv (list A) :=
    fix F (a b: list A) :=
      match a, b with
      | nil, nil => True
      | x::y, x'::y' => x = x' @equiv _ F y y'
      | _, _ => False
      end.

  Global Instance: Proper (=) (@cons A).

  Instance: Reflexive (_: Equiv (list A)).

  Instance: Symmetric (_: Equiv (list A)).

  Instance: Transitive (_: Equiv (list A)).

  Global Instance: Setoid (list A).

  Global Instance: SemiGroupOp (list A) := app.

  Global Instance app_proper: Proper (=) (@app A).

  Global Instance app_assoc_inst: Associative (@app A).

  Global Instance: SemiGroup (list A) := {}.

  Global Instance: MonoidUnit (list A) := nil.

  Global Instance: Monoid (list A).

  Definition concat: list (list A) list A := fold_right app nil.

  Lemma concat_app (a b: list (list A)): concat (a ++ b) = concat a ++ concat b.
End contents.

Implicit Arguments concat [[A]].

Instance concat_proper `{Equiv A}: Proper (=) (@concat A).

Instance: MonadReturn list := λ _ x, [x].
Instance: MonadBind list := λ _ _ l f, concat (map f l).

Instance ret_proper `{Equiv A}: Proper (=) ((_: MonadReturn list) A).

Instance bind_proper `{Equiv A} `{Equiv B}: Proper (=) ((_: MonadBind list) A B).