Previously, I was told how to
use setoid_rewrite to deal with functional_extensionality. Unluckily, I've
found that this nice solution doesn't work in the following scenario. Suppose
that we've defined a Monoid class:
Class Monoid (m : Type) :=
{ mzero : m
; mappend : m -> m -> m
}.
Notation "m1 * m2" := (mappend m1 m2) (at level 40, left associativity).
Class MonoidLaws m `{Monoid m} :=
{ left_unit : forall m, mzero * m = m (* ; other laws... *) }.
If we add pointwise_eq_ext in
the picture, monoid_proof becomes trivial:
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.
apply (Hfg x).
Qed.
Example monoid_proof `{ml : MonoidLaws m} :
(fun m => mzero * m) = (fun m => m).
Proof. now setoid_rewrite left_unit. Qed.
However, if the same monoid expression appears as an argument for option_fold,
the tactic fails:
Definition option_fold {A B} (some : A -> B) (none : B) (oa : option A) : B :=
match oa with
| Some a => some a
| None => none
end.
(* Expression is an argument for [option_fold] *)
Example monoid_proof' `{ml : MonoidLaws m} :
forall om,
option_fold (fun m => mzero * m) mzero om = option_fold (fun m => m) mzero om.
Proof. intros. now setoid_rewrite left_unit. (* error! *) Qed.
I'm not familiar with the details of setoid_rewrite, but it seems that the
pattern matching is conforming a context which is preventing this tactic to
execute properly. Is there any way to teach setoid_rewrite how to deal with
this kind of situations? I've been trying to provide several subrelation
instances, but I lack the theoretical background to understand the whole
picture. A general solution would be awesome, but I'd be happy enough with an
ad hoc approach to rewrite expressions in the arguments of (nested)
invocations of option_fold.
The pointwise_eq_ext instance lets you to rewrite in the goals like this one:
(fun m => mzero * m) = (fun m => m)
but things break if you have your function inside some context. To fix this you need to add the following subrelation:
Instance subrel_eq_respect {A B : Type}
`(sa : subrelation A RA eq)
`(sb : subrelation B eq RB) :
subrelation eq (respectful RA RB).
Proof. intros f g -> a a' Raa'. apply sb. f_equal. apply (sa _ _ Raa'). Qed.
You might want to take a look at the full code in this Coq Club post by Matthieu Sozeau.