(**************************************************************************)
(*                Le damier de Cachan                                     *)
(*                  Coq V7                                                *)
(**************************************************************************)

(* 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                                                                *)


(* I- Couleurs 
      On modélise la notion de couleur comme un type color à deux éléments 
      Black et White
*)

Inductive color : Set := ...

Definition turn_color : color -> color := ...

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


(* II- 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 position à trois valeurs (A,B,C) permet d'indicer chacune
      des positions dans le triplet.
*)

Section Polymorphic_Triple.

        Variable M : Set.

        Inductive triple : Set := ...

        (* Check Triple : M -> M -> M -> triple. *)

        Definition triple_x : M -> triple := [m](Triple m m m).

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

        (* fonction de projection d'un triplet suivant une position *)
        Definition proj_triple : pos -> triple -> M := ...


        Variable f : M -> M.

        Definition triple_map : triple -> triple := ...

        Definition triple_map_select : pos -> triple -> triple := ...

End Polymorphic_Triple.

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

(* III- Damier *)

Definition board := ...

Definition white_board : board := ...

Definition start : board := ...

Definition target : board := ...

Definition proj_board : pos -> pos -> board -> color := ...

Definition turn_line : pos -> board -> board := ...

Definition turn_col : pos -> board -> board := ...


(* Test *)

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

(* IV-Déplacement *)

(*
Check move : board -> board -> Prop
Check move_line : (b1:board)(p:pos)(move b1 (turn_line p b1))
Check move_col  : (b1:board)(p:pos)(move b1 (turn_col p b1))
*)

Inductive moves [b1:board]: board -> Prop := ...
  
| moves_step : (b2,b3:board)(moves b1 b2) -> (move b2 b3) -> (moves b1 b3).

(* Check moves_init : (b1:board)(moves b1 b1)
   Check move_moves : (b1,b2:board)(move b1 b2) -> (moves b1 b2)
   Check moves_trans 
        : (b1,b2,b3:board)(moves b1 b2)->(moves b2 b3)->(moves b1 b3)
*)

(* Target est accessible à partir de start *)
Lemma acessible : (moves start target).

(* White_board n'est pas accessible à partir de start *)

Definition odd_board : board -> bool := ...

Lemma odd_invariant_move : 
          (b1,b2:board)(move b1 b2) -> (odd_board b1) = (odd_board b2).

Lemma odd_invariant_moves : 
              (b1,b2:board)(moves b1 b2) -> (odd_board b1) = (odd_board b2).

Lemma not_accessible : ~(moves start white_board).