Module Refl_ex

Set Implicit Arguments.

Require damier_ex.

I-Invariant Un invariant est une fonction sur les damiers qui est préservée par les jeux

Definition invariant
         := [M:Set][f:board®M](b1,b2:board)(moves b1 b2)®(f b1)=(f b2).

Lemma invariant_move : (M:Set)(f:board®M)
         ((b1,b2:board)(move b1 b2)®(f b1)=(f b2))
         ®(invariant f).
Red; Induction 2; Intros; Trivial.
Transitivity (f b0); Auto.
Save.
Hints Resolve invariant_move.

Lemma invariant_not_moves : (M:Set)(f:board®M)(invariant f)
         ®(b1,b2:board)not((f b1)=(f b2))®not(moves b1 b2).
Red; EAuto.
Save.

II-Fonctions involutives
On établit que les fonctions turn_line et turn_color sont des
involutions, pour cela on prouve que les fonctions triple_map et
triple_map_select preservent les involutions
Definition involution := [M:Set][f:M®M](x:M)(f (f x))=x.

Lemma triple_map_inv
   : (M:Set)(f:M®M)(involution f)®(involution (triple_map f)).
Red; Intros.
Case x; Simpl.
Intros; Repeat Rewrite H; Trivial.
Save.

Lemma triple_map_select_inv
   : (M:Set)(f:M®M)(p:pos)(involution f)®(involution (triple_map_select f p)).
Red; Intros.
Case x; Case p; Simpl; Intros; Rewrite H; Trivial.
Save.

Lemma turn_color_inv : (involution turn_color).
Red.
Destruct x; Trivial.
Save.

Hints Resolve triple_map_inv triple_map_select_inv turn_color_inv.

Lemma turn_line_inv : (p:pos)(involution (turn_line p)).
Unfold turn_line board; Auto.
Save.

Lemma turn_col_inv : (p:pos)(involution (turn_col p)).
Unfold turn_col board; Auto.
Save.

III - Symétrie des relations move et moves
Lemma move_sym : (b1,b2:board)(move b1 b2)®(move b2 b1).
Destruct 1; Intros.
Pattern 2 b1; Replace b1 with (turn_line p (turn_line p b1)); Auto.
Apply (turn_line_inv p).
Pattern 2 b1; Replace b1 with (turn_col p (turn_col p b1)); Auto.
Apply (turn_col_inv p).
Save.
Hints Immediate move_sym.

Lemma moves_sym : (b1,b2:board)(moves b1 b2)®(moves b2 b1).
Induction 1; Intros; EAuto.
Save.
Hints Immediate moves_sym.

Une fonction de normalisation pour les damiers, on retourne ligne et colonne de manière à n'avoir que des blancs sur la première ligne et colonne
Definition force_white_line : pos ® board ® board :=
         [p,b]Cases (proj_board p A b) of White Þ b
                                         |Black Þ (turn_line p b)
               end.

Lemma force_white_line_moves
         : (p:pos)(b:board)(moves b (force_white_line p b)).
Unfold force_white_line; Intros.
Case (proj_board p A b); Auto.
Save.

Definition force_white_col : pos ® board ® board :=
         [p,b]Cases (proj_board A p b) of White Þ b
                                         |Black Þ (turn_col p b)
               end.

Lemma force_white_col_moves : (p:pos)(b:board)(moves b (force_white_col p b)).
Unfold force_white_col; Intros.
Case (proj_board A p b); Auto.
Save.

Definition force_white : board ® board :=
[b](force_white_line B
         (force_white_line C
         (force_white_col A
         (force_white_col B
         (force_white_col C b))))).

Hints Resolve force_white_line_moves force_white_col_moves.

Preuve que la fonction de mise en forme normale préserve les déplacements
Lemma force_white_moves : (b:board)(moves b (force_white b)).
Intros; Unfold force_white.
Apply moves_trans with (force_white_col C b); Auto.
Apply moves_trans with (force_white_col B (force_white_col C b)); Auto.
Apply moves_trans with (force_white_col A (force_white_col B
                                 (force_white_col C b))); Auto.
Apply moves_trans with (force_white_line C (force_white_col A
                         (force_white_col B (force_white_col C b)))); Auto.
Save.
Hints Resolve force_white_moves.

On en déduit aisément que 2 damiers qui ont la même forme normale sont dans la même orbite

Lemma force_eq_moves
         : (b1,b2:board)(force_white b1)=(force_white b2)®(moves b1 b2).
Intros; Apply moves_trans with (force_white b1); Auto.
Rewrite H; Auto.
Save.

