(************************************************************************)
(* Copyright 2007 Milad Niqui                                           *)
(* This file is distributed under the terms of the                      *)
(* GNU Lesser General Public License Version 2.1                        *)
(* A copy of the license can be found at                                *)
(*                  <http://www.gnu.org/licenses/lgpl.txt>              *)
(************************************************************************)

Require Import Arith Omega.

Require OrderedTypeEx.
Require FSetList.
Module NatSet := FSetList.Make(OrderedTypeEx.Nat_as_OT).
Import NatSet.

Infix "++" := add (at level 60, right associativity).
Notation "s [=] t" := (Equal s t) (at level 70, no associativity).

Require FSetFacts FSetProperties.
Require Extraction.

Module GeneralProperties := FSetProperties.Properties NatSet.
Import GeneralProperties.

Section problem_knows_not_refl.

Variable town: t.
Variable n:nat.
Variable cardinality: cardinal town = 2*n+1.

Variable knows: elt -> elt -> Prop. 

Variable knows_sym: forall m n, knows m n ->  knows n m.
Variable knows_extensional:forall m n p, E.eq n p -> knows m n-> knows m p.

Variable property: forall B, Subset B town -> cardinal B = n -> 
           {d:elt | In d (diff town B)/\(forall b, In b B -> knows d b)}.

Lemma extendible_by_one:forall B', cardinal B' <= (cardinal town)-1 -> {d:elt| In d town /\ ~(In d B')}.
Proof.
(* Goal: forall (B' : t) (_ : le (cardinal B') (Init.Nat.sub (cardinal town) (S O))), @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 clear knows knows_sym knows_extensional property.
(* Goal: forall (B' : t) (_ : le (cardinal B') (Init.Nat.sub (cardinal town) (S O))), @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 intros B' H_cardinal_town.
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 assert (H_town:1<=(cardinal town)); [omega|].
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 rewrite <- (diff_inter_cardinal town B') in H_cardinal_town.
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 rewrite <- (diff_inter_cardinal town B') in H_town.
 assert (H_inter:cardinal (inter town B') <= cardinal B');
  [apply (subset_cardinal);apply (inter_subset_2)|].
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 generalize (le_trans _ _ _ H_inter H_cardinal_town); intro H1.
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 assert (H2:1<=cardinal (diff town B')); [omega|].
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 assert (H3:=(S_pred _ _ H2)).
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 destruct (cardinal_inv_2 H3) as [d Hd].
(* Goal: @sig elt (fun d : elt => and (In d town) (not (In d B'))) *)
 exists d; split.
(* Goal: In d town *)
(* Goal: not (In d B') *)
  apply diff_1 with B'; assumption.
(* Goal: forall _ : In d B, False *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
  apply diff_2 with town; assumption.
Qed.  

Lemma extendible_to_n:forall B', Subset B' town -> cardinal B' <= n -> 
     {B:t| cardinal B = n /\  Subset B' B /\ Subset B town}.  
Proof.
(* Goal: forall (B' : t) (_ : Subset B' town) (_ : le (cardinal B') n), @sig t (fun B : t => and (@Logic.eq nat (cardinal B) n) (and (Subset B' B) (Subset B town))) *)
 intros B' H_sub H_B'_cardinal.
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) n) (and (Subset B' B) (Subset B town))) *)
 assert (H_cardinal_aux_3:2*n<=(cardinal town)-1);[apply le_trans with (2*n); omega|].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) n) (and (Subset B' B) (Subset B town))) *)
 clear property.
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) n) (and (Subset B' B) (Subset B town))) *)
 induction n in H_B'_cardinal, H_cardinal_aux_3 |- *.
 (* n = 0 *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) O) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
 generalize (sym_eq (le_n_O_eq _ H_B'_cardinal)); intro H_eq.
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) O) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
 generalize (empty_is_empty_1 (cardinal_inv_1 H_eq)).
(* Goal: forall _ : Equal B' empty, @sig t (fun B : t => and (@Logic.eq nat (cardinal B) O) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
 intro H_B'.
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) O) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
 exists empty; repeat split. 
(* Goal: Subset B' empty *)
(* Goal: Subset empty town *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  rewrite H_B'; apply subset_empty.
(* Goal: Subset empty town *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  apply subset_empty.
 (* n = S n0 *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
 destruct (le_lt_eq_dec _ _ H_B'_cardinal) as [H_lt|H_le].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  generalize (lt_n_Sm_le _ _ H_lt); clear H_lt; intro H_le.
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  assert (H_cardinal_town_2:2 * n0 <= cardinal town - 1);[omega|].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  destruct (IHn0 H_le H_cardinal_town_2) as [C [HC1 [HC2 HC3]]].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  assert (HC5:cardinal C <= cardinal town - 1).
(* Goal: le (cardinal C) (Init.Nat.sub (cardinal town) (S O)) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
   rewrite HC1; apply le_trans with (2*(S n0));[omega| assumption].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  destruct (extendible_by_one C HC5) as [d [Hd1 Hd2]].
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  exists (d ++ C).
(* Goal: and (Subset empty town) (and (@Logic.eq nat (cardinal empty) O) (forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1)) *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  repeat split.
(* Goal: @Logic.eq nat (cardinal (add d C)) (S n0) *)
(* Goal: Subset B' (add d C) *)
(* Goal: Subset (add d C) town *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
   rewrite (add_cardinal_2 Hd2); rewrite HC1; reflexivity.
(* Goal: Subset B' (add d C) *)
(* Goal: Subset (add d C) town *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
   apply subset_add_2; assumption.
(* Goal: Subset (add d C) town *)
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
   apply subset_add_3; assumption.
  
(* Goal: @sig t (fun B : t => and (@Logic.eq nat (cardinal B) (S n0)) (and (Subset B' B) (Subset B town))) *)
  exists B'.
(* Goal: and (@Logic.eq nat (cardinal B') (S n0)) (and (Subset B' B') (Subset B' town)) *)
  repeat split; trivial; apply subset_refl.
Qed.


(** The following property, proven by induction, is the heart of the
solution, and is due to Tonny Hurkens. *)
Lemma inductive_invariant:forall m, m<= n ->
   {B':t| Subset B' town /\ cardinal B' = m /\ forall b'0 b'1, In b'0 B' -> In b'1 B' -> ~(E.eq b'0 b'1) -> knows b'0 b'1}.
Proof.
(* Goal: forall (m : nat) (_ : le m n), @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') m) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
 intros m.
(* Goal: forall _ : le m n, @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') m) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
 induction m; intros H_le.
  (* 0 *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') O) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  exists empty.
(* Goal: and (Subset empty town) (and (@Logic.eq nat (cardinal empty) O) (forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1)) *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  repeat split.
(* Goal: Subset empty town *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
   apply subset_empty.
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
   intros b'0 b'1 H0 H1; apply False_ind. 
(* Goal: False *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
   elim (FM.empty_iff b'0); intros H2 _; apply H2; assumption.
  (* S n *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  assert (H_le0:=le_Sn_le _ _ H_le).
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  destruct (IHm H_le0) as [B' [H3' [H1 H2]]].
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  rewrite <- H1 in H_le0.
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  destruct (extendible_to_n B' H3' H_le0) as [B [HB1 [HB2 HB3]]].
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  destruct (property B HB3 HB1) as [d [Hd1 Hd2]].
(* Goal: and (Subset empty town) (and (@Logic.eq nat (cardinal empty) O) (forall (b'0 b'1 : elt) (_ : In b'0 empty) (_ : In b'1 empty) (_ : not (E.eq b'0 b'1)), knows b'0 b'1)) *)
(* Goal: @sig t (fun B' : t => and (Subset B' town) (and (@Logic.eq nat (cardinal B') (S m)) (forall (b'0 b'1 : elt) (_ : In b'0 B') (_ : In b'1 B') (_ : not (E.eq b'0 b'1)), knows b'0 b'1))) *)
  exists (add d B'); repeat split.
   (* subset of town *)
(* Goal: Subset (add d B') town *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   apply subset_add_3.
(* Goal: In d town *)
(* Goal: Subset B' town *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   apply diff_1 with B; assumption.
(* Goal: Subset B' town *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   apply subset_trans with B; assumption.
   (* cardinality *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   rewrite <- H1.
(* Goal: @Logic.eq nat (cardinal (add d B')) (S (cardinal B')) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   apply add_cardinal_2.
(* Goal: not (In d B') *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   intro Hd4.
(* Goal: False *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   generalize (in_subset Hd4 HB2).
(* Goal: forall _ : In d B, False *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   apply diff_2 with town; assumption.
(* second big goal *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   intros b'0 b'1 H_b'0 H_b'1 H_neq.
(* Goal: knows b'0 b'1 *)
   destruct ((proj1 (FM.add_iff B' d b'0)) H_b'0) as [H3|H3].
(* Goal: knows b'0 b'1 *)
(* Goal: knows b'0 b'1 *)
    apply knows_sym; apply knows_extensional with d; trivial.
(* Goal: knows b'0 b'1 *)
    destruct ((proj1 (FM.add_iff B' d b'1)) H_b'1) as [H4|H4].
(* Goal: knows b'1 d *)
(* Goal: knows b'1 d *)
(* Goal: knows b'0 b'1 *)
     apply False_ind; apply H_neq; rewrite <- H3; assumption.
(* Goal: knows e d *)
(* Goal: knows e u *)
     apply knows_sym. 
(* Goal: knows d b'0 *)
(* Goal: knows b'0 b'1 *)
     apply Hd2; apply in_subset with B'; trivial.
(* Goal: knows b'0 b'1 *)
    destruct ((proj1 (FM.add_iff B' d b'1)) H_b'1) as [H4|H4].
(* Goal: knows e u *)
(* Goal: knows e u *)
     apply knows_extensional with d; trivial.
(* Goal: knows e d *)
(* Goal: knows e u *)
     apply knows_sym.
(* Goal: knows d b'0 *)
(* Goal: knows b'0 b'1 *)
     apply Hd2; apply in_subset with B'; trivial.
(* Goal: knows b'0 b'1 *)
     apply H2; assumption.
Qed.

Theorem AMM11262: {e:elt | In e town /\ forall u, In u town /\ ~(E.eq u e)-> knows e u}.
Proof.
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 destruct (inductive_invariant n (le_refl n)) as [B [HB1 [HB2 HB3]]].
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 destruct (property B HB1 HB2) as [d [Hd1 Hd2]].
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 set (C:=(diff town (d ++ B))).
 (* C subset town *)
 assert (H_susbset_C:Subset C town);
 [ subst C; apply subset_diff; apply subset_refl
 | ].
 (* inter town *) 
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 assert (H_inter_town: inter town (d ++ B)[=]d ++ B).
  rewrite inter_sym; apply inter_subset_equal;
(* Goal: In d town *)
(* Goal: Subset B' town *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
  apply subset_add_3; trivial; apply diff_1 with B; assumption.
 (* ~ In d B *)
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 assert (H_d_nin_B:~In d B); [apply diff_2 with town; assumption|].
 (* cardinal C = n *)
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 assert (H_cardinal_C:cardinal C=n).
(* Goal: @Logic.eq nat (cardinal C) n *)
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
  assert (H_aux:cardinal (inter town (d ++ B))=S n).
   rewrite (@Equal_cardinal (inter town (d ++ B)) (d++B) H_inter_town);
   rewrite (add_cardinal_2 H_d_nin_B); rewrite HB2; reflexivity.
  generalize (diff_inter_cardinal town (d++B));
  fold C; rewrite H_aux; rewrite cardinality; omega.
 
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 destruct (property C H_susbset_C H_cardinal_C) as [e [He1 He2]].
(* Goal: @sig elt (fun e : elt => and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u)) *)
 exists e.
 (* Subset (d++B) town *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
 assert (H_dB_town:Subset (d++B) town).
(* Goal: Subset (add d B) town *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
  intros a Ha0; destruct ((proj1 (FM.add_iff B d a)) Ha0) as [Had|HaB].  
(* Goal: In d town *)
(* Goal: Subset B' town *)
(* Goal: @Logic.eq nat (cardinal (add d B')) (S m) *)
(* Goal: forall (b'0 b'1 : elt) (_ : In b'0 (add d B')) (_ : In b'1 (add d B')) (_ : not (E.eq b'0 b'1)), knows b'0 b'1 *)
   rewrite <- Had; apply diff_1 with B; assumption.
(* Goal: In a town *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
   apply HB1; assumption.
 (* diff town C = d++B *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
 assert (H_diff:diff town C [=] d++B ).
(* Goal: Equal (diff town C) (add d B) *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
  unfold C; split; intro H_mem.
   (* => *)
   assert (H_a0:=diff_1 H_mem);
   assert (H_a1:=diff_2 H_mem);
   destruct (In_dec a (d++B)) as [H_a2|H_a2]; trivial;
   apply False_ind; apply H_a1; exact (diff_3 H_a0 H_a2).
   (* <= *)
(* Goal: In a (diff town (diff town (add d B))) *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
   destruct (In_dec a (diff town (d++B))) as [H_a2|H_a2].
(* Goal: In a (diff town (diff town (add d B))) *)
(* Goal: In a (diff town (diff town (add d B))) *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
    apply False_ind; exact (diff_2 H_a2 H_mem). 
(* Goal: In a (diff town (diff town (add d B))) *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
    apply diff_3; trivial; apply H_dB_town; assumption.
 (* In e (d++B) *)
(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
 assert (H_e_dB:In e (d++B)); [rewrite <- H_diff; assumption|].

(* Goal: and (In e town) (forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u) *)
 split.
(* Goal: In e town *)
(* Goal: forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u *)
  apply diff_1 with C; assumption...
(* Goal: forall (u : elt) (_ : and (In u town) (not (E.eq u e))), knows e u *)
  intros u [Hu Hu'].
(* Goal: knows e u *)
  assert (H_town_part:town [=] (union C (d++B))).
(* Goal: Equal town (union C (add d B)) *)
(* Goal: knows e u *)
   rewrite <- (diff_inter_all town (d++B)); rewrite H_inter_town; apply equal_refl.
(* Goal: knows e u *)
   rewrite H_town_part in Hu.
(* Goal: knows e u *)
   destruct (union_1 Hu) as [HuC|HudB].
    (* In u C *)
(* Goal: knows e u *)
(* Goal: knows e u *)
    apply He2; assumption. 
    (* In u (d++B) *)
(* Goal: knows e u *)
    destruct ((proj1 (FM.add_iff B d u)) HudB) as [Hud|HuB].
     (* d=u *)
(* Goal: knows e u *)
(* Goal: knows e u *)
     apply knows_extensional with d; trivial.
(* Goal: knows e d *)
(* Goal: knows e u *)
     apply knows_sym.
(* Goal: knows e u *)
     destruct ((proj1 (FM.add_iff B d e)) H_e_dB) as [Hed|HeB].
      (* d=e *)
(* Goal: knows d e *)
(* Goal: knows d e *)
(* Goal: knows e u *)
      apply False_ind; apply Hu'; rewrite <- Hud; assumption.
      (* In e B *)
(* Goal: knows d e *)
(* Goal: knows e u *)
      apply Hd2; assumption.
     (* In u B *)
(* Goal: knows e u *)
     destruct ((proj1 (FM.add_iff B d e)) H_e_dB) as [Hed|HeB].
      (* d=e *) 
      apply knows_sym; apply knows_extensional with d; trivial;
(* Goal: knows d e *)
(* Goal: knows e u *)
      apply knows_sym; apply Hd2; assumption.
      (* In e B *)
(* Goal: knows e u *)
      apply HB3; assumption || contradict Hu'; auto with *.
Qed.

End problem_knows_not_refl.

Extraction "amm11262" AMM11262.
