# 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   end. Obligations. ```
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   end. ```
Again, 3 obligations are generated that are easily solved
``` ```