Set Implicit Arguments.

Require Import board.

(** Proving forall b: board, P(b) by a brute-force approach *) 
(** Tactic to destruct a board *)
Ltac triple_force tac t := 
    let x := fresh "x" in 
    let y := fresh "y" in
    let z := fresh "z" in
    destruct t as (x,y,z); tac x; tac y; tac z.

Ltac board_force tac t := 
    let tac1 := triple_force tac in
    triple_force tac1 t.

Ltac bool_force tac t := destruct t; tac.

Ltac nothing x := idtac.

Ltac finish := compute; trivial.

Ltac bool_force_compute := bool_force finish.
Ltac bool_force_idtac := bool_force idtac.

Lemma commute_col_row : forall p q b, 
   turn_col p (turn_row q b) = turn_row q (turn_col p b).
Time destruct p; destruct q; board_force bool_force_compute b.
Save.

(** Other version using small reflexion *)

Definition repr (b:bool) (P:Prop) := b = true -> P.

Definition repr_forall A (b:bool) (P:A -> Prop) := 
           repr b (forall x:A,P x).

Definition enum A (red : (A -> bool) -> bool) :=
           forall (P: A -> Prop) (f: A -> bool),
           (forall x, repr (f x) (P x)) 
           -> repr (red f) (forall x, P x).

Definition enum_color (boolP : color -> bool) : bool := 
           boolP White && boolP Black.

Lemma enum_color_ok : enum enum_color.
unfold enum_color; intros P boolP H Hr.
destruct (andb_prop _ _ Hr) as (Hw,Hb); clear Hr.
destruct x; apply H; auto.
Save.
Hint Resolve enum_color_ok.

Definition enum_pos (boolP : pos -> bool) : bool := 
           boolP A && boolP B && boolP C.

