Welcome to Coq 8.1pl2 (Oct. 2007)

Coq < Section test_ensemble.

(* Load library involving basic theory of subsets of a fixed
underlying type U (or set). These subsets are called called
"ensembles". Check out the link Standard Library on the Coq
home page. *)

Coq < Require Import Coq.Sets.Constructive_sets.

Coq < Variable U:Set.  (* The underlying set *)
U is assumed

Coq < Variable A B: (Ensemble U). (* Two subsets of U are declared. *)
A is assumed
B is assumed

Coq < Print Ensemble.
Ensemble = fun U : Type => U -> Prop
     : Type -> Type


Argument scope is [type_scope]



Coq < Theorem Int2 : (Included U (Intersection U  A B) (Intersection U B A)).
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  ============================
   Included U (Intersection U A B) (Intersection U B A)

Int2 < intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  ============================
   Included U (Intersection U A B) (Intersection U B A)

Int2 < red.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  ============================
   forall x : U, In U (Intersection U A B) x -> In U (Intersection U B A) x

Int2 < intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  H : In U (Intersection U A B) x
  ============================
   In U (Intersection U B A) x

(* Intersection is defined as an inductive family, so elim H is an
applicable tactic. *)

Int2 < elim H.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  H : In U (Intersection U A B) x
  ============================
   forall x0 : U, In U A x0 -> In U B x0 -> In U (Intersection U B A) x0

Int2 < intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  H : In U (Intersection U A B) x
  x0 : U
  H0 : In U A x0
  H1 : In U B x0
  ============================
   In U (Intersection U B A) x0

(* To prove the goal we can prove the subgoals
   In U B x0  and  In U A x0 . *)

Int2 < split.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  H : In U (Intersection U A B) x
  x0 : U
  H0 : In U A x0
  H1 : In U B x0
  ============================
   In U B x0

subgoal 2 is:
 In U A x0

Int2 < assumption.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  H : In U (Intersection U A B) x
  x0 : U
  H0 : In U A x0
  H1 : In U B x0
  ============================
   In U A x0

Int2 < assumption.
Proof completed.

Int2 < Qed.
intros.
intros.
red in |- *.
intros.
elim H.
intros.
split.
 assumption.
assumption.
Int2 is defined


 (* We show  now that A - {x, y} is always included in 
 the intersection of (A - {x}) and (B - {y}). *)

Coq < Theorem Subt2: (forall x y: U,
      Included U (Setminus U A (Couple U x y))
                 (Intersection U
                       (Setminus U A (Singleton U x))
                       (Setminus U A (Singleton U y)))).
Subt2 <

intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  ============================
   Included U (Setminus U A (Couple U x y))
     (Intersection U (Setminus U A (Singleton U x))
        (Setminus U A (Singleton U y)))

< red in |- *; intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U
     (Intersection U (Setminus U A (Singleton U x))
        (Setminus U A (Singleton U y))) x0

< split.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U (Setminus U A (Singleton U x)) x0

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<  red in |- *; red in |- *.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0 /\ ~ In U (Singleton U x) x0

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<   split.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0

subgoal 2 is:
 ~ In U (Singleton U x) x0
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<  red in |- *.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   A x0

subgoal 2 is:
 ~ In U (Singleton U x) x0
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<    elim H.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0 -> ~ In U (Couple U x y) x0 -> A x0

subgoal 2 is:
 ~ In U (Singleton U x) x0
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<    intros; assumption.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   ~ In U (Singleton U x) x0

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

< elim H.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0 -> ~ In U (Couple U x y) x0 -> ~ In U (Singleton U x) x0

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<   intros.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  ============================
   ~ In U (Singleton U x) x0

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<   red in |- *.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  ============================
   In U (Singleton U x) x0 -> False

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<   intro.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U x) x0
  ============================
   False

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<   assert (In U (Couple U x y) x0).
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U x) x0
  ============================
   In U (Couple U x y) x0

subgoal 2 is:
 False
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<  red in |- *.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U x) x0
  ============================
   Couple U x y x0

subgoal 2 is:
 False
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<    unfold In in H2.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : Singleton U x x0
  ============================
   Couple U x y x0

subgoal 2 is:
 False
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<    elim H2.
3 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : Singleton U x x0
  ============================
   Couple U x y x

subgoal 2 is:
 False
subgoal 3 is:
 In U (Setminus U A (Singleton U y)) x0

<    left.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U x) x0
  H3 : In U (Couple U x y) x0
  ============================
   False

subgoal 2 is:
 In U (Setminus U A (Singleton U y)) x0

<  contradiction.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U (Setminus U A (Singleton U y)) x0

< red in |- *; split.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0

subgoal 2 is:
 ~ In U (Singleton U y) x0

< elim H.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0 -> ~ In U (Couple U x y) x0 -> In U A x0

subgoal 2 is:
 ~ In U (Singleton U y) x0

<   intros; assumption.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   ~ In U (Singleton U y) x0

< elim H.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  ============================
   In U A x0 -> ~ In U (Couple U x y) x0 -> ~ In U (Singleton U y) x0

<  intros.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  ============================
   ~ In U (Singleton U y) x0

<  intro.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U y) x0
  ============================
   False

<  assert (In U (Couple U x y) x0).
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U y) x0
  ============================
   In U (Couple U x y) x0

subgoal 2 is:
 False

< red in |- *.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U y) x0
  ============================
   Couple U x y x0

subgoal 2 is:
 False

<   unfold In in H2.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : Singleton U y x0
  ============================
   Couple U x y x0

subgoal 2 is:
 False

<   elim H2.
2 subgoals

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : Singleton U y x0
  ============================
   Couple U x y y

subgoal 2 is:
 False

<   right.
1 subgoal

  U : Set
  A : Ensemble U
  B : Ensemble U
  x : U
  y : U
  x0 : U
  H : In U (Setminus U A (Couple U x y)) x0
  H0 : In U A x0
  H1 : ~ In U (Couple U x y) x0
  H2 : In U (Singleton U y) x0
  H3 : In U (Couple U x y) x0
  ============================
   False

Subt2 <  contradiction.
Proof completed.