The Coq mailing list

["Mark Dickinson" <dickinsm AT gmail.com>]

(**

Section 23.12 of the reference manual for Coq v8.2, 'Constant
unfolding', seems to say that setoid_rewrite and related tactics
should automatically unfold definitions declared using "Typeclasses
unfold ...".

I'm having some trouble making this work, and am wondering what I'm
doing wrong.  Here's a summary, with the boring bits omitted (the full
code is included at the end of this message).  In the following, 'set'
is a type of setoids, '==' is setoid equality, and 'A >-> B' is the
setoid of '=='-respecting maps from A to B.  After doing:

  Definition binary_operation A : set := A >-> A >-> A.
  Definition associative (A : set) (op : binary_operation A) : Prop := ...
  Definition commutative (A : set) (op : binary_operation A) : Prop := ...
  Typeclasses unfold binary_operation associative commutative.

I declare a type of commutative semigroups with:

  Record ab_semigrp : Type := {
    carrier :> set;
    addition : binary_operation carrier;
    assoc : associative addition;
    comm : commutative addition
  }.
  Notation "x + y" := (addition _ x y).

Now I attempt to prove the following:

  Lemma add_rotate : forall A : ab_semigrp, forall x y z : A,
    x + y + z == y + z + x.
  Proof.
    intros.
    setoid_rewrite <- assoc at 1.
    setoid_rewrite comm at 1.
    reflexivity.
  Qed.

But the proof stops at the first 'setoid_rewrite', with the error message:

  Toplevel input, characters 16-44:
  Error: The term does not end with an applied homogeneous relation.

So it looks as though setoid_rewrite can't or won't unfold
'associative'.  If I manually unfold 'associative' in the declaration
of assoc:

  assoc : forall a b c : carrier,
    addition a (addition b c) == addition (addition a b) c;

(and similarly for comm) then the proof works as intended.  I can also
make it work by supplying enough arguments to assoc to force the
unfolding;  for example,

  setoid_rewrite <- (assoc A x) at 1.
  setoid_rewrite (comm A x) at 1.

But if I'm reading section 23.12 right, then neither of these tricks
should be necessary.  What am I missing here?  Is there a good reason
why setoid_rewrite doesn't automatically unfold 'associative'?

I'm using a fairly recent (Nov 1.) build of the v8.2 svn branch.

Here's the complete code.

**)

Set Implicit Arguments.

Require Import Setoid.

(* sets are represented by setoids *)
Record set : Type := {
  element :> Type;
  equal : relation element;
  equiv_prf : equivalence element equal
}.
Notation "x == y" := (equal _ x y) (at level 70, no associativity).

(* Maps A B is the set of functions from a set A to a set B *)
Record function (A B : set) : Type := {
  felement :> A -> B;
  equal_prf : forall x y : A, x == y -> felement x == felement y
}.
Definition fequal (A B : set) (f g : function A B) :=
  forall x, felement f x == felement g x.
Lemma fequal_equiv : forall A B : set, equivalence (function A B) (@fequal A 
B).
Proof.
  intros A B. unfold fequal.
  generalize (equiv_prf B); split; elim H; eauto with sets.
Qed.
Definition Maps (A B : set) := Build_set (fequal_equiv A B).
Notation "A >-> B" := (Maps A B) (at level 95, right associativity).

(* register equal and fequal as relations, felement as morphism *)
Add Parametric Relation (A : set) : (element A) (equal A)
  reflexivity proved by (equiv_refl _ _ (equiv_prf A))
  symmetry proved by (equiv_sym _ _ (equiv_prf A))
  transitivity proved by (equiv_trans _ _ (equiv_prf A))
as element_equal_equivalence.

Add Parametric Relation (A B : set) : (function A B) (@fequal A B)
  reflexivity proved by (equiv_refl _ _ (equiv_prf (Maps A B)))
  symmetry proved by (equiv_sym _ _ (equiv_prf (Maps A B)))
  transitivity proved by (equiv_trans _ _ (equiv_prf (Maps A B)))
as function_fequal_equivalence.

Add Parametric Morphism A B : (@felement A B)
  with signature (@fequal A B ==> equal A ==> equal B) as felement_morphism.
Proof.
  unfold fequal. intros f g H1 x y H2.
  generalize (equal_prf g x y H2) (equiv_trans _ _ (equiv_prf B)).
  eauto with sets.
Qed.

Definition binary_operation A : set := A >-> A >-> A.
Definition associative (A : set) (op : binary_operation A) : Prop :=
  forall a b c : A, op a (op b c) == op (op a b) c.
Definition commutative (A : set) (op : binary_operation A) : Prop :=
  forall a b : A, op a b == op b a.

Typeclasses unfold binary_operation associative commutative.

Record ab_semigrp : Type := {
  carrier :> set;
  addition : binary_operation carrier;
  assoc : associative addition;
  comm : commutative addition
}.
Notation "x + y" := (addition _ x y).

Lemma add_rotate : forall A : ab_semigrp, forall x y z : A,
  x + y + z == y + z + x.
Proof.
  intros.
  setoid_rewrite <- assoc at 1.
  setoid_rewrite comm at 1.
  reflexivity.
Qed.