Half-verify alternative version of monad laws

cont.v

Parameter m : Type -> Type.
Notation c r a := ((a -> m r) -> m r).

Parameter lift : forall r a, m a -> c r a.
Arguments lift {r a}.

Parameter pure : forall a, a -> m a.
Arguments pure {a}.

Definition unlift {a} : c a a -> m a := fun u => u pure.

(* lift-unlift-pure monad laws *)

Parameter unlift_lift : forall a (u : m a), unlift (lift u) = u.
Parameter lift_pure' : forall a r (x : a), lift (unlift (fun k => k x)) = (fun (k : _ -> m r) => k x).
Parameter unlift_bind : forall (r a b : Type) (u : m a) (k : a -> m b) (h : b -> m r),
  lift (unlift (fun h => lift u (fun x => lift (k x) h))) h = lift u (fun x => lift (k x) h).

Lemma lift_pure : forall a r (x : a), lift (pure x) = (fun (k : _ -> m r) => k x).
Proof. apply lift_pure'. Qed.

Notation bind := lift.

(* bind-pure monad laws *)

Lemma bind_pure : forall a (u : m a), bind u pure = u.
Proof.
  apply unlift_lift.
Qed.

Lemma pure_bind : forall a b (x : a) (h : a -> m b), bind (pure x) h = h x.
Proof.
  intros; simpl. rewrite lift_pure. reflexivity.
Qed.

Require Import FunctionalExtensionality.

Lemma bind_bind : forall a b c (u : m a) (h : a -> m b) (l : b -> m c),
    bind (bind u h) l = bind u (fun x => bind (h x) l).
Proof.
  intros.
  rewrite <- unlift_bind. unfold unlift.
  replace (fun x => bind (h x) pure) with h.
  reflexivity.
  apply functional_extensionality.
  intros. symmetry; apply unlift_lift.
Qed.