The Coq mailing list

[Amirhossein Vakili <avakili AT outlook.com>]

I really like Coq and theorem proving. A solution to this problem in 
Alloy is attached. Using a finite model finder like Alloy, one can solve 
this problem automatically and show that it has a unique solution too.

Best,
Amir

On 2016-09-24 06:53 AM, Fred Smith wrote:
> Hi all,
>
> Below is a puzzle my son brought home from school.  It came on a 
> crumpled up piece of paper, photocopied out of some unknown puzzle 
> book; irresistible.   We raced to solve it.  He beat me by a hair.  To 
> lengthen the fun, I thought to formalize and solve it using Coq; and 
> have just finished the project.
>
> I thought some readers of the list might enjoy doing the same.
>
> Enjoy,
>
> Fred
>
> (*
> New York City Guys
> by Frank Alward
>
> The five-story Manning Building, located in the Wall Streat area of
> Manhattan, houses the home offices of Matt and four other prominent
> businessmen.  Each man's business is located on a different floor of
> the building, and each also has a branch office located in a foreign
> city.  No two have a branch in the same city.  The man who visits his
> branch in Cairo usually combines his trip with a short vacation.  Each
> of the five men resides in a different borough of New York City.
> From this information and the clues below, can you determine each man's
> home borough, branch office location, and floor?
>
> 1. Rick's office is one floor below the office of the man who lives in
> the Bronx, which is not on the fourth floor.
>
> 2. The office of the Staten Island resident is one floor below
> Roland's, who doesn't live in Queens.
>
> 3. Shaun's office is one floor below the one who visits his branch in
> Rome.
>
> 4. Cliff's branch isn't located in Athens.
>
> 5. The man who lives in Manhattan has no branch in Rome.
>
> 6. The Paris branch is not Shaun's.
>
> 7. The office of the man who lives in Brooklyn is one floor below that
> of the businessman who visits his branch in Geneva, which is not on
> the fifth floor.
>
> 8. The office of the one who lives in the Bronx is on some floor above
> Roland's.
>
> 9. Rick, who has no branch in Geneva, doesn't live in Queens.
>
> 10. Neither the Staten Island resident nor the Manhattan resident has
> a branch in Athens.
>
>  *)
>
> Require Import Arith.
> Require Import Nat.
> Require Import Psatz. (* Required for lia -- tactic for solving linear 
> arithmetic. *)
>
> Inductive person := Cliff | Matt | Rick | Roland | Shaun.
>
> Inductive branch := Athens | Cairo | Geneva | Paris | Rome.
>
> Inductive home := Brooklyn | Bronx | Manhattan | Queens | StatenIsland.
>
> Section Puzzle.
>
>   Parameter B : person -> branch.
>   Parameter H : person -> home.
>   Parameter F : person -> nat.
>   Axiom B_unique : forall p1 p2 : person, B p1 = B p2 -> p1 = p2.
>   Axiom H_unique : forall p1 p2 : person, H p1 = H p2 -> p1 = p2.
>   Axiom F_unique : forall p1 p2 : person, F p1 = F p2 -> p1 = p2.
>
>   Axiom F_range : forall p : person, F p > 0 /\ F p <= 5.
>
>   Lemma F_cases : forall p : person, F p = 1 \/ F p = 2 \/ F p = 3 \/ 
> F p = 4 \/ F p = 5.
>   Proof.
>     intro p.
>     assert (H := F_range p).
>     lia.
>   Qed.
>   Variables X1 X2 X3 X4 X5 X6 X7 X8 X9 : person.
>
>   Axiom R1 : S (F Rick) = (F X1) /\ (H X1) = Bronx /\ (F X1) <> 4.
>   Axiom R2: S (F X2) = (F Roland) /\ (H X2) = StatenIsland /\ (H 
> Roland) <> Queens.
>   Axiom R3: S (F Shaun) = (F X3) /\ (B X3) = Rome.
>   Axiom R4: (B Cliff) <> Athens.
>   Axiom R5: (H X4) = Manhattan /\ (B X4) <> Rome.
>   Axiom R6: (B Shaun) <> Paris.
>   Axiom R7: S (F X5) = (F X6) /\ (H X5) = Brooklyn /\ (B X6) = Geneva 
> /\ (F X6) <> 5.
>   Axiom R8: (F X7) > (F Roland) /\ (H X7) = Bronx.
>   Axiom R9: (B Rick) <> Geneva /\ (H Rick) <> Queens.
>   Axiom R10: (H X8) = StatenIsland /\ (B X8) <> Athens /\ (H X9) = 
> Manhattan /\ (B X9) <> Athens.
>
> End Puzzle.
>

