The Coq mailing list

[Edsko de Vries <devriese AT cs.tcd.ie>]

Hi,

Thanks for all the help on merge and finite sets! I have now defined a
commutative associative 'union' operation on lists which has the
following properties:

Lemma in_union_l1 : forall l1 l2 a,
  In a l1 -> In a (union l1 l2).

Lemma in_union_l2 : forall l1 l2 a,
  In a l2 -> In a (union l1 l2).

Lemma in_union_inv : forall l1 l2 a,
  In a (union l1 l2) -> In a l1 \/ In a l2.

Lemma union_length : forall l1 l2,
  length (union l1 l2) = length l1 + length l2.

Lemma union_comm : forall l1 l2,
  union l1 l2 = union l2 l1.

Lemma union_assoc : forall l1 l2 l3,
  union l1 (union l2 l3) = union (union l1 l2) l3.

(Context: I am working on a formalization of a substructural type system using
the formal binders library developed by Arthur Chargueraud and Brian Aydemir;
I'm using this 'union' operator to combine environments (the "&" symbol in the
formal binders library) so that I get the "Exchange" rule for free, which is
extremely convenient.)

(I am this definition to combine typing environments in a formalization
of a substructural type system, so that I don't have to worry about
"Exchange")

Module can be downloaded form http://www.cs.tcd.ie/~devriese/coq

Edsko