The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi,

The behavior of setoid_rewrite under binders is a little bit
confusing. Could someone explain what is wrong in the following
examples ?

Thanks,
Thomas Braibant

------------------------------------ Code begins here
------------------------------------
Require Import Setoid.
Module Nat.
Definition t := nat -> Prop.
Definition mor1 (f : t) : Prop := forall n,  f n.
Definition mor2 (i : nat) (f : t) : Prop := forall n, i < n -> f n.

Instance mor1_morph  :
Morphism (((@eq nat) ==> iff) ==> iff) (mor1).
Admitted.

Instance mor2_morph (i : nat) :
Morphism (((@eq nat) ==> iff) ==> iff) (@mor2 i).
Admitted.

Hypothesis H : forall n m, (n = m <-> m = n *m).
Goal mor1 (fun  n => n = n + n) <-> True.
setoid_rewrite H.
Abort. (* Ok *)

Goal mor2 5 (fun  n => n = n + n) <-> True.
setoid_rewrite H. (*  does not work *)
Abort.
End Nat.

(* This example looks like the first (working) one in module Nat, and
is not working here *)
Module Exemple.
Variable X: Set.
Variable zero: X.
Variable plus: X -> X -> X.
Variable nplus: nat -> X -> X.
Variable equal: X -> X -> Prop.

Variable sum: (nat -> X) -> X.
Infix "==" := equal (at level 50).

Variable Heq: Equivalence equal.
Variable sum_mor: forall f g, (forall i, f i == g i) -> sum f == sum g.

Instance eqeq : Equivalence equal.
apply Heq.
Qed.

Instance mor_morph :
Morphism (((@eq nat) ==> equal) ==> equal) (@sum).
repeat intro.  apply sum_mor. intro. apply H. reflexivity.
Qed.

Hypothesis H: forall x, plus zero x == zero.
Goal sum (fun  n => plus zero (nplus n zero)) == zero.
  setoid_rewrite H.  (* does not work *)
Abort.

End Exemple.