The Coq mailing list

["Aaron Bohannon" <bohannon AT cis.upenn.edu>]

The first code snippet below is the smallest complete example I could
find of the problematic situation.  (The "rewrite" tactic in the lemma
foo2 fails.)  I am using Coq version 8.1pl3.  We are trying to develop
a library on top of the FSets library that would hopefully be
compatible with Coq 8.1pl3.  But if that is not possible, I would at
least really hope there is a fix for this scenario in Coq 8.2.

In constructing the example, I observed that he problem is apparently
critically dependent on the fact that the relation "sim" is defined in
the argument to the functor.  This lead me to see that a rather simple
and elegant work-around: introduce new relation names in the functor
(defined as equal to those in the functor argument).  The solution is
given in the second code snippet.  As long as this methodology is
followed, it seems that functors and setoids might play well together
after all.  If "snippet1" doesn't automatically work in the next
version of Coq, then it would be extremely nice if the methodology of
"snippet2" is employed in Coq's libraries, assuming that no one sees
serious problems with it.

 - Aaron

<snippet1>

Require Import Setoid.
Require Import Arith.

Module Type S.
  Parameter t : Set.
  Parameter c : t.
  Parameter sim : t -> t -> Prop.
  Parameter sim_spec : forall a b : t,
    sim a b <-> (a = c <-> b = c).
  Parameter is_c : t -> Prop.
  Parameter is_c_spec : forall a :t,
    (is_c a) <-> a = c.
End S.

Module F (X : S).

  Definition ST : Setoid_Theory X.t X.sim.
  Proof.
    constructor.
    (* reflexivity *)
    intros x. rewrite X.sim_spec. intuition.
    (* symmetry *)
    intros x y H. rewrite X.sim_spec in *. intuition.
    (* transitivity *)
    intros x y z H1 H2. rewrite X.sim_spec in *.
     intuition.
  Qed.

  Add Setoid X.t X.sim ST as MySetoid.

  Add Morphism X.is_c with signature X.sim ==> iff as is_c_m.
  Proof.
    intros x y H. rewrite X.sim_spec in H.
     repeat rewrite X.is_c_spec. intuition.
  Qed.

End F.

Module M.
  Definition t := nat.
  Definition c := 0.
  Definition dec := eq_nat_dec 0.
  Definition sim a b := (a = c) <-> (b = c).
  Lemma sim_spec : forall a b : t,
    sim a b <-> (a = c <-> b = c).
  Proof.
    unfold sim. intuition.
  Qed.
  Inductive is_c' : t -> Prop :=
    is_c_1 : is_c' c.
  Definition is_c := is_c'.
  Lemma is_c_spec : forall a : t,
    is_c a <-> a = c.
  Proof.
    intros a. unfold is_c. split.
      intros H; inversion H; auto.
      intros H; subst; auto using is_c_1.
  Qed.
End M.

Module M1 := F M.

Lemma foo1 : forall a b,
  M.sim a b -> M.is_c a -> M.is_c b.
Proof.
  intros a b H1 H2. rewrite -> H1 in H2. assumption.
Qed.

Module M2 := F M.

Lemma foo2 : forall a b,
  M.sim a b -> M.is_c a -> M.is_c b.
Proof.
  intros a b H1 H2. rewrite -> H1 in H2. assumption.
Qed.

</snippet1>

<snippet2>

Require Import Setoid.
Require Import Arith.

Module Type S.
  Parameter t : Set.
  Parameter c : t.
  Parameter sim : t -> t -> Prop.
  Parameter sim_spec : forall a b : t,
    sim a b <-> (a = c <-> b = c).
  Parameter is_c : t -> Prop.
  Parameter is_c_spec : forall a :t,
    (is_c a) <-> a = c.
End S.

Module F (X : S).

  Definition sim := X.sim.
  Definition is_c := X.is_c.

  Definition ST : Setoid_Theory X.t sim.
  Proof.
    constructor.
    (* reflexivity *)
    intros x. rewrite X.sim_spec. intuition.
    (* symmetry *)
    intros x y H. rewrite X.sim_spec in *. intuition.
    (* transitivity *)
    intros x y z H1 H2. rewrite X.sim_spec in *.
     intuition.
  Qed.

  Add Setoid X.t sim ST as MySetoid.

  Add Morphism is_c with signature sim ==> iff as is_c_m.
  Proof.
    intros x y H. rewrite X.sim_spec in H.
     repeat rewrite X.is_c_spec. intuition.
  Qed.

End F.

