# 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

```
```