einstein.why 3.85 KB
Newer Older
1 2 3 4 5 6 7 8 9 10
(*
   This problem is usually referred to as Einstein's Logic Problem.
   see http://en.wikipedia.org/wiki/Zebra_Puzzle
   (contribution by Stéphane Lescuyer)
*)

theory Bijection
  type t
  type u

11
  logic of t : u
12
  logic to_ u : t
13

14 15
  axiom To_of : forall x : t. to_ (of x) = x
  axiom Of_to : forall y : u. of (to_ y) = y
16 17 18 19
end

theory Einstein "Einstein's problem"
  (* Types *)
20 21
  type house  = H1 | H2 | H3 | H4 | H5
  type color  = Blue | Green | Red | White | Yellow
22
  type person = Dane | Englishman | German | Norwegian | Swede
23 24 25
  type drink  = Beer | Coffee | Milk | Tea | Water
  type cigar  = Blend | BlueMaster | Dunhill | PallMall | Prince
  type pet    = Birds | Cats | Dogs | Fish | Horse
26 27 28 29 30 31 32 33
  
  (* Each house is associated bijectively to a color and a person *)
  clone Bijection as Color with type t = house, type u = color
  clone Bijection as Owner with type t = house, type u = person

  (* Each drink, cigar brand and pet are associated bijectively to a person *)
  clone Bijection as Drink with type t = person, type u = drink
  clone Bijection as Cigar with type t = person, type u = cigar
34
  clone Bijection as Pet   with type t = person, type u = pet
35 36

  (* Relative positions of the houses *)
37
  logic leftof (h1 h2 : house) =
38
    match h1, h2 with
39 40 41
    | H1, H2 
    | H2, H3 
    | H3, H4 
42
    | H4, H5 -> true
43
    | _      -> false
44
    end
45 46
  logic rightof (h1 h2 : house) =
    leftof h2 h1
47
  logic neighbour (h1 h2 : house) =
48
    leftof h1 h2 or rightof h1 h2
49 50
end

51
theory EinsteinClues "Clues"
52 53 54
  use import Einstein

  (* The Englishman lives in a red house *)
55
  axiom Clue1: Color.of (Owner.to_ Englishman) = Red
56 57

  (* The Swede has dogs *)
58
  axiom Clue2: Pet.of Swede = Dogs
59 60

  (* The Dane drinks tea *)
61
  axiom Clue3: Drink.of Dane = Tea
62 63

  (* The green house is on the left of the white one *)
64
  axiom Clue4: leftof (Color.to_ Green) (Color.to_ White)
65 66

  (* The green house's owner drinks coffee *)
67
  axiom Clue5: Drink.of (Owner.of (Color.to_ Green)) = Coffee
68 69

  (* The person who smokes Pall Mall has birds *)
70
  axiom Clue6: Pet.of (Cigar.to_ PallMall) = Birds
71 72

  (* The yellow house's owner smokes Dunhill *)
73
  axiom Clue7: Cigar.of (Owner.of (Color.to_ Yellow)) = Dunhill
74 75

  (* In the house in the center lives someone who drinks milk *)
76
  axiom  Clue8: Drink.of (Owner.of H3) = Milk
77 78

  (* The Norwegian lives in the first house *)
79
  axiom Clue9: Owner.of H1 = Norwegian
80 81

  (* The man who smokes Blends lives next to the one who has cats *)
82
  axiom Clue10: neighbour 
83
    (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Pet.to_ Cats))
84 85

  (* The man who owns a horse lives next to the one who smokes Dunhills *)
86
  axiom Clue11: neighbour
87
    (Owner.to_ (Pet.to_ Horse)) (Owner.to_ (Cigar.to_ Dunhill))
88 89

  (* The man who smokes Blue Masters drinks beer *)
90
  axiom Clue12:
91
    Drink.of (Cigar.to_ BlueMaster) = Beer
92 93

  (* The German smokes Prince *)
94
  axiom Clue13:
95
    Cigar.of German = Prince
96 97

  (* The Norwegian lives next to the blue house *)
98
  axiom Clue14:
99
    neighbour (Owner.to_ Norwegian) (Color.to_ Blue)
100 101

  (* The man who smokes Blends has a neighbour who drinks water *)
102
  axiom Clue15:
103
    neighbour (Owner.to_ (Cigar.to_ Blend)) (Owner.to_ (Drink.to_ Water))
104 105 106 107 108

end

theory Goals "Goals about Einstein's problem"
  use import Einstein
109
  use import EinsteinClues
110

111 112 113 114 115 116 117 118 119 120 121 122 123 124
(*
  lemma First_House_Not_White: Color.of H1 <> White
  lemma Last_House_Not_Green: Color.of H5 <> Green

  lemma Blue_not_Red: Blue <> Red
  lemma Englishman_not_H2: Owner.to_ Englishman <> H2
  lemma Englishman_not_H1: Owner.to_ Englishman <> H1

  lemma Second_House_Blue: Color.of H2 = Blue
  lemma Green_H4 : Color.of H4 = Green
  lemma White_H5 : Color.of H5 = White
  lemma Red_H3 : Color.of H3 = Red
  lemma Yellow_H1 : Color.of H1 = Yellow
*)
MARCHE Claude's avatar
MARCHE Claude committed
125
  goal G1: Pet.to_ Fish = German
126 127
  goal Wrong: Pet.to_ Cats = Swede 
  goal G2: Pet.to_ Cats = Norwegian
128 129 130 131 132 133 134 135

end

(*
Local Variables: 
compile-command: "make -C .. examples/einstein.gui"
End: 
*)