(* This program is free software; you can redistribute it and/or      *)
(* modify it under the terms of the GNU Lesser General Public License *)
(* as published by the Free Software Foundation; either version 2.1   *)
(* of the License, or (at your option) any later version.             *)
(*                                                                    *)
(* This program is distributed in the hope that it will be useful,    *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of     *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the      *)
(* GNU General Public License for more details.                       *)
(*                                                                    *)
(* You should have received a copy of the GNU Lesser General Public   *)
(* License along with this program; if not, write to the Free         *)
(* Software Foundation, Inc., 51 Franklin St, Fifth Floor, Boston, MA *)
(* 02110-1301 USA                                                     *)


Set Implicit Arguments.
Unset Strict Implicit.
Require Export Fpart2.
Section tiroirs_def.
Variable E F : Setoid.
Variable f : MAP E F.

Lemma diff_add_part2 :
 forall (E : Setoid) (A : part_set E) (x : E),
 in_part x A -> Equal A (add_part (diff A (single x)) x).
(* Goal: forall (E : Setoid) (A : Carrier (part_set E)) (x : Carrier E) (_ : @in_part E x A), @Equal (part_set E) A (@add_part E (@diff E A (@single E x)) x) *)
intros E0 A x H'; try assumption.
(* Goal: @Equal (part_set E0) A (@add_part E0 (@diff E0 A (@single E0 x)) x) *)
apply in_eq_part.
(* Goal: forall (x0 : Carrier E0) (_ : @in_part E0 x0 (@add_part E0 (@diff E0 A (@single E0 x)) x)), @in_part E0 x0 A *)
intros x0 H'0; try assumption.
(* Goal: @in_part E0 x0 A *)
elim (classic (Equal x x0)); intros.
(* Goal: @in_part E x1 (@single E x) *)
(* Goal: not (@in_part E x1 (@single E x)) *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply in_part_trans_eq with x; auto with *.
(* Goal: @in_part E0 x0 A *)
cut (in_part x0 (diff A (single x))).
(* Goal: forall _ : @in_part E0 x0 (@diff E0 A (@single E0 x)), @in_part E0 x0 (@add_part E0 (@diff E0 A (@single E0 x)) x) *)
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
(* Goal: forall (x0 : Carrier E0) (_ : @in_part E0 x0 (@add_part E0 (@diff E0 A (@single E0 x)) x)), @in_part E0 x0 A *)
unfold add_part in |- *; auto with *.
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
(* Goal: forall (x0 : Carrier E0) (_ : @in_part E0 x0 (@add_part E0 (@diff E0 A (@single E0 x)) x)), @in_part E0 x0 A *)
apply in_diff; auto with *.
(* Goal: forall (x0 : Carrier E0) (_ : @in_part E0 x0 (@add_part E0 (@diff E0 A (@single E0 x)) x)), @in_part E0 x0 A *)
intros x0 H'0; try assumption.
(* Goal: @in_part E0 x0 A *)
elim (classic (Equal x x0)); intros.
(* Goal: @in_part E x1 (@single E x) *)
(* Goal: not (@in_part E x1 (@single E x)) *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply in_part_trans_eq with x; auto with *.
(* Goal: @in_part E0 x0 A *)
cut (in_part x0 (diff A (single x))).
(* Goal: forall _ : @in_part E0 x0 (@diff E0 A (@single E0 x)), @in_part E0 x0 A *)
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
intros H'1; try assumption.
(* Goal: @in_part E0 x0 A *)
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
apply diff_in_l with (single x).
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
unfold add_part in H'0.
(* Goal: @in_part E0 x0 (@diff E0 A (@single E0 x)) *)
elim (in_part_union H'0); intros.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
absurd (Equal x x0); auto with *.
Qed.
Hint Resolve diff_add_part2: algebra.

Lemma cardinal_minus_part :
 forall (B : part_set F) (x : F) (n : nat),
 cardinal B (S n) -> in_part x B -> cardinal (diff B (single x)) n.
(* Goal: forall (B : Carrier (part_set F)) (x : Carrier F) (n : nat) (_ : @cardinal F B (S n)) (_ : @in_part F x B), @cardinal F (@diff F B (@single F x)) n *)
intros B x n H' H'0; try assumption.
(* Goal: @eq nat (S n2) (S n2) *)
apply cardinal_S with B x; auto with *.
(* Goal: not (@in_part F (@Ap E F f x1) (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
unfold not in |- *; intros.
(* Goal: False *)
cut (~ in_part x (single x)).
(* Goal: @eq nat (S n2) (S n2) *)
unfold not in |- *; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply diff_in_r with B; auto with *.
Qed.
Hint Resolve cardinal_minus_part: algebra.

Lemma tiroirs :
 forall (n : nat) (Chaussettes : part_set E),
 cardinal Chaussettes n ->
 forall (m : nat) (Tiroirs : part_set F),
 cardinal Tiroirs m ->
 m < n ->
 (forall x : E, in_part x Chaussettes -> in_part (f x) Tiroirs) ->
 exists x : E, (exists y : E, ~ Equal x y /\ Equal (f x) (f y)).
(* Goal: forall (n : nat) (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes n) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m n) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
simple induction n.
(* Goal: forall (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes O) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m O) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
(* Goal: forall (n : nat) (_ : forall (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes n) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m n) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y))))) (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes (S n)) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m (S n)) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
intros Chaussettes H' m Tiroirs H'0 H'1; try assumption.
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
inversion H'1.
(* Goal: forall (n : nat) (_ : forall (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes n) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m n) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y))))) (Chaussettes : Carrier (part_set E)) (_ : @cardinal E Chaussettes (S n)) (m : nat) (Tiroirs : Carrier (part_set F)) (_ : @cardinal F Tiroirs m) (_ : lt m (S n)) (_ : forall (x : Carrier E) (_ : @in_part E x Chaussettes), @in_part F (@Ap E F f x) Tiroirs), @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
intros n0 H' Chaussettes H'0 m Tiroirs H'1 H'2 H'3; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
inversion H'0.
elim (classic (ex (fun y : E => ~ Equal x y /\ Equal (Ap f x) (Ap f y))));
 intros.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
