The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Thu, Aug 24, 2006 at 07:34:52PM +0200, David de Villiers wrote:
> Hi all,
> Can anyone help with the solution of the following problem?
> Suppose:
> A={2,3}
> B={2,3,4,5}
> C={2,3}
> D=A∩B (D is the intersection of A and B).
> Prove that C=D.
> Ciao,
> David.
> 

Hi 

As explained in the answer by Damien Ledoux, one solution is indeed to
use the Ensemble structure to represent a set. But as this
representation is based on Coq relations ( Ensemble = Domain -> Prop),
you will have to reason on such sets by hand, as in Damien's proof,
or develop your own tactic. Almost nothing can be _computed_ about
such sets (e.g. no cardinal _function_). 

At first look, this representation seems cool nonetheless since you can 
use Coq's default equality on them, and really write and prove C=D. 
But this is possible only thanks to an axiom hidden inside Ensemble.v : 

Axiom Extensionality_Ensembles : forall A B:Ensemble, Same_set A B -> A = B.

Said otherwise: sets with similar elements are equal. Nothing wrong in this, 
just check that you don't end with a nasty combination of axioms (see Coq 
FAQ). 
That was just to say that concerning sets, nothing comes for free. 


As I explained in my previous mail, the alternative approach is to use
a computational structure such as lists or whatever. I personnally
recommend using the new FSets library that provides an abstraction
layer with respect to which actual implementation is chosen at the low
level (ordered lists, AVL trees, etc).

Then, if you follow this approach, equality is a delicate issue. Think
of sets-as-lists: 1::2::nil is not Coq-equal to 2::1::nil, but they
both represent the same set. In FSets, even if we choose a unique
representation such as ordered lists, then we have to attach some
proof to every sets (e.g. to certify that the list is sorted). That's
why using Coq equality on FSets sets is pointless. Instead, a relation
Equal is provided (and even a function equal : set -> set -> bool),
that mean that both sets contain the same elements. And thanks to
coq's setoids, you can use this Equal predicate (almost) as the usual
equality, and in particular do some rewriting. 

Below is a solution to your question using FSets (needs Coq 8.1beta). 

Best regards, 
Pierre Letouzey

---------------------------------------------------------------------

(* Let's use fast integers. *)
Require Import ZArith.
Open Scope Z_scope.

(* Some examples of ordered types, including Z *)
Require OrderedTypeEx.
(* One implementation of finite sets over an ordered type, based on lists *)
Require FSetList.
(* Other possibility: FSetAVL, heavier for Coq but more efficient *)

(* We combine the two in a specialized module for sets of integers *)
Module IntSet := FSetList.Make(OrderedTypeEx.Z_as_OT).
Import IntSet.
(* To have a rough idea of what's available in this IntSet: *)
Print IntSet.

(* Your set: *)
Definition A := add 2 (add 3 empty).

(* Idem, with a nice notation: *)
Infix "++" := add (at level 30, right associativity).
Definition B := 2++3++4++5++empty.
Definition C := 2++3++empty.

Definition D := inter A B.


(* As explained in the mail, Coq equality = isn't meaningful on such sets *)
(* Rather use the provided Equal relation and equal function *)
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).

Lemma C_eq_D : C [=] D.
Proof.
apply equal_2. (* change the Equal problem into an equal problem *)
compute; trivial. (* to solve a concrete equal problem, just compute! *)
Qed.


(* Here we show that Equal can be declared as a setoid equality, 
   and hence can be used for doing some rewriting. *)

Require FSetFacts.
Module SomeFacts := FSetFacts.Facts IntSet.

Lemma test_rewrite : union B (inter A D) [=] B.
Proof.
rewrite <- C_eq_D.
apply equal_2; auto.
Qed.