(* A very simple Coq encoding of the "Towers of Hanoi" puzzle game. *)

Require Import Coq.Lists.List.
Import ListNotations.
Require Import Coq.Arith.Compare_dec.


(* Proof of a sorted list *)
Inductive Sorted : list nat -> Prop :=
 | sorted'nil : Sorted []
 | sorted'cons'nil x : Sorted [x]
 | sorted'cons x y xs:
    Sorted (y::xs)
  -> x < y
  -> Sorted (x::y::xs).


(* We have three towers. Each tower is a sorted list of numbers. *)
Inductive Towers : Set :=
 | towers : list nat -> list nat -> list nat -> Towers.

(* A group of towers is valid if all the lists are sorted. *)
Definition Valid (t : Towers) : Prop :=
 match t with
 | towers a b c => Sorted a /\ Sorted b /\ Sorted c
 end.

(* Each tower is given an index from 1 to 3. *)
Inductive Ix : Set :=
  | Ix1
  | Ix2
  | Ix3.

(* Pop the top element off a given tower *)
Definition unconsT (ix : Ix) (t : Towers) : option (nat * Towers) :=
 match ix, t with
 | Ix1, towers (v::vs) b c => Some (v, towers vs b c)
 | Ix2, towers a (v::vs) c => Some (v, towers a vs c)
 | Ix3, towers a b (v::vs) => Some (v, towers a b vs)
 | _,   _                  => None
 end.

(* Push a value onto a given tower.
This requires the new value to be smaller than the current head of the list.
Otherwise it returns 'None'. *)
Definition consT (ix : Ix) (v : nat) (t : Towers) : option Towers :=
  match ix, t with
  | Ix1, towers [] b c => Some (towers [v] b c)
  | Ix1, towers (x::vs) b c =>
    if lt_dec v x
    then Some (towers (v::x::vs) b c)
    else None

  | Ix2, towers a [] c => Some (towers a [v] c)
  | Ix2, towers a (x::vs) c =>
    if lt_dec v x
    then Some (towers a (v::x::vs) c)
    else None

  | Ix3, towers a b [] => Some (towers a b [v])
  | Ix3, towers a b (x::vs) =>
    if lt_dec v x
    then Some (towers a b (v::x::vs))
    else None
  end.

(* Move a value from one tower to another. This can fail if:
  the 'from' tower is empty; or
  the 'from' tower's value is larger than the head of the 'to' tower. *)
Definition shift (from to : Ix) (t : Towers) : option Towers
 := match unconsT from t with
  | None        => None
  | Some (x,t') => consT to x t'
  end.


(* If the towers were sorted and we move a value, the result is still sorted.
This is rather tedious to prove, and conceptually not very interesting. *)
Theorem Valid_shift_Valid t from to t':
    Valid t
 -> shift from to t = Some t'
 -> Valid t'.
Proof.
Admitted.

(* We play a game by making a list of moves *)
Inductive move : Towers -> Towers -> Prop :=
  | MNil t : move t t
  | MCons t from to t' t'':
       shift from to t = Some t'
    -> move t' t''
    -> move t  t''.


(* The tactic "MOVE Ix1 Ix3"
 means "move a value from the top of tower 1 to tower 3" *)
Ltac MOVE f t :=
 eapply MCons with (from := f) (to := t); try reflexivity;
 try solve [apply MNil; idtac "Well done!"].

(* Play a game! *)
Theorem play_3:
  move
    (* Initial state *)
    (towers [1;2;3] [] [])
    (* Goal state *)
    (towers [] [] [1;2;3]).
Proof.
 MOVE _ _.
Admitted.