TD10: Damier (checker)

NB: Boards are finite. Number of configurations:

\[2^9 = 512\] 
f: board -> board -> bool

(* Goal : *)
forall b b', f b b' = true <-> Moves b b'

Le Damier de Cachan

M1 Informatique - Preuves Assistées par Ordinateur

Pierre Letouzey (d’après C. Paulin)

Le Damier

On considère un damier de dimensions 3x3. Sur chaque case se trouve un jeton bicolore : blanc sur une face et noir sur l’autre (une seule des deux faces est visible). À chaque étape il est possible de retourner une rangée ou une colonne du damier. On cherche ici à examiner les configurations qu’il est possible d’atteindre à partir d’une configuration donnée. Voici par exemple deux configurations possibles (où Wh marque une case blanche et Bl une case noire) :

start =
 Wh Wh Bl
 Bl Wh Wh
 Bl Bl Bl

target =
 Bl Bl Bl
 Wh Bl Wh
 Bl Bl Wh

Montrer informellement qu’on peut bien aller de la configuration start à la configuration target.

start =
 Wh Wh Bl
 Bl Wh Wh
 Bl Bl Bl

Swap the first row:
 Bl Bl Wh
 Bl Wh Wh
 Bl Bl Bl

Swap the second row:
 Bl Bl Wh
 Wh Bl Bl
 Bl Bl Bl

Swap the last column:
 Bl Bl Bl
 Wh Bl Wh
 Bl Bl Wh


target =
 Bl Bl Bl
 Wh Bl Wh
 Bl Bl Wh

NB: Plusieurs scopes:

Open Scope type_nat

(* ou *)

(X * X)%type

Modélisation du damier

Il est conseillé d’utiliser la commande Set Implicit Arguments pour éviter de taper certains arguments de type dans ce qui suit.

1. Définir un type color à deux valeurs Bl et Wh.

Inductive color := W | B.

NB: autre possibilité: définir le nouveau type à partir d’un ancien

Definition color := bool

2. Définit une fonction inv_color : color -> color qui échange les deux couleurs.

Fixpoint inv_color (c : color) : color :=
  match c with
  | 𝕎 => 𝔹
  | 𝔹 => 𝕎
end.

3. Ouvrir une section avec la commande Section Triple, et déclarer une variable locale X : Type à l’intérieur de cette section à l’aide de la commande Variable X : Type.

Section Triple.
Variable X : Type.

4. Définir un type triple : Type des triplets (x, y, z) d’éléments de X.

Definition triple := (X * X * X)%type.

5. Définir une fonction triple_x : X -> triple qui à tout x : X associe le triplet (x, x, x).

Definition triple_x (x : X) : triple := (x, x, x).

6. Définir une fonction triple_map : (X -> X) -> triple -> triple qui à une fonction f et à un triplet (x, y, z) associe le triplet (f (x), f (y), f (z)).

Definition triple_map (f : X -> X) (t: triple) : triple :=
let '(x, y, z) := t in (f x, f y, f z).

7. Définir un type des positions pos à trois valeurs A, B et C.

Inductive pos := A | B | C.

8. Définir une fonction triple_proj : pos -> triple -> X qui extrait une composante d’un triplet donnée par sa position.

Definition triple_proj (p : pos) (t: triple) : X :=
  let '(x, y, z) := t in match p with
                         | A => x
                         | B => y
                         | C => z
                         end.

9. Définir une fonction triple_map_select : (X -> X) -> pos -> triple -> triple qui applique une fonction à une composante d’un triplet donnée par sa position.

Definition triple_map_select (f: X -> X) (p : pos) (t: triple) : triple :=
  let '(x, y, z) := t in match p with
                         | A => (f x, y, z)
                         | B => (x, f y, z)
                         | C => (x, y, f z)
                         end.

10. Fermer la section avec la commande End Triple. Quel est maintenant le type des objets définis dans la section ?

X est maintenant quelconque:

Par exemple:

Check triple_x.

donne

triple_x: forall X : Type, X -> triple X

11. Définir le type board des configurations comme le type des triplets de triplets de couleurs, ainsi qu’un objet white_board qui modélise la configuration blanche partout.

Definition board := triple (triple color).

(* The scope of Let is local, but outside of a section, it's the
 exact same thing as Definition, whose scope is global *)

Let white_board := ((𝕎, 𝕎, 𝕎), (𝕎, 𝕎, 𝕎), (𝕎, 𝕎, 𝕎)).