exists x; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
cut (exists m0 : nat, m = S m0).
(* Goal: forall _ : @in_part F (@Ap E F f x) Tiroirs, @ex nat (fun m0 : nat => @eq nat O (S m0)) *)
(* Goal: @in_part F (@Ap E F f x) Tiroirs *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (S n2) (S m0)) *)
intros H'4; try assumption.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
case H'4; clear H'4; intros.
(* Goal: @ex (Carrier E) (fun x : Carrier E => @ex (Carrier E) (fun y : Carrier E => and (not (@Equal E x y)) (@Equal F (@Ap E F f x) (@Ap E F f y)))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply H' with (diff Chaussettes (single x)) x0 (diff Tiroirs (single (f x))).
(* Goal: @cardinal E (@diff E Chaussettes (@single E x)) n0 *)
(* Goal: @cardinal F (@diff F Tiroirs (@single F (@Ap E F f x))) x0 *)
(* Goal: lt x0 n0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (@diff E Chaussettes (@single E x))), @in_part F (@Ap E F f x0) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply cardinal_S with Chaussettes x.
(* Goal: not (@in_part F (@Ap E F f x1) (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
unfold not in |- *; intros.
(* Goal: @eq nat (S n2) (S n2) *)
absurd (~ in_part x (single x)); auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply diff_in_r with Chaussettes; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @Equal (part_set E) Chaussettes (@add_part E (@diff E Chaussettes (@single E x)) x) *)
(* Goal: @cardinal E Chaussettes (S n0) *)
(* Goal: @cardinal F (@diff F Tiroirs (@single F (@Ap E F f x))) x0 *)
(* Goal: lt x0 n0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (@diff E Chaussettes (@single E x))), @in_part F (@Ap E F f x0) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply diff_add_part2.
(* Goal: @eq nat (S n2) (S n2) *)
apply in_part_comp_r with (add_part B x); auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @cardinal F (@diff F Tiroirs (@single F (@Ap E F f x))) x0 *)
(* Goal: lt x0 n0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (@diff E Chaussettes (@single E x))), @in_part F (@Ap E F f x0) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply cardinal_minus_part.
(* Goal: @eq nat (S n2) (S n2) *)
rewrite <- H5; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply H'3; auto with *.
(* Goal: @in_part E x Chaussettes *)
(* Goal: lt x0 n0 *)
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (@diff E Chaussettes (@single E x))), @in_part F (@Ap E F f x0) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply in_part_comp_r with (add_part B x).
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
rewrite H5 in H'2; auto with *.
(* Goal: forall (x0 : Carrier E) (_ : @in_part E x0 (@diff E Chaussettes (@single E x))), @in_part F (@Ap E F f x0) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
intros x1 H'4; try assumption.
(* Goal: @in_part F (@Ap E F f x1) (@diff F Tiroirs (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply in_diff.
(* Goal: @eq nat (S n2) (S n2) *)
apply H'3; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply diff_in_l with (single x); auto with *.
(* Goal: not (@in_part F (@Ap E F f x1) (@single F (@Ap E F f x))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
unfold not in |- *; intros.
(* Goal: False *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
unfold not in H4.
(* Goal: False *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply H4.
(* Goal: @ex (Carrier E) (fun y : Carrier E => and (forall _ : @Equal E x y, False) (@Equal F (@Ap E F f x) (@Ap E F f y))) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
exists x1; try assumption.
(* Goal: and (forall _ : @Equal E x x1, False) (@Equal F (@Ap E F f x) (@Ap E F f x1)) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
split.
(* Goal: forall _ : @Equal E x x1, False *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
intros H'5; try assumption.
(* Goal: False *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
cut (~ in_part x1 (single x)).
(* Goal: forall _ : not (@in_part E x1 (@single E x)), False *)
(* Goal: not (@in_part E x1 (@single E x)) *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
intro.
(* Goal: False *)
(* Goal: not (@in_part E x1 (@single E x)) *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply H7.
(* Goal: @in_part E x1 (@single E x) *)
(* Goal: not (@in_part E x1 (@single E x)) *)
(* Goal: @Equal F (@Ap E F f x) (@Ap E F f x1) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
apply in_part_trans_eq with x; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply diff_in_r with Chaussettes; auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
(* Goal: @ex nat (fun m0 : nat => @eq nat m (S m0)) *)
inversion H'1.
(* Goal: @ex nat (fun m0 : nat => @eq nat O (S m0)) *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (S n2) (S m0)) *)
cut (in_part (f x) Tiroirs).
(* Goal: forall _ : @in_part F (@Ap E F f x) Tiroirs, @ex nat (fun m0 : nat => @eq nat O (S m0)) *)
(* Goal: @in_part F (@Ap E F f x) Tiroirs *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (S n2) (S m0)) *)
intros H'4; try assumption.
(* Goal: @eq nat (S n2) (S n2) *)
absurd (in_part (f x) (empty F)); auto with *.
(* Goal: @eq nat (S n2) (S n2) *)
apply in_part_comp_r with Tiroirs; auto with *.
(* Goal: @in_part F (@Ap E F f x) Tiroirs *)
(* Goal: @ex nat (fun m0 : nat => @eq nat (S n2) (S m0)) *)
apply H'3.
(* Goal: @eq nat (S n2) (S n2) *)
apply in_part_comp_r with (add_part B x); auto with *.
(* Goal: @ex nat (fun m0 : nat => @eq nat (S n2) (S m0)) *)
exists n2; try assumption.
(* Goal: @eq nat (S n2) (S n2) *)
auto with *.
Qed.
End tiroirs_def.
