Coq text adventure

House.v

Set Implicit Arguments.


Inductive Place
 := Kitchen | Bedroom | Hallway | Outside.

Inductive Card := NORTH | EAST | SOUTH | WEST.

Definition moveTo (p : Place) (c : Card) : option Place :=
 match p, c with
 | Hallway, SOUTH => Some Bedroom
 | Hallway, WEST  => Some Outside
 | Hallway, EAST  => Some Kitchen
 | Kitchen, WEST  => Some Hallway
 | Bedroom, NORTH => Some Hallway
 | Outside, EAST  => Some Hallway
 | _, _ => None
 end.

Inductive Move : Place -> Place -> Set
 := Go   : forall a b c dir, moveTo a dir = Some b -> Move b c -> Move a c
  | Stay : forall a, Move a a.

Ltac DESCRIBE room :=
 match room with
 | Kitchen => idtac "You are in a cramped, claustrophobic kitchen. You can see the tiles peeling off the walls. A hallway leads WEST."
 | Hallway => idtac "You are in a cramped, claustrophobic hallway. The hallway continues EAST and WEST, while there is an open door SOUTH."
 | Bedroom => idtac "You are in a cramped, claustrophobic bedroom. Exits are NORTH."
 | Outside => idtac "You are outside. Exits are WEST."
 end.


Ltac OK   := match goal with
 | |- Move ?a ?a
  => apply Stay;
     idtac "You win!"
 end.

Ltac GO X :=
   let x  := fresh "X"
in let hx := fresh "HX"
in match goal with
   | |- Move ?a _ =>
     remember (moveTo a X) as x eqn:hx;
     destruct x; inversion hx
  end;
  subst;
  match goal with
   | _ : (Some ?bbb = moveTo ?aaa _) |- _
   => apply Go with (a := aaa) (b := bbb) (dir := X)
   | _ : None = moveTo _ _ |- _
   => idtac "There is no exit to the" X
  end;
  try assumption;
  try OK;
  clear hx;
  match goal with
  | |- Move ?a _ =>
      DESCRIBE a
  end.

Ltac START :=
  match goal with
  | |- Move ?a _ => DESCRIBE a
  end.

Theorem x : Move Kitchen Outside.
Proof.
 START.
 GO SOUTH.