Search code examples
functioncoqproof

Struggling with functional extensionality

I've been programming in Coq for a few months now. Particularly, I'm interested in functional programming proofs where functions arise everywhere (optics, state monad, etc.). In this sense, dealing with functional extensionality has become essential, though extremely annoying. To illustrate the situation, let us assume a simplication of Monad (just one law defined):

Class Monad (m : Type -> Type) :=
{ ret : forall {X}, X -> m X
; bind : forall {A B}, m A -> (A -> m B) -> m B
}.
Notation "ma >>= f" := (bind ma f) (at level 50, left associativity).

Class MonadLaws m `{Monad m} :=
{ right_id : forall X (p : m X), p >>= ret = p }.

Now, I'd like to prove that chaining several rets to a program p should be equivalent to the very same program:

Example ugly_proof :
  forall m `{MonadLaws m} A (p : m A), 
    p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  intros.
  destruct H0 as [r_id].

  assert (J : (fun a2 : A => ret a2 >>= ret) =
              (fun a2 : A => ret a2)).
  { auto using functional_extensionality. }
  rewrite J.

  assert (K : (fun a1 : A => ret a1 >>= (fun a2 : A => ret a2)) =
              (fun a1 : A => ret a1)).
  { auto using functional_extensionality. }
  rewrite K.

  now rewrite r_id.
Qed.

The proof is correct, but the iterative assert pattern makes it very cumbersome. Indeed, it becomes impractical when things get more complex, as you can find in this proof (which evidences that an affine traversal is closed under composition).

Having said so, what is the best way of implementing the aforementioned proof? Is there any project or article (more approachable than this one) around functional extensionality to be taken as reference?

Solution

  • There is an approach with setoid_rewrite tactic (I tried to demostrate it in this answer):

    Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.

Generalizable All Variables.

Instance pointwise_eq_ext {A B : Type} `(sb : subrelation B RB eq)
  : subrelation (pointwise_relation A RB) eq.
Proof. intros f g Hfg. apply functional_extensionality. intro x; apply sb, (Hfg x). Qed.

Example easy_proof `{ml : MonadLaws m} `{p : m A} :
  p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof. now repeat setoid_rewrite right_id. Qed.

    Reading material: