The Coq mailing list

[James McKinna <james.mckinna AT cs.ru.nl>]

Ben Horsfall 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.
>   

Ben,

I think Arnaud's answer nails it, but for more details (and historical 
interest), please see the attached LEGO file from 1992.

The concept you are after is in Paul Cohn's "Universal Algebra" (1965), 
the idea of an *intersection-closed* family of sets:

F is intersection-closed iff forall G \subseteq F, F(\bigcap G)

(so trivially, F(\bigcap F)). IC-families have nice closure properties, 
but for most applications in CS, the observation that for monotone phi, 
the family

fn C => phi C \subseteq C

is IC, is pretty much all you need for Knaster-Tarski and related 
results (intersections of jointly commutative families of monotone 
operators, a la Andrews 1973).

Cheers,

James McKinna
> 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.
>
>
>
>