The Coq mailing list

["Damien Ledoux" <dam.ledoux AT gmail.com>]

Hi David,


Require Import Ensembles.

Definition def_A : Ensemble nat :=
  let e1 := Add nat (Empty_set nat) 2 in
  Add nat e1 3.

Definition def_B : Ensemble nat :=
  let e1 := Add nat (Empty_set nat) 2 in
  let e2 := Add nat e1 3 in
  let e3 := Add nat e2 4 in
  Add nat e3 5.

Definition def_C : Ensemble nat :=
  let e1 := Add nat (Empty_set nat) 2 in
  Add nat e1 3.

Definition def_D : Ensemble nat := Intersection nat def_A def_B.

Lemma not_included_empty_Inhabited :
 forall (A B C D : Ensemble nat),
   A = def_A ->
   B = def_B ->
   C = def_C ->
   D = def_D ->
   C = D.
Proof.
  intros A B C D.
  intros.
  apply Extensionality_Ensembles.
  red.
  rewrite H1.
  rewrite H2.
  split.
  red.
  intros x H'.
  red.
  red.
  apply Intersection_intro.
  unfold def_C in H'.
  unfold def_A.
  auto.
  unfold def_B.
  unfold def_C in H'.
  red in H'.
  red.
  red.
  apply Union_introl.
  red.
  red.
  apply Union_introl.
  red.
  auto.
  red.
  intros x H'.
  red in H'.
  red in H'.
  inversion_clear H'.
  red.
  red.
  red in H3.
  red in H3.
  auto.
Qed.

bye.
Damien


Le Thu, 24 Aug 2006 19:34:52 +0200, David de Villiers  
<davidc1 AT ananzi.co.za> a �crit:

> Hi all,
> Can anyone help with the solution of the following problem?
> Suppose:
> A={2,3}
> B={2,3,4,5}
> C={2,3}
> D=Aâ?©B (D is the intersection of A and B).
> Prove that C=D.
> Ciao,
> David.
>
> Sign up for Ananzi Mail Plus and you receive a larger mailbox, POP3  
> access, RPOP and much more. So sign up now, from just R 8,29 per month.
>
> http://www.swiftsms.co.za/swiftT/track.asp?e=*em*&cid=113&u=8&tid=1138
>
>
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club