The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

(* Dear Andrej,

   This can be done using the [setoid_rewrite] tactic in Coq 8.2.
   Sadly, [rewrite] and [autorewrite] call a variant of
   [setoid_rewrite] which does not allow rewriting under binders to
   ensure backward compatibility. Anyhow, here's how you can do it:
*)

Axiom extensionality: forall (A B : Set), forall (f g : A -> B),
  (forall x : A, f x = g x) -> f = g.

Parameter A : Set.
Parameter op : A -> A -> A.
Parameter e : A.

Notation "x ** y" := (op x y) (at level 60, left associativity).

Axiom e_neutral_1: forall x, x ** e = x.
Axiom e_neutral_2: forall x, e ** x = x.
Hint Rewrite e_neutral_1 e_neutral_2 : my_hints.

(** We will use the support for subrelations to inform the tactic that
   pointwise equality and regular equality coincide. Now every  
morphism for
   one relation will be a morphism for the other. As every Coq  
function is a
   morphism for Leibniz equality, that'll make the pointwise  
extension available as
   as an equivalent for every argument of functional type. When we  
rewrite under a
   lambda as argument of [f : (A -> A) -> A], the tactic generates a  
constraint
   for [f] to be a morphism for pointwise equivalent functions, which  
will reduce
   to be a morphism for Leibniz-equal functions which is in turn  
trivial. *)

Require Import Setoid Morphisms Program.Syntax.

(** The [respectful RA RB] relation is reflexive when [RA] is included  
in equality and
   [RB] includes equality. This will be used to show, e.g that  
[Reflexive (pointwise_relation A eq ==> eq)] *)

Instance refl_respectful {A B : Set} `(sa : subrelation A RA eq)  
`(sb : subrelation B eq RB) : Reflexive (RA ++> RB)%signature.
Proof. intros. intros f x x' Hxx'. apply sb. f_equal. apply (sa _ _  
Hxx'). Qed.

(** The same lemma in terms of [subrelation] only that can be applied  
recursively. *)

Instance subrel_eq_respect {A B : Set} `(sa : subrelation A RA eq)  
`(sb : subrelation B eq RB) :
  subrelation eq (respectful RA RB).
Proof. intros. intros f g Hfg. subst. intros a a' Raa'. apply sb.  
f_equal. apply (sa _ _ Raa'). Qed.

(** Using extensionality, we can show that any two pointwise equal  
functions are Leibniz-equal: *)

Instance pointwise_eq_ext {A B : Set} `(sb : subrelation B RB (@eq  
B)) : subrelation (pointwise_relation A RB) eq.
Proof. intros. intros f g Hfg. apply extensionality. intros x. apply  
sb. apply (Hfg x). Qed.

(** Conversely, two equal functions are trivially pointwise-equal.  
This instance and [refl_respectful]
   should be in the library. *)

Instance eq_pointwise {A B : Set} `(sb : subrelation B (@eq B) RB) :  
subrelation eq (pointwise_relation A RB).
Proof. intros. intros f g Hfg x. apply sb. subst f. reflexivity. Qed.

(* Now suppose we want to simplify something that appears inside a
  lambda abstraction. *)

Lemma bar (f : (A -> A) -> A):
 f (fun x => e ** x) = f (fun x => x ** e).
Proof.
 intro f. setoid_rewrite e_neutral_1. setoid_rewrite e_neutral_2.
 reflexivity.
Qed.

(* You can look at the proof to see how [pointwise_eq_ext] is
   used: the structure of the proof basically mimics the one of
   the term, decorating it with congruence proofs.

   You can now build a tactic to do [setoid_rewrite] with your
   lemmas as much as possible, but there's currently no way to
   make [autorewrite] work here: it simply won't consider subterms
   under abstractions. I've been recently working on a rewrite of
   autorewrite to make it more efficient (instead of repeat rewrite,
   one can do multiple rewrites at once) and integrate it more nicely
   with setoids. In the current trunk, you can even specify particular
   rewriting strategies (à la ELAN) to apply to the term. On your
   example:
*)

Lemma baz (f : (A -> A) -> A):
  f (fun x => e ** x ** e ** x) = f (fun x => x ** x).
Proof.
  intros.
  (* The regular [autorewrite] is not using this particular strategy
     but it seems to give the best results: it rewrites using the hints
     in my_hints, trying to reach a fixpoint starting from the leaves  
of the
     term. *)
  clrewrite_strat (bottomup (hints my_hints)).
  Show Proof.
  reflexivity.
Qed.

(* Hope this helps,
   Matthieu
*)