Réciproquement on veut établir que 2 damiers dans la même orbite ont même forme normale.

Lemma move_force_eq
         : (b1,b2:board)(move b1 b2)®(force_white b1)=(force_white b2).
Destruct 1.

Case b1; Intros l1 l2 l3; Case l1; Intros x1 y1 z1; Case l2; Intros x2 y2 z2;
Case l3; Intros x3 y3 z3; Simpl.

3 * 2⁹ cas, prend 23 s en natif :
Time (Destruct p; Case x1; Case y1; Case z1; Case x2; Case y2; Case z2;
         Case x3; Case y3; Case z3; Compute; Trivial).

Case b1; Intros l1 l2 l3; Case l1; Intros x1 y1 z1; Case l2; Intros x2 y2 z2;
Case l3; Intros x3 y3 z3; Simpl.

Time (Destruct p; Case x1; Case y1; Case z1; Case x2; Case y2; Case z2;
         Case x3; Case y3; Case z3; Compute; Trivial).
Save.

Lemma moves_force_eq
         : (b1,b2:board)(moves b1 b2)®(force_white b1)=(force_white b2).
Change (invariant force_white).
Apply invariant_move.
Exact move_force_eq.
Save.

On a établi l'équivalence entre la relation moves et l'égalité des
formes normales. Pour décider de la relation moves, il suffit de
décider de l'égalité de deux damiers
Decidabilité de l'égalité
Definition dec_eq := [M:Set](x,y:M){x=y}+{notx=y}.

Lemma dec_eq_triple : (M:Set)(dec_eq M)®(dec_eq (triple M)).
Red; Intros M eqdM (x1,x2,x3) (y1,y2,y3).
Case (eqdM x1 y1); Intro H.
Case (eqdM x2 y2); Intro H1.
Case (eqdM x3 y3); Intro H3.
Left; Rewrite H; Rewrite H1; Rewrite H3; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Right; Red; Intro abs; Injection abs; Auto.
Defined.

Une tactique automatique construit la preuve de la décidabilité de
l'égalité sur les types construits sans paramètres
Require EqDecide.
Lemma dec_eq_color : (dec_eq color).
Red; Decide Equality.
Defined.

Lemma dec_eq_board : (dec_eq board).
Unfold board; Apply dec_eq_triple; Apply dec_eq_triple; Exact dec_eq_color.
Defined.

Pour décider si deux damiers sont dans la même orbite, il suffit de décider de l'égalité des formes normales

Lemma moves_dec : (b1,b2:board){(moves b1 b2)}+{not(moves b1 b2)}.
Intros; Case (dec_eq_board (force_white b1) (force_white b2)).
Left; Apply force_eq_moves; Auto.
Right; Apply invariant_not_moves with f:=force_white; Trivial.
Exact moves_force_eq.
Defined.

Definition moves_dec_fun : board ® board ® bool :=
         [b1,b2](if (moves_dec b1 b2) then [_]true else [_]false).

Lemma moves_proof : (b1,b2:board)(moves_dec_fun b1 b2)=true ® (moves b1 b2).
Unfold moves_dec_fun; Intros b1 b2.
Case (moves_dec b1 b2); Simpl; [Trivial | Intros; Discriminate].
Save.

Lemma not_moves_proof
         : (b1,b2:board)(moves_dec_fun b1 b2)=false ® not(moves b1 b2).
Unfold moves_dec_fun; Intros b1 b2.
Case (moves_dec b1 b2); Simpl; [Intros; Discriminate | Trivial].
Save.

Lemma accessible_auto : (moves start target).
Apply moves_proof; Reflexivity.
Save.

Lemma not_accessible_auto : not(moves start white_board).
Apply not_moves_proof; Reflexivity.
Save.

1 Index

accessible_auto, X,
dec_eq (definition), X,
dec_eq_board, X,
dec_eq_color, X,
dec_eq_triple, X,
force_eq_moves, X,
force_white (definition), X,
force_white_col (definition), X,
force_white_col_moves, X,
force_white_line (definition), X,
force_white_line_moves, X,
force_white_moves, X,
invariant (definition), X,
invariant_move, X,
invariant_not_moves, X,
involution (definition), X,
moves_dec, X,
moves_dec_fun (definition), X,
moves_force_eq, X,
moves_proof, X,
moves_sym, X,
move_force_eq, X,
move_sym, X,
not_accessible_auto, X,
not_moves_proof, X,
triple_map_inv, X,
triple_map_select_inv, X,
turn_color_inv, X,
turn_col_inv, X,
turn_line_inv, X,

This document was translated from L^AT_EX by H^EV^EA.