Struggling with functional extensionality

2
votes

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?

3
functioncoqproof

3 Answers

2
votes

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:

2
votes

I'm going to generalize right_id law a bit:

Require Import Coq.Logic.FunctionalExtensionality.
Generalizable Variables m A.

Lemma right_id_gen `{ml : MonadLaws m} `{p : m A} r :
  r = ret -> p >>= r = p.
Proof. intros ->; apply ml. Qed.

Now we can use backward reasoning:

Example not_so_ugly_proof `{ml : MonadLaws m} `{p : m A} :
  p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  apply right_id_gen, functional_extensionality; intros.
  apply right_id_gen, functional_extensionality; intros.
  now apply right_id_gen.
Qed.
1
votes

You can rewrite the RHS to p >>= ret and reason backwards with f_equal, changing the goal to (fun _ => ...) = ret where functional_extensionality is applicable.

Class MonadLaws m `{Monad m} :=
  { right_id : forall X (p : m X), p >>= ret = p }.
Example ugly_proof :
  forall m `{MonadLaws m} A (p : m A), 
    p >>= (fun a1 => ret a1 >>= (fun a2 => ret a2 >>= ret)) = p.
Proof.
  intros.
  transitivity (p >>= ret).
  rewrite <- (right_id _ p) at 2.
  f_equal.
  apply functional_extensionality.
  intro x.
  rewrite <- (right_id _ (ret x)) at 2.
  f_equal.
  apply functional_extensionality.
  intro x0.
  rewrite <- (right_id _ (ret x0)) at 2.
  auto.
Qed.