The Coq mailing list

[Alex Shkotin <alex.shkotin AT gmail.com>]

Hi Fred,

it looks like widely known in restrict groups https://en.wikipedia.org/wiki/Zebra_Puzzle

does it?

Alex

2016-09-24 13:53 GMT+03:00 Fred Smith <fsmith1024 AT gmail.com>:

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.