(** Sur un damier 3x3 sont posés 9 pions bicolores (une face blanche, une 
    face noire). Les pions peuvent être retournés par ligne ou par colonne.
    Il s'agit d'étudier les positions atteignables à partir d'un état      
    initial                                                                
*)

Set Implicit Arguments.

(** **Triplets 
      On modélise la notion de triplet d'objets d'un type quelconque M, 
      un damier sera représenté comme un triplet de triplet de booléens 
      représentant le pion posé sur la case.
      Un type de pos à trois valeurs [(A,B,C)] permet d'indicer chacune
      des poss dans le triplet.
*)

Section Polymorphic_Triple.

  Variable M : Set.
  
  Inductive triple : Set := Triple : M -> M -> M -> triple.
  
  Definition triple_x (m : M) := Triple m m m.

  Inductive pos : Set := A : pos | B : pos | C : pos.

(** Fonction de projection d'un triplet suivant une pos *)
  Definition proj_triple (p : pos)(t : triple) : M :=
    match t with
      |Triple a b c =>
        match p with
          |A => a
          |B => b
          |C => c
        end
    end.

  Variable f : M -> M.

  Definition triple_map (t : triple) : triple :=
    match t with
      |Triple a b c => Triple (f a) (f b) (f c)
    end.

  Definition triple_map_select (p : pos)(t : triple) : triple :=
    match t with
      |Triple a b c =>
        match p with
          |A => Triple (f a) b c
          |B => Triple a (f b) c
          |C => Triple a b (f c)
        end
    end.

End Polymorphic_Triple.

(** Observer le type des objets définis après la fermeture de la section.*)

(** **Couleurs 
 on modélise la notion de couleur comme un type color 
à deux éléments [Black] et [White]*)
Inductive color : Set := White : color | Black : color.

Definition turn_color (c : color) : color := 
  match c with | White => Black | Black => White end.

(** Tester la fonction définie *)
Eval compute in (turn_color White).

(** **Damier : un triplet (3 lignes) de colonnes *)
Definition board := (triple (triple color)).

Definition proj_board (c l : pos) (b : board) : color :=
	(proj_triple l (proj_triple c b)).

Definition turn_line (p : pos)(b : board) : board := 
  triple_map_select (triple_map turn_color) p b.

Definition turn_col (p : pos)(b : board) : board := 
  triple_map (triple_map_select turn_color p) b.

(** **Test *)

Definition white_board : board 
	:= (triple_x (triple_x White)).

Eval compute in (turn_line A (turn_col B white_board)).

(* Configuration de départ *)
Definition start : board 
	:= (Triple (Triple White White Black)
		   (Triple Black White White)
		   (Triple Black Black Black)).

(* Configuration d'arrivée *)
Definition target : board 
	:= (Triple 
		(Triple Black Black White)
		(Triple White Black Black)
		(Triple Black Black Black)).

(** **Déplacement licite *)
Inductive move (b1:board) : board -> Prop :=
  move_line : forall p:pos, (move b1 (turn_line p b1))
| move_col  : forall p:pos, (move b1 (turn_col p b1)).

(** Alternative sans définition inductive : *)
Definition move2 (b1 b2 : board) : Prop := 
  exists p : pos, b2 = (turn_line p b1) \/
  exists p : pos, b2 = (turn_col p b1).

Lemma move2_line : forall (b1:board)(p:pos), move2 b1 (turn_line p b1).
Proof.
intros b1 p; unfold move2.
exists p; left.
trivial.
Qed.

(* Issu d'une suite de déplacements licites à partir de b1 *)
Inductive moves (b1:board) : board -> Prop := 
  moves_init : (moves b1 b1)
| moves_step : forall b2 b3:board, (move b1 b2) -> (moves b2 b3) -> (moves b1 b3).

(*Hints Resolve move_line move_col moves_init moves_step.*)

Lemma move_moves : forall b1 b2:board, move b1 b2 -> (moves b1 b2).
intros; apply moves_step with b2; trivial; constructor.
Qed.

Lemma moves_trans : forall b1 b2 : board, 
  moves b1 b2 -> forall  b3 : board, moves b2 b3 -> moves b1 b3.
intros b1 b2 h1; elim h1; trivial.
intros b3 b4 b5 mb34 mb45 Ih b6 mb56.
apply moves_step with b4; trivial.
apply Ih.
trivial.
Qed.

(** **Propriétés
  [Target] est accessible à partir de [start] *)
Lemma acessible : moves start target.
apply moves_step with (turn_line A start).
  apply move_line.
replace target with (turn_line B (turn_line A start)); trivial.
apply moves_step with (turn_line B (turn_line A start)).
  apply move_line.
constructor.
Qed.
  

(** [White_board] n'est pas accessible à partir de [start] *)
Require Bool.

Definition diff_color (c1 c2 : color) : bool :=
  match c1, c2 with
    |White, Black => true
    |Black, White => true
    |_, _ => false
  end.

Definition odd_board (b : board) := 
      (xorb (diff_color (proj_board A A b) (proj_board A C b))
                     (diff_color (proj_board C A b) (proj_board C C b))).
                     
Eval compute in (odd_board start).
Eval compute in (odd_board target).
Eval compute in (odd_board white_board).

Lemma odd_invariant_move : forall b1 b2,
          (move b1 b2) -> (odd_board b1) = (odd_board b2).
intros b1 b2 h1. unfold odd_board. unfold diff_color; destruct h1;
case b1; intros l1 l2 l3;
case l1; intros x1 x2 x3; case l2; intros y1 y2 y3; case l3; intros z1 z2 z3; destruct p; simpl; case x1; case x3; case z1; case z3; simpl; trivial.
Qed.

(*Hints Resolve odd_invariant_move.*)

Lemma odd_invariant_moves : 
     forall b1 b2:board, moves b1 b2 -> (odd_board b1) = (odd_board b2).
intros b1 b2 h1; induction h1; trivial.
transitivity (odd_board b2); trivial.
apply odd_invariant_move; trivial.
Qed.

Lemma odd_board_val : ~(odd_board start)=(odd_board white_board).
compute.
discriminate.
Qed.

Lemma not_accessible : ~(moves start white_board).
intros h1.
apply odd_board_val.
apply odd_invariant_moves.
trivial.
Qed.

(* constructor, elim, discriminate, trivial,  assert *)