fixedpoint.jp

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.