12. Définir en Coq les deux configurations start et target données en préambule.

Let start := ((𝕎, 𝕎, 𝔹), (𝔹, 𝕎, 𝕎), (𝔹, 𝔹, 𝔹)).
Let target := ((𝔹, 𝔹, 𝔹), (𝕎, 𝔹, 𝕎), (𝔹, 𝔹, 𝕎)).

Manipulation des configurations

1. Définir la fonction board_proj : board -> pos -> pos -> color qui extrait le contenu d’une case d’une configuration donnée.

Definition board_proj (b: board) (p : pos) (p': pos) : color :=
  let t := triple_proj p b in triple_proj p' t.

2. Définir les fonctions inv_row, inv_col : board -> pos -> board qui inversent respectivement une rangée et une colonne d’une configuration donnée.

Definition inv_row (b: board) (p : pos) : board := triple_map_select (triple_map inv_color) p b.

Definition inv_col (b: board) (p : pos) : board := triple_map (triple_map_select inv_color p) b.

NB: Définir une nouvelle tactique:

Ltac break :=
    match goal with
        | b: board |- _ => destruct b; break
        | t: triple _ |- _ => destruct t; break
        | c: color |- _ => destruct c; break
        | _ => idtac
    end.

3. Définir une relation move : board -> board -> Prop telle que move b1 b2 exprime que b2 s’obtient à partir de b1 en inversant une rangée ou une colonne.

Definition move b1 b2 : Prop := exists p, (b2 = inv_row b1 p \/ b2 = inv_col b1 p).

4. Montrer que cette relation move est symétrique.

Lemme: $\texttt{inv_row}$ et $\texttt{inv_col}$ sont involutives.

Ltac break :=
    match goal with
        | b: board |- _ => destruct b; break
        | t: triple _ |- _ => destruct t; break
        | c: color |- _ => destruct c; break
        | p: (_ * _) |- _ => destruct p; break
        | _ => idtac
    end.

Lemma inv_row_invol : forall b p, inv_row (inv_row b p) p = b.
Proof.
  intros.
  destruct p; break; reflexivity.
Qed.

Lemma inv_col_invol : forall b p, inv_col (inv_col b p) p = b.
Proof.
  intros.
  destruct p; break; reflexivity.
Qed.

Beaucoup mieux:

Ltac break2 :=
  match goal with
  | X: _ |- _ =>
    destruct X; break2
  | _ => idtac
  end.

Lemma inv_row_invol2 : forall b p, inv_row (inv_row b p) p = b.
Proof.
  intros.
  break2; reflexivity.
Qed.

5. Définir inductivement la relation moves : board -> board -> Prop à partir des deux règles suivantes :

  • Pour tout b, on a moves b b
  • Si moves b1 b2 et move b2 b3 alors moves b1 b3 (pour tout b1, b2, b3)

6. Montrer que la relation moves est réflexive, symétrique et transitive.

7. Vérifier que moves start target.

8. Peut-on aisément montrer que ~(moves white_board start) par une preuve directe ?

L’invariant de normalisation

  1. Définir une fonction force_white : board -> board qui inverse certaines rangées et/ou certaines colonnes d’une configuration donnée de manière à ce que la première rangée et la première colonne de la configuration retournée par cette fonction soient entièrement blanches. Vérifier que pour toute configuration b on a moves b (force_white b).
  2. Montrer que move b1 b2 -> force_white b1 = force_white b2.
  3. Montrer que moves b1 b2 <-> force_white b1 = force_white b2.
  4. En déduire que ~(moves white_board start), ainsi qu’une preuve simplifiée de moves start target.

Décidabilité de la relation moves

En Coq, on exprime qu’une relation R (définie sur un type de données X) est décidable par la proposition :

forall x y : X, {R x y}+{~R x y}

où {...}+{...} désigne la disjonction calculatoire (définie dans Type). Notez que cette forme de tiers-exclu calculatoire ne peut pas être déduite du tiers-exclu sur les propositions.

  1. Montrer que l’égalité x = y est décidable sur le type color.
  2. Montrer que si l’égalité est décidable sur un type X, alors elle est décidable sur triple X. En déduire qu’elle est décidable sur le type board.
  3. À l’aide de tout ce qui précède, montrer que la relation moves est décidable.
  4. Extraire le programme OCaml correspondant et tester.

Leave a comment