(* begin hide *)
Require Import List.
Require Import Coq.subtac.Utils.    
(* end hide *)
(** 
Roughly inspired by the article:
Richard S. Bird, Sharon A. Curtis: 
Functional Pearls: Finding celebrities: A lesson in functional programming. 
J. Funct. Program. 16(1): 13-20 (2006)
   
Actually, more inspired by a discussion with Nicolas Oury on
finding a formalization of the problem and implementing a solution in
Coq. Original challenge idea due to Conor McBride.

The goal is to find the clique of celebrities among the guests of a
party, knowing that there exists such a clique. The algorithm can then
be done in linear time. *)
(** The set of people at the party. *)

Variable person : Set.

(** Predicate [celeb] asserts celebrity. *)

Variables celeb : person -> Prop.

(** The type of persons who are celebrities *)

Definition celebrity : Set := sig celeb.

(** Who knows who ? *) 

Variable knows : person -> person -> Prop.

(** Is decidable *)

Axiom knows_dec : forall x y, { knows x y } + { ~ knows x y }.

(** Pretty notations. *)

Notation " x 'knows' y " := (knows x y) (at level 20).
Notation " x 'knows_dec' y " := (knows_dec x y) (at level 20).

(** Statement that every celebrity is known by everyone. *)

Program Axiom guest_knows_celeb :
  forall (c : celebrity) (g : person), g knows c.

(** Statement that every celebrity knows only celebrities (closed circle). *)

Program Axiom celeb_knows_celeb :
  forall (c : celebrity) (g : person), c knows g -> celeb g.

(** We represent set of people by lists. *)
Definition persons := list person.

(** Abbreviation for being part of a clique. The [:>] casts
   subset objects to their underlying support type. *)

Notation " x 'In' l " := (In (x :>) l) (at level 20).
Definition in_clique p c := 
  forall x, x In c -> (p knows x /\ x knows p). 
Hint Unfold in_clique.

(** The [entry] program builds the clique of VIPs from all the people
  coming at the party using a (disposable) doorman which discriminate
  between celebs and regular people.
  The definition is clearly tail recursive hence we get a linear-time algorithm 
  as advertised in the paper.
  *)

Program Fixpoint entry (guests : persons)
  (doorman : person | celeb doorman \/ exists x : celebrity, x In guests)
  (clique : persons | in_clique doorman clique /\
    (forall x : celebrity, x In guests \/ x `= doorman \/ x In clique))
  { struct guests } :
  { celebs : persons | forall x, x In celebs <-> celeb x } :=
  match guests with
    g :: gs => 
      if doorman knows_dec g then
        if g knows_dec doorman then 
          entry gs doorman (g :: clique)
        else entry gs g nil
      else entry gs doorman clique
   | nil => doorman :: clique
  end.

Obligations.

(** Skipping 7 obligations solved using the axioms. *)

(* begin hide *)
Next Obligation.
Proof.
  unfold in_clique in * ; simpl in * ; intros.
  destruct H3. 
  left ; auto.

  destruct H3 as [c [Hc|Hc]].
  subst g.
  left.
  apply (celeb_knows_celeb c _ H0).

  right ; exists c ; intuition.
Qed.

Next Obligation.
Proof.
  intros.
  destruct_exists ; split.


  red ; intros x Inx.
  destruct Inx as [Inx|Inx].
  subst g ; intuition.
  apply (H1 _ Inx).

  intros.
  pose (H3 x).
  intuition.
    
  destruct H2 as [Hs | Hx] ; [ subst ; intuition | idtac ] ;
  left ; auto.

  destruct H2 as [Hs | Hx] ; [ subst ; intuition | idtac ] ; left ; auto.
Qed.

Tactic Notation "contradiction" "by" constr(c) := pose c ; contradiction.
  
Next Obligation.
Proof.
  intros.
  destruct H3.
  contradiction by (guest_knows_celeb (exist _ doorman H3) g).

  destruct H3 as [x [xg|Inx]].
  subst g ; left ; destruct x ; auto.
  right ; exists x ; intuition.
Qed.

Next Obligation.
Proof.
  split ; try red ; intros.

  inversion H4.

  pose (H2 x).
  destruct o.
  induction H4 as [Inx|Inx].
  subst g.
  right ; left ; intuition.
  left ; auto.

  destruct H4.
  subst.
  contradiction by (guest_knows_celeb x g).

  destruct (H1 _ H4) as [Hx0x1 Hx1x0].
  
    assert(celeb doorman) by (apply (celeb_knows_celeb x) ; auto).
    contradiction by (guest_knows_celeb (exist _ doorman H5) g).
Qed.

Next Obligation.
Proof.
  intros.
  destruct H2.
  left ; assumption.
  
  destruct H2 as [x [xg|Inx]].
  subst g.
  contradiction by (guest_knows_celeb x doorman).

  right ; eauto.
Qed.

Next Obligation.
Proof.
  intros.
  destruct H0. 
  split ; auto ; intros.

  destruct (H2 x).
  destruct H3 as [xg|Inx].

  subst g ; contradiction by (guest_knows_celeb x doorman).
  
  intuition.
  intuition.
Qed.

Next Obligation.
Proof.
  intros.
  destruct H as [Hcl Hcel].
  split ; intros.
  
  destruct H0 as [Hx1|[y Iny]] ; [idtac | inversion Iny ].

  destruct H as [Heq | Hin] ; [ subst ; apply Hx1 | idtac ].
  destruct  (Hcl _ Hin).
  apply (celeb_knows_celeb (exist _ _ Hx1) _ H).

  destruct (Hcel (exist _ _ H)) as [Hn|[Hn|Hn]] ; simpl in Hn ; try solve [inversion Hn] ; intuition.
Qed.
(* end hide *)  
(** We bootstrap the [entry] program, asserting that guests
    contains all existing people. *)

Program Definition find_celebs 
  (guests : persons | (exists x, x In guests /\ celeb x) /\ forall x, x In guests) :
  { celebs : persons | forall x, x In celebs <-> celeb x } := 
  match guests with
  | nil => !
  | p :: ps => entry ps p nil
  end.

(** Again, 3 obligations are generated that are easily solved *)

Next Obligation.
Proof.
  destruct_exists.
  inversion H1.
Qed.

Next Obligation.
Proof.
  destruct_exists.
  destruct H1.
  subst p ; left ; auto.
  right ; exists (exist celeb _ H2) ; intuition.
Qed.

Next Obligation.
Proof.
  destruct_exists.
  split.
  
  red ; intros.
  inversion H3.

  intros.
  pose (H0 (`x)).
  destruct i.
  subst.
  right ; left ; auto.
  left ; assumption.
Qed.