Require Import List.

Variable Guest : Set.

Parameter Knows : Guest -> Guest -> Prop.

Parameter KnowsDec : forall (x y : Guest), {Knows x y} + {not (Knows x y)}.

Definition Group := list Guest.

Definition CelebrityClique (party : Group) (clique : Group)  :=
  incl clique party
  /\
  clique <> nil
  /\
  (forall c x : Guest, In c clique -> In x party -> Knows x c)
  /\ 
  (forall c1 c2 : Guest, In c1 clique /\ In c2 party /\ Knows c1 c2 -> In c2 clique).

Hint Unfold CelebrityClique.

Definition CliqueExists (party : Group) :=
  (forall c : Group, CelebrityClique c party -> False) -> False.

Hint Unfold CliqueExists.

Lemma incl_nil (A : Set) (xs : list A) : incl nil xs.
  Proof.
  unfold incl.
  intuition.
  elim H.
  Qed.

Lemma incl_single (A : Set) (x : A) (xs : list A) : incl (x :: nil) (x :: xs).
  Proof.
  intros.
  apply incl_cons.
  intuition.
  apply incl_nil.
  Qed.


(*
Lemma CliqueExtension (c : Guest) (party : Group)  :
  not(CliqueExists party) -> CliqueExists(c::party) -> CelebrityClique (c::party) (c::nil).
  intros c party NEx Ex.
  unfold CelebrityClique.
  split; try apply incl_single; split; try discriminate.
  split.
  unfold CliqueExists in NEx.
  unfold
  intuition; try discriminate.
  split; try incl_cons. try discriminate.
*)
  
Program Fixpoint findClique (guests : list Guest) {struct guests}:
  {celebs : Group | CliqueExists guests -> CelebrityClique guests celebs} :=
  match guests with
    | nil => nil
    | x::xs =>
      let clique := findClique xs
      in match clique with
           | nil => x :: nil
           | (doorman :: celebs) => 
             if KnowsDec doorman x
             then if KnowsDec x doorman
                  then x :: clique
                  else x :: nil
             else clique
           end 
  end.

Obligations.

(* The case for an empty list of guests *)
Next Obligation.
  elim H.
  unfold CelebrityClique.
  intuition.
  Qed.

Next Obligation.
  unfold CelebrityClique.
  split.
  apply incl_cons.
  auto with datatypes.
  apply incl_nil.  
  split; try discriminate.
  split.
  intros celeb y.
  assert (not(CliqueExists xs)).
  generalize (findClique xs).  
  unfold CliqueExists.
  unfold CliqueExists in H.
  unfold CelebrityClique in H.
  unfold CelebrityClique.
  intuition.