The Coq mailing list

[Ben Horsfall <ben.horsfall AT gmail.com>]

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.