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

(* Na szachownicy 3x3 jest 9 piokow dwukolorowych (z jednej strony  *)
(* biale - z drugiej czarne). Operacje wykonywane na szachownicy to *)
(* odwracanie wszystkich pionkow danego wiersza lub kolumny.        *)
(* Bedziemy badac pozycje osiagalne ze stanu poczatkowego           *)
(* (wszystkie pionki same biale)                                    *)

(* I- Kolory 
      Modelujemy kolory, jako typ color z dwoma elementami  
      Black i White
*)

Inductive color : Set := ...

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

(* Testujemy... *)
Eval Compute in (turn_color White).


(* II- Trojki
      Modelujemy pojecie trojki dowolnego typu M. Szachownica bedzie
      reprezentowana jako trojka trojek kolorow, reprezentujacych
      pionki lezace na odpowiedniej pozycji szachownicy.

      Trzywartosciowy typ pozycji pomaga indeksowac.
*)

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.

(* Zaobserwowac typ obiektow zdefiniowanych w sekcji po jej zamknieciu! *)

(* III- Szachownica *)

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

(*
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 jest dostepny z start *)
Lemma acessible : (moves start target).

(* White_board nie jest dostepny z start *)

(* Tu trzeba wymyslec cos sprytnego... *)

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).