The Coq mailing list

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

Hi,

I just saw this topic, which is something that has also been of
interest to me.  I am doing a large development with many datatypes,
some of whose constructors take FSets/FMaps as arguments.  I wanted to
be able to ensure that I could use the "setoid_rewrite" and such
tactics, as defined in the "SetoidTactics" module, to rewrite FMaps in
my datatypes, and that the Setoid equality on my FMaps would be
automatically derived in the natural way from the Setoid equality on
the range type of the FMaps.

I was not really sure whether I could get type-classes and modules
working together in this way.  Also, all of the Setoid-related code
seems to be lacking documentation and examples and is therefore very
confusing.  So it took me quite some time to figure out, but I did
seem to get it all working.  I also wrote generic code for lifting
Setoid equivalences over the basic type constructors (sum, prod,
option, list, etc).  It does seem like all of this should be code that
belongs in the standard library.

Unfortunately, I do not have time to polish up my code for mass
consumption right now (my name choices may not be ideal; my code may
not be as complete as it shoud be; my code loosely depends on some
custom tactics; etc).  But if someone is very interested in it, I
would be willing to send what I have privately...especially if they
are willing to help me refine and polish it!

 - Aaron

P.S. One hidden gotcha that has nothing to do with FSets/FMaps is
that, in order to get setoid rewriting working in the way you expect,
you have to do this:

Instance Setoid_DefaultRelation {A: Type} {S: Setoid A}: DefaultRelation 
equiv.

I am not sure why the DefaultRelation class exists at all or why this
instance declaration does appear in the standard library.  After all,
to declare a type as an instance of Setoid literally means to
associate it with a default equivalence relation.  Why would I want
another level of indirection?  As I said, the Setoid code in the
standard library is confusing.

On Fri, Jan 28, 2011 at 4:19 AM, AUGER Cedric 
<Cedric.Auger AT lri.fr>
 wrote:
