The Coq mailing list

[Fred Smith <fsmith1024 AT gmail.com>]

I didn't want to spoil the fun.  Haven't shared my solution yet.  

-Fred

On Tue, Sep 27, 2016 at 2:30 AM, Jean-François Dufourd <jfd AT unistra.fr> wrote:

Hi Fred,

Thank you for the nice puzzle and Coq formalization. But, where is the solution?

Regards,

Jean-François

Le 24/09/2016 12:53, Fred Smith a écrit :

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.