Module Damier_ex

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


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

         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 ab c)
                           | B Þ (Triple a (f bc)
                           | 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 : color ® color := 
   [c]Cases c of White Þ Black | Black Þ White end.

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

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

Definition turn_line : pos ® board ® board := 
   [p](triple_map_select (triple_map turn_colorp).

Definition turn_col : pos ® board ® board := 
   [p](triple_map (triple_map_select turn_color p)).

Definition proj_board : pos ® pos ® board ® color :=
         [x,y,b](proj_triple y (proj_triple x b)).

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

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

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

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

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

* Alternative sans définition inductive :
Definition move2 : board ® board ® Prop := 
         [b1,b2](EX p : pos | b2=(turn_line p b1)) or 
                 (EX p : pos | b2=(turn_col p b1)).

Lemma move2_line : (b1:board)(p:pos)(moveb1 (turn_line p b1)).
IntrosLeftExists pTrivial.
Save.

Inductive moves [b1:board]: board ® Prop := 
   moves_init : (moves bb1)
moves_step : (b2,b3:board)(moves bb2) ® (move bb3) ® (moves bb3).

Hints Resolve move_line move_col moves_init moves_step.

Lemma move_moves : (b1,b2:board)(move bb2) ® (moves bb2).
IntrosApply moves_step with b1; Trivial.
Save.

Lemma moves_trans 
         : (b1,b2,b3:board)(moves bb2)®(moves bb3)®(moves bb3).
Induction 2; EAuto.
Save.
Hints Resolve move_moves moves_trans.

* **Propriétés Target est accessible à partir de start
Lemma acessible : (moves start target).
Apply moves_step with (turn_line A start); Auto.
Replace target with (turn_line B (turn_line A start)); Auto.
Save.

* White_board n'est pas accessible à partir de start
Require Bool.

Definition diff_color : color ® color ® bool :=
   [c1,c2:color
       Cases ccof Black White Þ true
                   | White Black Þ 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 : 
           (b1,b2:board)(move bb2) ® (odd_board b1) = (odd_board b2).

* On regarde tous les cas possibles
Unfold odd_board;Destruct 1;
Case b1; Intros lll3; Case l1; Intros xxx3;
Case l2; Intros yyy3; Case l3; Intros zzz3;
Destruct pSimplCase x1; Case x3; Case z1; Case z3;
Simpl;Intros;Contradiction Orelse Auto.

Save.

Hints Resolve odd_invariant_move.

Lemma odd_invariant_moves : 
               (b1,b2:board)(moves bb2) ® (odd_board b1) = (odd_board b2).

Induction 1;Intros;Trivial.
Transitivity (odd_board b0);Auto.
Save.

Hints Resolve odd_invariant_moves.

Lemma not_accessible : not(moves start white_board).
Red;Intro.
Cut (not(odd_board start)=(odd_board white_board));Auto.
Compute.
Discriminate.
Save.


1   Index


This document was translated from LATEX by HEVEA.