The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Well, being closed under binary intersection doesn't imply closed under arbitrary intersection in general. You might want to phrase your closure property in term of an arbitrary VS included in US. Then it should be easy.


Arnaud Spiwack

On 7 December 2011 04:58, Ben Horsfall <ben.horsfall AT gmail.com> wrote:

I've been trying to prove something which ought to be able to be done by a straightforward induction: that if a set of sets is closed under intersection, then it has a least element (under ordering by set inclusion), viz. the intersection of all of its elements. I have tried *many* variations, including (co)inductive ones -- a simple non-inductive formulation is below. It's easy to show that the intersection of all elements is included in every element, but I can't show that it is an element. From a practical point of view, I can't see how to define the generalized intersection in such a way that it can be unified with an Intersection term.

I'm sure I have a blind spot here. Any advice would be appreciated.

Ben


Require Export Coq.Sets.Ensembles.

Definition intersections {A} (US : Ensemble (Ensemble A)) : Ensemble A :=
 fun (x : A) => forall U : Ensemble A, In (Ensemble A) US U -> In A U x.

Definition closed_under_intersection {A} (US : Ensemble (Ensemble A)) : Prop :=
 forall U V : Ensemble A,
 In (Ensemble A) US U -> In (Ensemble A) US V ->
 In (Ensemble A) US (Intersection A U V).

Lemma closed_under_intersection_least :
 forall {A} (US : Ensemble (Ensemble A)),
 closed_under_intersection US ->
 exists X, In (Ensemble A) US X /\
 forall Y, In (Ensemble A) US Y -> Included A X Y.
Proof.
 intros. exists (intersections US). split.
 admit.  (**** In (Ensemble A) US (intersections US) ****)
 intros. unfold Included. intros. apply H1. apply H0.
Qed.