/*
New York City Guys 
by Frank Alward

The five-story Manning Building, located in the Wall Streat area of
Manhattan, houses the home offices of Matt and four other prominent
businessmen.  Each man's business is located on a different floor of
the building, and each also has a branch office located in a foreign
city.  No two have a branch in the same city.  The man who visits his
branch in Cairo usually combines his trip with a short vacation.  Each
of the five men resides in a different borough of New York City.
From this information and the clues below, can you determine each man's
home borough, branch office location, and floor?

1. Rick's office is one floor below the office of the man who lives in
the Bronx, which is not on the fourth floor.

2. The office of the Staten Island resident is one floor below
Roland's, who doesn't live in Queens.

3. Shaun's office is one floor below the one who visits his branch in
Rome.

4. Cliff's branch isn't located in Athens.

5. The man who lives in Manhattan has no branch in Rome.

6. The Paris branch is not Shaun's.

7. The office of the man who lives in Brooklyn is one floor below that
of the businessman who visits his branch in Geneva, which is not on
the fifth floor.

8. The office of the one who lives in the Bronx is on some floor above
Roland's.

9. Rick, who has no branch in Geneva, doesn't live in Queens.

10. Neither the Staten Island resident nor the Manhattan resident has
a branch in Athens.
*/

abstract sig Floor {one_above: set Floor}
one sig F1, F2, F3, F4, F5 extends Floor {}

fact {
  one_above = F5 -> F4 + F4 -> F3 + F3 -> F2 + F2 -> F1
}

pred is_one_floor_above[f1, f2: Floor] {
  f1 -> f2 in one_above
}

abstract sig NewYork {}
one sig Bronx, Saten, Queens, Manhattan, Brooklyn extends NewYork {}

abstract sig City{}
one sig Cairo, Rome, Athens, Paris, Geneva extends City {}

abstract sig Person{floor: one Floor, branch: one City, lives: one NewYork}
one sig Matt, Rick, Roland, Shaun, Cliff extends Person {}

fact {
// Every two distinct people have distinct floors, branches and live in 
different parts of New York.
  all p1, p2: Person| floor[p1] = floor[p2] implies p1 = p2
  all p1, p2: Person| branch[p1] = branch[p2] implies p1 = p2
  all p1, p2: Person| lives[p1] = lives[p2] implies p1 = p2

// 1. Rick's office is one floor below the office of the man who lives in
// the Bronx, which is not on the fourth floor.
  is_one_floor_above[floor[lives.Bronx], floor[Rick]]
  floor[lives.Bronx] != F4
// 2. The office of the Staten Island resident is one floor below
// Roland's, who doesn't live in Queens.
  is_one_floor_above[floor[Roland],  floor[lives.Saten]]
   lives[Roland] != Queens
// 3. Shaun's office is one floor below the one who visits his branch in
// Rome.
  is_one_floor_above[floor[branch.Rome], floor[Shaun]]
// 4. Cliff's branch isn't located in Athens.
  branch[Cliff] != Athens
// 5. The man who lives in Manhattan has no branch in Rome.
  branch[lives.Manhattan] != Rome
// 6. The Paris branch is not Shaun's.
  branch[Shaun] != Paris
// 7. The office of the man who lives in Brooklyn is one floor below that
// of the businessman who visits his branch in Geneva, which is not on
// the fifth floor.
  is_one_floor_above[floor[branch.Geneva], floor[lives.Brooklyn]]
  floor[branch.Geneva] != F5
// 8. The office of the one who lives in the Bronx is on some floor above
// Roland's.
  floor[lives.Bronx] -> floor[Roland] in ^one_above
// 9. Rick, who has no branch in Geneva, doesn't live in Queens.
   branch[Rick] != Geneva
  lives[Rick] != Queens
// 10. Neither the Staten Island resident nor the Manhattan resident has
// a branch in Athens.
  not Athens in (lives.(Saten + Manhattan)).branch
}

run {}