> Le Fri, 28 Jan 2011 08:58:06 +0800,
> Frederic Blanqui 
> <frederic.blanqui AT inria.fr>
>  a écrit :
>
>> Thank you very much Cedric! But it would be nice that your code be
>> included in the standard lib. Frederic.
>
> Maybe, but it won't be tomorrow! I believe the Coq devellopers in
> particular (P. Letouzey) want to rewrite the Set/Map modules.
> And S. Lescuyer containers may also be added before.
> Eventually, if we add this code, we should add a many other lemmas
> (for delete, union, intersection, same thing for equality, inclusion,
> dijunction and so on), which may make the signature of the interface
> quite big, and probably needless for most usages.
>
> So if you think it is a good thing, you can try to complete it and send
> it as a contribution.
>
>> Le 28/01/2011 02:24, AUGER Cedric a écrit :
>> > Le Thu, 27 Jan 2011 22:48:01 +0800,
>> > Frederic 
>> > Blanqui<frederic.blanqui AT inria.fr>
>> >   a écrit :
>> >
>> >> Hello Cedric.
>> >>
>> >> I guess that for having M=M', you assume that the equality on A is
>> >> also = (Leibniz equality). But what if the equality on A is an
>> >> arbitrary equivalence relation?...
>> > Of course I assume that (else Coq would probably be inconsistant).
>> >
>> > Else you can try to complete the following code for your purpouse;
>> > it is a functor which will add some lemmas you want.
>> >
>> > I may have bad tastes for notations (particulary in using UTF8 even
>> > if people are used to ascii); for people who would like to have
>> > easy ways to input them and are using an X window system, I advise
>> > them to take a look at XCompose; for the others they can try some
>> > input method (such as uim; or some provided by emacs if they use
>> > proof general) Require Import FMapInterface.
>> > Require Import Utf8_core.
>> > Set Implicit Arguments.
>> >
>> > Notation "⊤" := (True).
>> > Notation "⊥" := (False).
>> >
>> > (* Abstraction *)
>> > Notation "'λ'  x .. y · t" := (fun x =>  .. (fun y =>  t) ..)
>> >    (at level 200, x binder, y binder, right associativity).
>> >
>> > Delimit Scope init_scope with init.
>> > Open Scope init_scope.
>> > Notation "'ℕ'" := nat: init_scope.
>> > Notation "'𝟘'" := Empty_set: init_scope.
>> > Notation "'𝟙'" := unit: init_scope.
>> > Notation "'𝟚'" := bool: init_scope.
>> > Notation "'𝕠'" := tt: init_scope.
>> > Notation "'𝕥'" := true: init_scope.
>> > Notation "'𝕗'" := false: init_scope.
>> > Notation "x ₁" := (let (y, _) := x in y) (at level 5).
>> > Notation "x ₂" := (let (_, y) := x in y) (at level 5).
>> >
>> > Module MapEquiv (M: S).
>> >   Definition elt_equiv A (elt_eq: A → A → 𝟚): relation A :=
>> >              λ x y·elt_eq x y = 𝕥.
>> >   Lemma t_morphism:
>> >   ∀ A elt_eq, equivalence A (elt_equiv elt_eq) →
>> >               equivalence (M.t A) (M.Equivb elt_eq).
>> >    Proof.
>> >    intros A elt_eq [Refl Trans Sym]; split.
>> >      intro m; split.
>> >       now split; auto.
>> >      intros k e e' H H'.
>> >      generalize (M.find_1 H').
>> >      rewrite (M.find_1 H).
>> >      intro Heq; inversion_clear Heq.
>> >      exact (Refl e').
>> >     intros m1 m2 m3 [H12 K12] [H23 K23]; split; intro.
>> >      generalize (H23 k); generalize (H12 k); clear.
>> >      now intros [] []; split; auto.
>> >     intros e e' H H'.
>> >     destruct ((H12 k)₁ (ex_intro (λ _ · _) e H)) as [e_ He_].
>> >     generalize (Trans e e_ e').
>> >     generalize (K23 _ _ _ He_ H').
>> >     generalize (K12 _ _ _ H He_).
>> >     clear; unfold Cmp, elt_equiv.
>> >     now auto.
>> >    intros m1 m2 [K H]; split.
>> >     intro k; split; intro L.
>> >      exact ((K k)₂ L).
>> >     exact ((K k)₁ L).
>> >    intros k e e' H1 H2.
>> >    generalize (Sym e' e).
>> >    generalize (H _ _ _ H2 H1).
>> >    clear; unfold Cmp, elt_equiv.
>> >    now auto.
>> >   Qed.
>> >
>> >   Instance add_m : ∀ A elt_eq,
>> >   Proper (M.E.eq ==>
>> >           elt_equiv elt_eq ==>
>> >           M.Equiv (elt_equiv elt_eq) ==>
>> >           M.Equiv (elt_equiv elt_eq))
>> >   (@M.add A).
>> >    Proof.
>> >    intros A elt_eq k1 k2 Hk e1 e2 He m1 m2 Hm.
>> >    split.
>> >     intro k.
>> >     generalize (Hm ₁ k); clear -Hm Hk.
>> >     intros [Hm1 Hm2]; split; intros [a_ Ha_].
>> >      destruct (M.E.eq_dec k2 k).
>> >       split with e2.
>> >       now apply M.add_1.
>> >      destruct Hm1.
>> >       split with a_.
>> >       apply M.add_3 with k1 e1; auto.
>> >       intro H; destruct n.
>> >       now apply M.E.eq_trans with k1; auto.
>> >      split with x.
>> >      now apply M.add_2; auto.
>> >     destruct (M.E.eq_dec k1 k).
>> >      split with e1.
>> >      now apply M.add_1.
>> >     destruct Hm2.
>> >      split with a_.
>> >      apply M.add_3 with k2 e2; auto.
>> >      intro H; destruct n.
>> >      now apply M.E.eq_trans with k2; auto.
>> >     split with x.
>> >     now apply M.add_2; auto.
>> >    intro k.
>> >    destruct (M.E.eq_dec k2 k).
>> >     intros e_ e_' H H'.
>> >     revert He.
>> >     generalize (M.find_1 H').
>> >     rewrite (M.find_1 (M.add_1 _ _ e)).
>> >     generalize (M.find_1 H).
>> >     rewrite (M.find_1 (M.add_1 _ _ (M.E.eq_trans Hk e))).
>> >     clear.
>> >     intro H; inversion_clear H.
>> >     intro H; inversion_clear H.
>> >     now auto.
>> >    intros e_ e_' H H'.
>> >    generalize (M.add_3 n H').
>> >    cut (¬M.E.eq k1 k).
>> >     intro n'; generalize (M.add_3 n' H).
>> >     exact (Hm ₂ k e_ e_').
>> >    clear -n Hk.
>> >    intro H; destruct n.
>> >    now apply M.E.eq_trans with k1; auto.
>> >   Qed.
>> >   End MapEquiv.
>
>
>