einstein.why 3.85 KB
 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 `````` Jean-Christophe committed Dec 16, 2010 11 `````` logic of t : u `````` Jean-Christophe Filliatre committed Dec 29, 2010 12 `````` logic to_ u : t `````` 13 `````` `````` Jean-Christophe Filliatre committed Dec 29, 2010 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 *) `````` Jean-Christophe committed Dec 16, 2010 20 21 `````` type house = H1 | H2 | H3 | H4 | H5 type color = Blue | Green | Red | White | Yellow `````` 22 `````` type person = Dane | Englishman | German | Norwegian | Swede `````` Jean-Christophe committed Dec 16, 2010 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 `````` Jean-Christophe committed Dec 16, 2010 34 `````` clone Bijection as Pet with type t = person, type u = pet `````` 35 36 `````` (* Relative positions of the houses *) `````` Jean-Christophe committed Dec 16, 2010 37 `````` logic leftof (h1 h2 : house) = `````` 38 `````` match h1, h2 with `````` Jean-Christophe committed Dec 16, 2010 39 40 41 `````` | H1, H2 | H2, H3 | H3, H4 `````` 42 `````` | H4, H5 -> true `````` Jean-Christophe committed Dec 16, 2010 43 `````` | _ -> false `````` 44 `````` end `````` Jean-Christophe committed Dec 16, 2010 45 46 `````` logic rightof (h1 h2 : house) = leftof h2 h1 `````` 47 `````` logic neighbour (h1 h2 : house) = `````` Jean-Christophe committed Dec 16, 2010 48 `````` leftof h1 h2 or rightof h1 h2 `````` 49 50 ``````end `````` MARCHE Claude committed May 16, 2011 51 ``````theory EinsteinClues "Clues" `````` 52 53 54 `````` use import Einstein (* The Englishman lives in a red house *) `````` MARCHE Claude committed May 16, 2011 55 `````` axiom Clue1: Color.of (Owner.to_ Englishman) = Red `````` 56 57 `````` (* The Swede has dogs *) `````` MARCHE Claude committed May 16, 2011 58 `````` axiom Clue2: Pet.of Swede = Dogs `````` 59 60 `````` (* The Dane drinks tea *) `````` MARCHE Claude committed May 16, 2011 61 `````` axiom Clue3: Drink.of Dane = Tea `````` 62 63 `````` (* The green house is on the left of the white one *) `````` MARCHE Claude committed May 16, 2011 64 `````` axiom Clue4: leftof (Color.to_ Green) (Color.to_ White) `````` 65 66 `````` (* The green house's owner drinks coffee *) `````` MARCHE Claude committed May 16, 2011 67 `````` axiom Clue5: Drink.of (Owner.of (Color.to_ Green)) = Coffee `````` 68 69 `````` (* The person who smokes Pall Mall has birds *) `````` MARCHE Claude committed May 16, 2011 70 `````` axiom Clue6: Pet.of (Cigar.to_ PallMall) = Birds `````` 71 72 `````` (* The yellow house's owner smokes Dunhill *) `````` MARCHE Claude committed May 16, 2011 73 `````` axiom Clue7: Cigar.of (Owner.of (Color.to_ Yellow)) = Dunhill `````` 74 75 `````` (* In the house in the center lives someone who drinks milk *) `````` MARCHE Claude committed May 16, 2011 76 `````` axiom Clue8: Drink.of (Owner.of H3) = Milk `````` 77 78 `````` (* The Norwegian lives in the first house *) `````` MARCHE Claude committed May 16, 2011 79 `````` axiom Clue9: Owner.of H1 = Norwegian `````` 80 81 `````` (* The man who smokes Blends lives next to the one who has cats *) `````` MARCHE Claude committed May 16, 2011 82 `````` axiom Clue10: neighbour `````` Jean-Christophe Filliatre committed Dec 29, 2010 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 *) `````` MARCHE Claude committed May 16, 2011 86 `````` axiom Clue11: neighbour `````` Jean-Christophe Filliatre committed Dec 29, 2010 87 `````` (Owner.to_ (Pet.to_ Horse)) (Owner.to_ (Cigar.to_ Dunhill)) `````` 88 89 `````` (* The man who smokes Blue Masters drinks beer *) `````` MARCHE Claude committed May 16, 2011 90 `````` axiom Clue12: `````` Jean-Christophe Filliatre committed Dec 29, 2010 91 `````` Drink.of (Cigar.to_ BlueMaster) = Beer `````` 92 93 `````` (* The German smokes Prince *) `````` MARCHE Claude committed May 16, 2011 94 `````` axiom Clue13: `````` Jean-Christophe committed Dec 16, 2010 95 `````` Cigar.of German = Prince `````` 96 97 `````` (* The Norwegian lives next to the blue house *) `````` MARCHE Claude committed May 16, 2011 98 `````` axiom Clue14: `````` Jean-Christophe Filliatre committed Dec 29, 2010 99 `````` neighbour (Owner.to_ Norwegian) (Color.to_ Blue) `````` 100 101 `````` (* The man who smokes Blends has a neighbour who drinks water *) `````` MARCHE Claude committed May 16, 2011 102 `````` axiom Clue15: `````` Jean-Christophe Filliatre committed Dec 29, 2010 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 `````` MARCHE Claude committed May 16, 2011 109 `````` use import EinsteinClues `````` 110 `````` `````` MARCHE Claude committed May 16, 2011 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 committed Jan 06, 2011 125 `````` goal G1: Pet.to_ Fish = German `````` MARCHE Claude committed May 16, 2011 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: *)``````