Lemma enum_pos_ok : enum enum_pos.
unfold enum_pos; intros P boolP H Hr.
destruct (andb_prop _ _ Hr) as (H',HC); clear Hr.
destruct (andb_prop _ _ H') as (HA,HB); clear H'.
destruct x; apply H; auto.
Save.
Hint Resolve enum_pos_ok.

Definition enum_triple M 
    (enumM: (M -> bool)-> bool) (boolP:triple M -> bool) := 
    enumM (fun x => enumM (fun y => enumM (fun z => boolP [x|y|z]))). 
  

Lemma enum_triple_ok : forall M (enumM:(M->bool)->bool), 
      enum enumM -> enum (enum_triple enumM).
unfold enum_color; intros M enumM He P boolP H Hr x.
case x.
generalize Hr; clear Hr.
change (repr (enum_triple enumM boolP) (forall m m0 m1 : M, P [m | m0 | m1])).
unfold enum_triple.
apply He.
intro x0.
apply He.
intro x1.
apply He; auto.
Save.
Hint Resolve enum_triple_ok.

Definition enum_board : (board -> bool) -> bool 
           := enum_triple (enum_triple enum_color).

Lemma enum_board_ok : enum enum_board.
unfold enum_board.
apply enum_triple_ok; auto.
Save.

Definition repr_eq A (eqb : A -> A -> bool) : Prop
           := forall x y : A,  repr (eqb x y) (x = y).
 
Definition eqb_color (b1 b2:color) : bool := 
   match (b1,b2) with (Black,Black) => true | (White,White) => true 
                    | _ => false end.

Lemma eqb_color_ok : repr_eq eqb_color.
intros x y; destruct x; destruct y; compute; auto; discriminate.
Save.
Hint Resolve eqb_color_ok.

Definition eqb_triple M (eqbM: M -> M -> bool) (x y : triple M) := 
    let (x1,x2,x3):= x in
    let (y1,y2,y3):= y in
    eqbM x1 y1 && eqbM x2 y2 && eqbM x3 y3.

Lemma eqb_triple_ok : 
    forall M (eqbM:M -> M -> bool), 
              repr_eq eqbM -> repr_eq (eqb_triple eqbM).
intros M eqbM H (x1,x2,x3) (y1,y2,y3); simpl; intro H1.
destruct (andb_prop _ _ H1) as (H',H3); clear H1.
destruct (andb_prop _ _ H') as (H1,H2); clear H'.
rewrite (H _ _ H1); trivial.
rewrite (H _ _ H2); trivial.
rewrite (H _ _ H3); trivial.
Save.
Hint Resolve eqb_triple_ok.

Definition eqb_board := eqb_triple (eqb_triple eqb_color).

Lemma eqb_board_ok : repr_eq eqb_board.
unfold eqb_board; auto.
Save.

Definition eq_board_fun f g :=
      enum_board (fun b => eqb_board (f b) (g b)).

Lemma eq_board_fun_ok (f g:board -> board) : 
  repr (eq_board_fun f g) (forall (b:board), f b = g b).
unfold eq_board_fun.
apply enum_board_ok; intro b.
apply eqb_board_ok.
Save.
Hint Resolve eq_board_fun_ok.

Definition eq_board_fun1 f g :=
      enum_pos (fun p => eq_board_fun (f p) (g p)).

Lemma eq_board_fun1_ok f g  : 
    repr (eq_board_fun1 f g) (forall p (b:board), f p b = g p b).
unfold eq_board_fun1.
apply enum_pos_ok; intro p; auto.
Save.
Hint Resolve eq_board_fun1_ok.

Definition eq_board_fun2 f g :=
      enum_pos (fun p => eq_board_fun1 (f p) (g p)).

Lemma eq_board_fun2_ok f g  : 
    repr (eq_board_fun2 f g) (forall p q (b:board), f p q b = g p q b).
unfold eq_board_fun2.
apply enum_pos_ok; intro p; auto.
Save.
Hint Resolve eq_board_fun2_ok.

Lemma commute_col_row1 : forall p q b, 
   turn_col p (turn_row q b) = turn_row q (turn_col p b).
cut (eq_board_fun2 (fun p q b => turn_col p (turn_row q b)) 
                     (fun p q b => turn_row q (turn_col p b))=true).
apply eq_board_fun2_ok.
compute; trivial.
Time Save.

(* Decision procedure for moves *)

(** ** Normalisation function on boards *)
(**  turns rows and columns to get only white tokens 
      on first row and column *)

(** - forces a white token on the first square of row p *)
Definition force_white_row (p: pos) (b:board) : board := 
	match proj_board p A b 
        with White => b | Black => turn_row p b
	end.

Lemma force_white_row_moves 
 : forall (p:pos)(b:board), moves b (force_white_row p b).
unfold force_white_row;intros.
case (proj_board p A b); auto.
Save.

(** - forces a white token on the first square of column p *)
Definition force_white_col (p: pos) (b: board) : board := 
	match proj_board A p b with 
        White => b |Black => turn_col p b
	end.


Lemma force_white_col_moves :
  forall (p:pos) (b:board), moves b (force_white_col p b).
intros p b.
unfold force_white_col; intros.
case (proj_board A p b); auto.
Save.
Hint Resolve force_white_col_moves.

(** - force white tokens on first row and column *)
Definition force_white ( b: board) : board := 
 force_white_row B
	(force_white_row C 
	(force_white_col A 
	(force_white_col B 
	(force_white_col C b)))).

Hint Resolve force_white_row_moves force_white_col_moves.

(** - normalisation function preserves moves  *)

Lemma force_white_moves : forall (b:board), moves b (force_white b).
intros; unfold force_white.
apply moves_trans with (force_white_col C b); auto.
apply moves_trans with (force_white_col B (force_white_col C b)); auto.
apply moves_trans with (force_white_col A (force_white_col B 
	   			(force_white_col C b))); auto.
apply moves_trans with (force_white_row C (force_white_col A 
			(force_white_col B (force_white_col C b)))); auto.
Save.
Hint Resolve force_white_moves.

(** Two boards with the same normal form are in the same orbit *)
(** Involution f if f o f = id   *)
(* [turn_row] and [turn_col] are involutions.
    We first prove that [triple_map] and [triple_map_select] 
    preserves involution, and [turn_color] is an involution *)

Definition involution (M : Set) (f:M -> M) 
     := forall (x:M), f (f x)=x.

Lemma triple_map_inv 
 : forall (M:Set) (f: M -> M), involution f -> involution (triple_map f).
red; intros.
case x; simpl.
intros; repeat rewrite H; trivial.
Save.

Lemma triple_map_select_inv 
 : forall (M:Set) (f:M -> M) (p:pos),
     involution f -> involution (triple_map_select f p).
red; intros.
case x; case p; simpl; intros; rewrite H; trivial.
Save.

Lemma turn_color_inv : involution turn_color.
red.
destruct x; trivial.
Save.

Hint Resolve triple_map_inv triple_map_select_inv turn_color_inv.

Lemma turn_row_inv : forall p:pos, involution (turn_row p).
unfold turn_row, board; auto.
Save.

Lemma turn_col_inv : forall p:pos, involution (turn_col p).
unfold turn_col, board; auto.
Save.

(** ** Symmetry of relations move and moves *)

Lemma move_sym : forall (b1 b2:board), move b1 b2 -> move b2 b1.
destruct 1; intros.
pattern b1 at 2; replace b1 with (turn_row p (turn_row p b1)); auto.
apply (turn_row_inv p).
pattern b1 at 2; replace b1 with (turn_col p (turn_col p b1)); auto.
apply (turn_col_inv p).
Save.
Hint Immediate move_sym.

Lemma moves_sym : 
  forall (b1 b2:board), moves b1 b2 -> moves b2 b1.
induction 1; intros.
auto.
apply moves_trans with b2; auto.
Save.
Hint Immediate moves_sym.


Lemma force_eq_moves 
	: forall (b1 b2:board), force_white b1 = force_white b2 -> moves b1 b2.
intros; apply moves_trans with (force_white b1); auto.
rewrite H; auto.
Save.

(** Other direction : the board after a move has the same normal form *)
(** ** Invariant *)
(** An  invariant is a function preserved by moves *)

Definition invariant (M:Set) (f:board -> M) :=
	forall b1 b2:board, moves b1 b2 -> f b1 = f b2.

Lemma invariant_move : forall (M:Set)(f:board -> M),
        (forall (b1 b2:board), move b1 b2 -> f b1 = f b2)
	-> invariant f.
red; induction 2; intros; trivial.
transitivity (f b2); auto.
Save.
Hint Resolve invariant_move.

Lemma invariant_not_moves : forall (M:Set)(f:board->M), 
  invariant f
   -> forall (b1 b2:board), ~ f b1 = f b2 -> ~ moves b1 b2.
red; eauto.
Save.


Lemma move_force_eq 
	: forall (b1 b2:board), move b1 b2 -> force_white b1 = force_white b2. 
destruct 1.
generalize p b1.
cut (eq_board_fun1 (fun p b => force_white b)
                   (fun p b => force_white (turn_row p b)) = true).
apply eq_board_fun1_ok.
compute; trivial.
generalize p b1.
cut (eq_board_fun1 (fun p b => force_white b)
                   (fun p b => force_white (turn_col p b)) = true).
apply eq_board_fun1_ok.
compute; trivial.
Save.

Lemma moves_force_eq 
	: forall (b1 b2:board), moves b1 b2 -> force_white b1 = force_white b2. 
change (invariant force_white).
apply invariant_move.
exact move_force_eq.
Save.

Lemma force_eq_not_moves : forall (b1 b2:board), 
      force_white b1 <> force_white b2 -> ~ moves b1 b2.
intros b1 b2 H1 H2; apply H1; apply moves_force_eq; auto.
Save.

(** ** Equivalence between relation moves and equality of normal forms *)
(** We decide relation [moves] by deciding equality of normal forms *)

Lemma accessible_auto : moves start target.
apply force_eq_moves; reflexivity.
Save.

Lemma not_accessible_auto : ~ moves start white_board.
apply force_eq_not_moves; compute; discriminate.
Save.