(**************************************************************************)
(*                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 := Black : color | White : color.

Definition turn_color : color -> color := [c]
  Cases c of
    White => Black
  | Black => White
  end.

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


Lemma turn_turn_nic : (c:color)(turn_color (turn_color c))=c.
NewDestruct c;Auto.
Save.

Hint Rewrite [turn_turn_nic] in colors.

(* 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 := Triple :  M -> M -> M -> triple.

        (* 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 := [p,t]
      	  Cases t of (Triple a b c) =>
	    Cases p of
	      A => a
      	    | B => b
	    | C => c
	    end
	  end.

        Variable f : M -> M.

        Definition triple_map : triple -> triple := [t]
	  Cases t of (Triple a b c) => (Triple (f a) (f b) (f c)) end.

        Definition triple_map_select : pos -> triple -> triple := [p,t]
	  Cases t of (Triple a b c) =>
	    Cases p of
	      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 :*)

(* III- Damier *)

Definition board := (triple (triple color)).

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

Definition start : board := (Triple ? 
  (Triple ? White White Black)
  (Triple ? White Black Black)
  (Triple ? Black Black Black)).

Definition target : board := (Triple ?
  (Triple ? Black Black White)
  (Triple ? Black White White)
  (Triple ? Black Black Black)).

Definition proj_board : pos -> pos -> board -> color := [p1,p2,b]
  (proj_triple ? p1 (proj_triple ? p2 b)).

Definition turn_line : pos -> board -> board :=
  (triple_map_select ? (triple_map ? turn_color)).

Definition turn_col : pos -> board -> board := [p]
  (triple_map ? (triple_map_select ? turn_color p)).


(* Test *)

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

(* IV-Déplacement *)

Inductive move [b1:board] : board -> Prop :=
  move_line : (p:pos) (move b1 (turn_line p b1))
| move_col  : (p:pos) (move b1 (turn_col p b1)).

Hints Resolve move_line move_col.
(*
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_init : (moves b1 b1)  
| moves_step : (b2,b3:board)(moves b1 b2) -> (move b2 b3) -> (moves b1 b3).

Hints Resolve moves_init moves_step.

Lemma move_moves : (b1,b2:board)(move b1 b2) -> (moves b1 b2).
EAuto.
Save.



Lemma moves_trans 
  : (b1,b2,b3:board)(moves b1 b2)->(moves b2 b3)->(moves b1 b3).
NewInduction 2; EAuto.
Save.

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


Lemma moves_symm :
  (b1,b2:board)(moves b1 b2) -> (moves b2 b1).
NewInduction 1.
Auto.

Apply moves_trans with b2:=b2; Auto.
Constructor 2 with b2:=b3; Auto.
Case H0.
Intro.
Cut b2=(turn_line p (turn_line p b2)).
Intro.
Pattern 2 b2.
Rewrite H1.
Auto.

Case b2.
Case p.
Destruct t.
Unfold turn_line triple_map_select triple_map.
Intros.
AutoRewrite [colors].
Reflexivity.

Destruct t0.
Unfold turn_line triple_map_select triple_map.
Intros.
AutoRewrite [colors].
Reflexivity.

Destruct t1.
Unfold turn_line triple_map_select triple_map.
Intros.
AutoRewrite [colors].
Reflexivity.

Intro.
Cut b2=(turn_col p (turn_col p b2)).
Intro.
Pattern 2 b2.
Rewrite H1.
Auto.

Case b2.
Case p;Destruct t; Destruct t0; Destruct t1;
Unfold turn_col triple_map_select triple_map;
Intros;
AutoRewrite [colors];
Reflexivity.

Save.


Hints Immediate moves_symm.

(* Target est accessible à partir de start *)

Lemma acessible : (moves start target).
Replace target with (turn_line A (turn_line B start)); EAuto.
Save.

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

Definition is_White : color -> bool := [c]
  Cases c of 
    White => true
  | Black => false
  end.

Require Bool.

Definition odd_board : board -> bool := [b]
  (xorb (is_White (proj_board A A b)) 
  (xorb (is_White (proj_board A C b))
  (xorb (is_White (proj_board C A b))
      	(is_White (proj_board C C b)) ))). 

Eval Compute in (odd_board start).
Eval Compute in (odd_board white_board).

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

NewDestruct 1; Case b1; Case p; Intros; Case t; Case t1; Intros.

(* linie *)

Case c; Case c1; Case c2; Case c4; Auto.

Auto.

Case c; Case c1; Case c2; Case c4; Auto.

(* kolumny *)

Case c; Case c1; Case c2; Case c4; Auto.

Auto.

Case c; Case c1; Case c2; Case c4; Auto.

Save.


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

EApply trans_eq.
Apply IHmoves.

Apply odd_invariant_move.
Assumption.

Save.

Lemma not_accessible : ~(moves start white_board).
Intro.
Absurd (odd_board start)=(odd_board white_board).

Auto with bool.

Apply odd_invariant_moves.
Auto.
Save.


Definition Cannonical := [b:board]
 (proj_board A A b)=White /\ (proj_board A B b)=White /\ (proj_board A C b)=White 
  /\ (proj_board B A b)=White /\ (proj_board C A b)=White.


Definition setAA := [b:board]   
  Cases (proj_board A A b) of
           Black => (turn_col A b)
         | White => b 
  end.

Definition setBA := [b:board]
   Cases (proj_board B A b) of
           Black => (turn_col B b)
         | White => b 
   end.

Definition setCA := [b:board]
   Cases (proj_board C A b) of
           Black => (turn_col C b)
         | White => b 
   end.

Definition setAB := [b:board]
   Cases (proj_board A B b) of
           Black => (turn_line B b)
         | White => b 
   end.

Definition setAC := [b:board]
   Cases (proj_board A C b) of
           Black => (turn_line C b)
         | White => b 
   end.

Definition normalize := [b:board](setAC(setAB(setCA(setBA(setAA b))))).


(*Definition normalize := [b:board]
 let b = 
   Cases (proj_board A A b) of
           Black => (turn_col A b)
         | White => b 
   end
 in
 let b = 
   Cases (proj_board B A b) of
           Black => (turn_col B b)
         | White => b 
   end
 in
 let b = 
   Cases (proj_board C A b) of
           Black => (turn_col C b)
         | White => b 
   end
 in
 let b = 
   Cases (proj_board A B b) of
           Black => (turn_line B b)
         | White => b 
   end
 in
 let b = 
   Cases (proj_board A C b) of
           Black => (turn_line C b)
         | White => b 
   end
 in
   b.
*)

Lemma normalize_cannonical : (b:board)(Cannonical (normalize b)).

Destruct b.
Destruct t;
Destruct c;Destruct c0;Destruct c1;
Destruct t0; Destruct c2;
Destruct t1;Destruct c5;
Compute;Auto.
Save.

Lemma normalized_accessible : (b:board)(moves b (normalize b)).

Unfold normalize.

Intro.
Apply moves_trans with b2:=(setAA b).
Unfold setAA.
Generalize (proj_board A A b).
Destruct c;EAuto.
Generalize (setAA b).
Clear b.

Intro.
Apply moves_trans with b2:=(setBA b).
Unfold setBA.
Generalize (proj_board B A b).
Destruct c;EAuto.
Generalize (setBA b).
Clear b.


Intro.
Apply moves_trans with b2:=(setCA b).
Unfold setCA.
Generalize (proj_board C A b).
Destruct c;EAuto.
Generalize (setCA b).
Clear b.

Intro.
Apply moves_trans with b2:=(setAB b).
Unfold setAB.
Generalize (proj_board A B b).
Destruct c;EAuto.
Generalize (setAB b).
Clear b.

Intro.
Apply moves_trans with b2:=(setAC b).
Unfold setAC.
Generalize (proj_board A C b).
Destruct c;EAuto.

Auto.

Save.

Hints Resolve normalized_accessible.


Lemma normalize_not_moves_canonical : 
 (b:board)(Cannonical b) -> (normalize b)=b.
Intros.
Unfold Cannonical in H.
Decompose [and] H.
Unfold normalize.
Unfold setAA.
Rewrite H0.
Unfold setBA.
Rewrite H3.
Unfold setCA.
Rewrite H5.
Unfold setAB.
Rewrite H2.
Unfold setAC.
Rewrite H1.
Reflexivity.
Save.


Lemma normalize_invariant : 
 (b,b1:board)(moves b b1) -> (normalize b)=(normalize b1).
NewInduction 1.
Auto.

Rewrite IHmoves.
Case H0;
NewDestruct p;Case b2;
Destruct t;
Destruct c;Destruct c0;Destruct c1;
Destruct t0;
Destruct c2;Destruct c3;Destruct c4;
Destruct t1;
Destruct c5;Destruct c6;Destruct c7;
Auto.

Save.

Hints Resolve normalize_invariant.

Lemma unique_cannonical : (b1,b2:board)(Cannonical b1) -> (Cannonical b2) -> (moves b1 b2) -> b1=b2.
Intros.
Cut (normalize b1)=(normalize b2).
Intro.
Rewrite <- normalize_not_moves_canonical with b:=b1; Auto.
Rewrite H2.
Apply normalize_not_moves_canonical; Auto.
Apply normalize_invariant; Auto.
Save.

Lemma normalize_divides : (b1,b2:board)(normalize b1)=(normalize b2) -> (moves b1 b2).
Intros.
Apply moves_trans with b2:=(normalize b1).
Auto. 
Rewrite H.
Auto.
Save.

Hints Resolve normalize_divides.

Lemma color_eq : (c1,c2:color){c1=c2}+{~c1=c2}.
Intros.
Decide Equality c1 c2.
Defined.

Hints Resolve color_eq.

Lemma triple_eq : (t1,t2:(triple color)){t1=t2}+{~t1=t2}.
Intros.
Decide Equality t1 t2;Auto.
Defined.

Hints Resolve triple_eq.


Lemma board_eq : (b1,b2:board){b1=b2}+{~b1=b2}.
Intros.
Decide Equality b1 b2.
Defined.

Hints Resolve board_eq.

Lemma moves_dec : (b1,b2:board){moves b1 b2}+{~(moves b1 b2)}.
Intros.
Cut {(normalize b1)=(normalize b2)}+{~(normalize b1)=(normalize b2)}.
Intro.
Case H.
Intro.
Left.
Auto.
Intro.
Right.
Auto.

Auto.

Defined.

Require Extraction.

Extract Inductive sumbool => bool [true false].
Set Extraction Optimize. 
Recursive Extraction moves_dec.

Eval Compute in (moves_dec start white_board).