Commit e47fb632 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td6 in english

parent d9b9e48c
TD6 : the Cachan Checkerboard
Pierre Letouzey (from Christine Paulin)
## The board ##
We consider here a rectangular board of size 3x3. On each cell, there is a two-colored piece : white on one side and black on the other. Only one side is visible at a time. A each step of the game, one may flip over a whole row or a whole column of the board. The question is wether a given configuration is reachable from an initial configuration. For example, two possible configurations are given below (with `Wh` to indicate a white side and `Bl` for a black side) :
start =
Wh Wh Bl
Bl Wh Wh
Bl Bl Bl
target =
Bl Bl Bl
Wh Bl Wh
Bl Bl Wh
Show informally that it is indeed possible to go from the `start` configuration to the `target` one.
## Formalizing the board ##
It is recommended to use first the `Set Implicit Arguments` command to avoid writing some type arguments later.
1. Define a type `color` with two values `Bl` and `Wh`.
2. Define a function `inv_color : color -> color` which flips over the two colors.
3. Open a *section* via the command `Section Triple`, and declare a local variable `X` inside that section via `Variable X : Type`.
4. Define an inductive type `triple` formalizing the triplets `(x, y, z)` of elements in `X`.
5. Define a function `triple_x : X -> triple` which expects a value `x : X` and returns the triplet `(x, x, x)`.
6. Define a function `triple_map : (X -> X) -> triple -> triple` which takes a function `f` and a triplet `(x,y,z)` and returns the triplet `(f (x), f (y), f (z))`.
7. Define a type `pos` for positions, with three possible values `A`, `B`, `C`.
8. Define a function `triple_proj : pos -> triple -> X` which selects the element of a triplet at a given position.
9. Define a function `triple_map_select : (X -> X) -> pos -> triple -> triple` which applies a function on a specific element of a triplet (given by its position).
10. Close the current section via the command `End Triple`. What is now the type of the different elements defined in the sections ?
11. Define the type `board` formalizing configurations as triplets of triplets of colors. Define a value `white_board` corresponding to an all-white board.
12. Define in Coq the `start` and `target` configurations seen earlier.
## Configuration manipulations ##
1. Define the function `board_proj : board -> pos -> pos -> color` which extracts the content of a cell from a given configuration.
2. Define the functions `inv_row, inv_col : board -> pos -> board` which flip over respectively some row and some column of a board.
3. Define a relation `move : board -> board -> Prop` such that `move b1 b2` states that `b2` is obtained from `b1` by flipping over one row or one column.
4. Prove that this `move` relation is symmetric.
5. Define inductively the relation `moves : board -> board -> Prop` from the two following rules:
- Fora all `b`, we have `moves b b`
- If `moves b1 b2` and `move b2 b3` then `moves b1 b3` (for all `b1`, `b2`, `b3`).
6. Prove that the `moves` relation is reflexive, symmetric and transitive.
7. Prove that `moves start target`.
8. Could we easily show that `~(moves white_board start)` via some direct proof ?
## Normalization ##
1. Define a function `force_white : board -> board` which flips some rows and/or some columns of a configuration in such a way that both the obtained first row and first column is entirely white.
2. Prove that for all configuration `b` we have `moves b (force_white b)`.
3. Prove that `move b1 b2 -> force_white b1 = force_white b2`.
4. Prove that `moves b1 b2 <-> force_white b1 = force_white b2`.
5. Deduce that `~(moves white_board start)`, and also obtain a simplified proof that `moves start target`.
## Decidability of the moves relation ##
Consider a relation `R : X->X->Prop` defined on some domain `X`. In Coq, we express that this relation is *decidable* (i.e. decidable via a computable algorithm) via the following statement :
forall x y : X, { R x y }+{ ~R x y }
Here the `{...}+{...}` syntax designates the computational disjunction : named `sumbool` internally, it is defined in `Type`, unlike the usual disjunction `\/` which is defined in `Prop`. And the above statement is hence a form of excluded-middle, but a computational excluded-middle that cannot be deduced from the propositional excluded-middle.
1. Show that the equality `x = y` is decidable on type `color`.
2. Show that whenever the equality is decidable on a type `X`, then it is also the case for the equality on `triple X`.
Deduce that the equality is decidable on the type `board`.
3. Thanks to all the previous proofs, conclude now that the `moves` relation is decidable.
4. Use the Coq extraction to obtain a corresponding program and test it.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment