The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

On Sat, 2 Jul 2011 14:14:10 +0200
Bas Spitters 
<spitters AT cs.ru.nl>
 wrote:

> You probably need functional extensionality/setoids.
> 

Thanks, that certainly helped:

  Lemma left_identity : forall (A B : Type) (x : A) (f : A -> M B),
    bind (return_m x) f = f x.
  Proof.
    intros A B x f.

    unfold return_m.
    unfold bind.
    unfold run.

    destruct (f x).
    assert (forall s : S, p s = (fun t : S => p t) s) as H0.
      reflexivity.
    assert (p = (fun s : S => p s)) as H1.
      apply (functional_extensionality p (fun s : S => p s) H0).

    rewrite <- H1.
    reflexivity.
  Defined.

  Lemma right_identity : forall (A : Type) (m : M A),
    bind m return_m = m.
  Proof.
    intros A m.
    destruct m.

    unfold bind.
    unfold run.
    unfold return_m.

    assert (forall s : S, p s = (fun t : S => let (a, t') := p t in (a, t')) 
s) as H1.
      intro s. destruct (p s). reflexivity.
    assert (p = (fun s : S => let (a, s') := p s in (a, s'))) as H2.
      apply (functional_extensionality p (fun s : S => let (a, s') := p s in 
(a, s')) H1).

    rewrite <- H2.
    reflexivity.
  Defined.

The proof of associativity still eludes me. Work continues...