Library celebs

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


Skipping 7 obligations solved using the axioms.

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

Again, 3 obligations are generated that are easily solved