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 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.
* **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_color) p).
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)(move2 b1 (turn_line p b1)).
Intros; Left; Exists p; Trivial.
Save.
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 move_line move_col moves_init moves_step.
Lemma move_moves : (b1,b2:board)(move b1 b2) ® (moves b1 b2).
Intros; Apply moves_step with b1; Trivial.
Save.
Lemma moves_trans
: (b1,b2,b3:board)(moves b1 b2)®(moves b2 b3)®(moves b1 b3).
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 c1 c2 of 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 b1 b2) ® (odd_board b1) = (odd_board b2).
* On regarde tous les cas possibles
Unfold odd_board;Destruct 1;
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;Intros;Contradiction Orelse Auto.
Save.
Hints Resolve odd_invariant_move.
Lemma odd_invariant_moves :
(b1,b2:board)(moves b1 b2) ® (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
-
acessible, X,
- Black (constructor), X,
- board (definition), X,
- color (inductive), X,
- diff_color (definition), X,
- move (inductive), X,
- move2 (definition), X,
- move2_line, X,
- moves (inductive), X,
- moves_init (constructor), X,
- moves_step (constructor), X,
- moves_trans, X,
- move_col (constructor), X,
- move_line (constructor), X,
- move_moves, X,
- not_accessible, X,
- odd_board (definition), X,
- odd_invariant_move, X,
- odd_invariant_moves, X,
- pos (inductive), X,
- proj_board (definition), X,
- proj_triple (definition), X,
- start (definition), X,
- target (definition), X,
- triple (inductive), X,
- Triple (constructor), X,
- triple_map (definition), X,
- triple_map_select (definition), X,
- triple_x (definition), X,
- turn_col (definition), X,
- turn_color (definition), X,
- turn_line (definition), X,
- White (constructor), X,
- white_board (definition), X,
This document was translated from LATEX by HEVEA.