(* Sur un damier 3x3 sont poses 9 pions bicolores (une face blanche, une 
    face noire). Les pions peuvent etre retournes par ligne ou par colonne.
    Il s'agit d'etudier les positions atteignables a partir d'un etat      
    initial                                                                
*)

Set Implicit Arguments.

(*Triplets 
      On modelise la notion de triplet d'objets d'un type quelconque M, 
      un damier sera represente comme un triplet de triplet de booleens 
      representant le pion pose sur la case.
      Un type de position a trois valeurs [(A,B,C)] permet d'indicer chacune
      des positions dans le triplet.
*)
(** **Couleurs 
 on modelise la notion de couleur comme un type color 
a deux elements [Black] et [White]*)

Print bool.

Inductive color : Set := ??? | ???.

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

(** Tester la fonction definie *)
Eval compute in (turn_color White).

Section Polymorphic_Triple.

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

  Inductive pos : Set := ???.

(** 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 => ???
          |B => ???
          |C => ???
        end
    end.

  Variable f : M -> M.

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

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

End Polymorphic_Triple.

(** Observer le type des objets definis après la fermeture de la section.*)
Check ???.

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

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


(* Configuration de depart *)
Definition start : board 
	:= (Triple (Triple White White Black)
		   (Triple Black White White)
		   (Triple Black Black Black)).

(* Configuration d'arrivee *)
Definition target : board 
	:= ???.

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


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 := ???.

(* Un test *)
Eval compute in (turn_line A (turn_col B white_board)).

(* Un deplacement licite *)
Inductive move (b1:board) : board -> Prop :=
  move_line :  forall p:pos, (move b1 (turn_line p b1))
| move_col  : ???

(* Alternative sans definition inductive : *)
Definition move2 (b1 b2 : board) : Prop := 
  exists p : pos, ?? \/ ??

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

Lemma move2_col : ???.

(* Issu d'une suite de deplacements licites a partir de b1 *)
Inductive moves (b1:board) : board -> Prop := 
  moves_init : ??
| moves_step :  ??

(*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.
???
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.
???
Qed.

(** **Proprietes
  [Target] est accessible a partir de [start] *)
Lemma acessible : moves start target.
replace target with ???; trivial.
???
Qed.
  

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

(* La fonction vraie si c1 et c2 sont deux couleurs differentes *)
Definition diff_color (c1 c2 : color) : bool :=
  match c1, c2 with
???
  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).

(* Pour cette preuve, on deplie tous les cas et on les compare*)
Lemma odd_invariant_move : ???
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.


Lemma odd_invariant_moves : ??
intros b1 b2 h1; induction h1; trivial.
??
Qed.

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

Lemma white_bord_not_accessible : ??
???
Qed.