The Coq mailing list

[Tillmann Rendel <rendel AT cs.au.dk>]

Hi Ian,

Ian Lynagh wrote:
> As part of a larger proof, I needed to show that adding A then B to a
> set is the same as adding B then A to the set (with some extra
> equalities floating round). This feels like there should be a 1-line
> solution, but I couldn't find one. I've extracted what I did as a
> standalone proof below, and I was wondering if anyone could tell me how
> I can do it more simply, please?

This is provided as lemma add_add in library FSetProperties. Just 
instantiate the WProperties functor for your particular FSet. This seems 
to register NameSet.Equal as an equivalence relation, so you can just do 
the following:

    Require Import FSetProperties.
    Module NameSetProperties := WProperties(NameSet).

    Lemma Foo : forall (o oa oab : NameSet.t) (a b : Name),
      NameSet.Equal oa (NameSet.add a o) ->
      NameSet.Equal oab (NameSet.add b oa) ->
      NameSet.Equal oab (NameSet.add a (NameSet.add b o)).
    Proof.
      intros ? ? ? ? ? H1 H2.
      rewrite H2, H1.
      auto with set.
    Qed.

However, it is even easier to instantiate the WDecide functor from 
library FSetDecide for your particular FSet, and use the tactic fsetdec.

    Require Import FSetDecide.
    Module NameSetDec := WDecide (NameSet).

    Lemma Foo : forall (o oa oab : NameSet.t) (a b : Name),
      NameSet.Equal oa (NameSet.add a o) ->
      NameSet.Equal oab (NameSet.add b oa) ->
      NameSet.Equal oab (NameSet.add a (NameSet.add b o)).
    Proof.
      NameSetDec.fsetdec.
    Qed.

I am not sure whether that is the supposed usage of the FSet libraries. 
I am missing a design document for the standard library which tells me 
how it is supposed to be used, something like [1] for Java collections.

  Tillmann

[1] http://java.sun.com/javase/6/docs/technotes/guides/collections/