The Coq mailing list

[Alexandre Pilkiewicz <alexandre.pilkiewicz AT polytechnique.org>]

Hi Ben,

There is a good reason why you can't prove it: it's False !

Take the set of all the sets of integers bigger than a given n
(the set containing  {m:nat| n < m} for all n)

This set is closed under finite intersection (take the max of the n),
but the global intersection is empty!

Please find below the proof script leading to False.

Cheers,
Alexandre



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.



(* let's find a contradiction *)

Definition nats_biger_than (n:nat) : Ensemble nat :=
  fun m => n < m.

Definition all_nats_biger_than: Ensemble (Ensemble nat) :=
  fun E => exists n, forall m, E m <-> nats_biger_than n m.

Require Import MinMax.
Require Import Omega.
Lemma all_nats_biger_than_closed: closed_under_intersection 
all_nats_biger_than.
Proof.
  unfold closed_under_intersection.
  unfold In. unfold all_nats_biger_than.
  intros U V [nU HU] [nV HV].
  exists (max nU nV).
  intros m. specialize (HU m). specialize (HV m).
  destruct HU. destruct HV.
  unfold nats_biger_than in *.
  split.

  intro INTER; destruct INTER. unfold In in *.
  destruct (max_spec nU nV); intuition.

  intros. constructor; unfold In; destruct (max_spec nU nV); intuition.
Qed.

Goal False.
  pose proof (closed_under_intersection_least all_nats_biger_than
all_nats_biger_than_closed).
  destruct H as [U [IN H]].
  unfold Included, In, all_nats_biger_than, nats_biger_than in *.
  destruct IN as [n IN].
  specialize (H (nats_biger_than (S n))).
  match type of H with
    | ?X -> _ => assert X as H0; [|specialize (H H0); clear H0]
  end.
  exists (S n). intros. unfold nats_biger_than. tauto.
  specialize (H (S n)). unfold nats_biger_than in *.
  assert (U (S n)).
  rewrite IN. omega.

  specialize (H H0). omega.
Qed.