fixedpoint.jp


"Einstein's five houses"パズルをCoqで解く (2016-08-02)

Einstein's five houses riddle、またはZebra puzzleとも呼ばれる有名なパズルがあります。今回はこの解答をCoqで形式的に証明しました。

以下がこの問題を定義と公理にしたものです。興味のある方はここから解答の証明を考えてみてください。

five_houses_problem.v
Section five_houses.

(* Definitions and axioms *)

Inductive owner : Type :=
| a : owner
| b : owner
| c : owner
| d : owner
| e : owner.

Inductive nationality : Type :=
| dane : nationality
| brit : nationality
| swede : nationality
| norwegian : nationality
| german : nationality.

Parameter citizen : owner -> nationality.

Inductive color : Type :=
| yellow : color
| red : color
| white : color
| green : color
| blue : color.

Parameter house : owner -> color.

Inductive animal : Type :=
| horse : animal
| cat : animal
| bird : animal
| fish : animal
| dog : animal.

Parameter pet : owner -> animal.

Inductive beverage : Type :=
| water : beverage
| tea : beverage
| milk : beverage
| coffee : beverage
| root_beer : beverage.

Parameter drink : owner -> beverage.

Inductive cigar : Type :=
| pall_mall : cigar
| prince : cigar
| blue_master : cigar
| dunhill : cigar
| blends : cigar.

Parameter smoke : owner -> cigar.

Definition left_of (X1 X2 : owner) : Prop :=
  match X1, X2 with
    | a, b => True
    | b, c => True
    | c, d => True
    | d, e => True
    | _, _ => False
  end.

Definition next_to (X1 X2 : owner) : Prop :=
  left_of X1 X2 \/ left_of X2 X1.

Axiom citizen_is_surjective:
  forall N : nationality, exists X : owner, citizen X = N.

Axiom house_is_surjective:
  forall C : color, exists X : owner, house X = C.

Axiom pet_is_surjective:
  forall A : animal, exists X : owner, pet X = A.

Axiom drink_is_surjective:
  forall B : beverage, exists X : owner, drink X = B.

Axiom smoke_is_surjective:
  forall C : cigar, exists X : owner, smoke X = C.

Axiom clue1: (* The Brit lives in the house with red walls. *)
  forall X : owner,  house X = red -> citizen X = brit.

Axiom clue2: (* The Swede has a dog. *)
  forall X : owner, citizen X = swede -> pet X = dog.

Axiom clue3: (* The Dane drinks tea. *)
  forall X : owner, citizen X = dane -> drink X = tea.

Axiom clue4: (* The house with green walls is directly to the left of the house with white walls. *)
  forall X1 X2 : owner,
    house X1 = green -> (left_of X1 X2 <-> house X2 = white).

Axiom clue5: (* The owner of the house with green walls drinks coffee. *)
  forall X : owner, house X = green -> drink X = coffee.

Axiom clue6: (* The person who smokes Pall Mall cigars owns a bird. *)
  forall X : owner, smoke X = pall_mall -> pet X = bird.

Axiom clue7: (* The owner of the house with yellow walls smokes Dunhill. *)
  forall X : owner, house X = yellow -> smoke X = dunhill.

Axiom clue8: (* The man living in the center house drinks milk. *)
  drink c = milk.

Axiom clue9: (* The Norwegian lives in the first house. *)
  citizen a = norwegian.

Axiom clue10: (* The man who smokes blends lives next to the cat owner. *)
  forall X1 X2 : owner,
    smoke X1 = blends -> pet X2 = cat -> next_to X1 X2.

Axiom clue11: (* The horse’s owner lives next to the man who smokes Dunhill. *)
  forall X1 X2: owner,
    pet X1 = horse -> smoke X2 = dunhill -> next_to X1 X2.

Axiom clue12: (* The man who smokes Blue Master drinks root beer. *)
  forall X : owner, drink X = root_beer -> smoke X = blue_master.

Axiom clue13: (* The German smokes Prince. *)
  forall X : owner, citizen X = german -> smoke X = prince.

Axiom clue14: (* The Norwegian lives next to the house with blue walls. *)
  forall X1 X2 : owner,
    citizen X1 = norwegian -> house X2 = blue -> next_to X1 X2.

Axiom clue15: (* The man who smokes Blends lives next to the man who drinks water. *)
  forall X1 X2 : owner,
    smoke X1 = blends -> drink X2 = water -> next_to X1 X2.

Coq 8.4pl4で確認した解答の証明はこちら:

five_houses.v

このように証明することで、上から順に補題を追っていけば、15の手掛りをどの段階で使ってパズルを解けばいいかが説明できるようになります。総当りで解いた場合にはそうはいきません。また、この形の定義と公理なら直観主義論理で証明できるということが分かります。ただし、citizen_is_surjectiveなど各関数の全射性を公理とする代わりに、単射性を公理として仮定した場合は(等しい有限基数を持つ集合間の関数なので同値ですが)この限りではなさそうです。

参考


© 2006-2023 fixedpoint.jp