Module M.
  Definition t := nat.
  Definition c := 0.
  Definition dec := eq_nat_dec 0.
  Definition sim a b := (a = c) <-> (b = c).
  Lemma sim_spec : forall a b : t,
    sim a b <-> (a = c <-> b = c).
  Proof.
    unfold sim. intuition.
  Qed.
  Inductive is_c' : t -> Prop :=
    is_c_1 : is_c' c.
  Definition is_c := is_c'.
  Lemma is_c_spec : forall a : t,
    is_c a <-> a = c.
  Proof.
    intros a. unfold is_c. split.
      intros H; inversion H; auto.
      intros H; subst; auto using is_c_1.
  Qed.
End M.

Module M1 := F M.

Lemma foo1 : forall a b,
  M.sim a b -> M.is_c a -> M.is_c b.
Proof.
  intros a b H1 H2.
  replace M.sim with M1.sim in * by reflexivity.
  replace M.is_c with M1.is_c in * by reflexivity.
  rewrite -> H1 in H2. assumption.
Qed.

Module M2 := M1.

Lemma foo2 : forall a b,
  M.sim a b -> M.is_c a -> M.is_c b.
Proof.
  intros a b H1 H2.
  replace M.sim with M1.sim in * by reflexivity.
  replace M.is_c with M1.is_c in * by reflexivity.
  rewrite -> H1 in H2. assumption.
Qed.

Lemma foo3 : forall a b,
  M.sim a b -> M.is_c a -> M.is_c b.
Proof.
  intros a b H1 H2.
  replace M.sim with M2.sim in * by reflexivity.
  replace M.is_c with M2.is_c in * by reflexivity.
  rewrite -> H1 in H2. assumption.
Qed.

</snippet2>

On Fri, Jun 6, 2008 at 2:32 PM, Pierre Letouzey
<Pierre.Letouzey AT pps.jussieu.fr>
 wrote:
> On Fri, Jun 06, 2008 at 10:51:33AM -0400, Aaron Bohannon wrote:
>> I tried something like that, but I don't understand how it can be made
>> to work.  Is there a way to write a signature for FSetFacts that
>> declares information about the setoid it defines?  Otherwise, the
>> client functor G will not be able to use rewriting in the setoid.  To
>> give a concrete example, how can I design G so that the rewriting
>> tactic in the proof will work, other than uncommenting the third line?
>>
>> Require Import FSets.
>> Module G (MyFSet : FSetInterface.S).
>>   (* Module MyFacts := FSetFacts.Facts MyFSet. *)
>>   Lemma foo : forall x y s,
>>     MyFSet.E.eq x y -> MyFSet.In x s -> MyFSet.In y s.
>>   Proof.
>>     intros x y s Heq H. rewrite -> Heq in H. assumption.
>>   Qed.
>> End G.
>>
>>  - Aaron
>>
>
>
> Hi Aaron, Hi Andrew,
>
> For the moment, I haven't managed yet to reproduce the issue you're
> mentioning. For instance, if I take the above code and duplicate the
> line about MyFacts into a MyFacts2 line, nothing strange happen on my
> machine, not even any warning. Could you please give me some code
> triggering the bug, as well as the exact coq version you're using (svn
> revision...)?
>
> In the meanwhile, I've killed in FSets one duplication of
> FSetFacts.WFacts instances that Aaron mentionned to my privately: in
> FSetProperties.WProperties, there's no need to create a new WFacts
> instance FM, since this module contains an instance Dec of
> FSetDecide.WDecide that itself contains an instance F of WFacts. So a
> simple FM:=Dec.F can replace the earlier FM:=WFacts E M (see svn
> commit 11064).
>
> This small change is far from ending this discussion, but it indicates
> at least that in many situations the duplication can be suppressed
> easily, especially if dependencies are linear (here WFacts --> WDecide
> --> WProperties). Of course, the duplication issue may remain in more
> complex situations (diamond dependencies, for instance). That's why we
> should investigate this problem with setoid rewrite and fix it. As
> far as I know, the earlier implementation of setoid rewrite was
> working in this situation (although it was generating tons of warning)
> and I don't see why the new version would not be able to do it as
> well.
>
> A last comment about your idea of using restrictive module types: it
> may be interesting as a quick workaround, but I doubt it can provide
> you more than that. Anyway, if you're looking for a way to declare a
> setoid relation and morphisms in a module type, you can have a look at
> theories/Numbers/NatInt/NZAxioms.v in a recent coq svn archive.
>
> Best regards,
> Pierre Letouzey
>
>
>
>
>