Library cachan
Require Import ssreflect.
On comprendra plus bas la signification de la commande suivante
Set Implicit Arguments.
Un type énuméré. C'est l'exemple le plus simple de type inductif; ici il peut être construit
par deux constructeurs White et Black
Inductive color : Type := White | Black.
Un type inductif est le plus petit type qui peut être construit par ses constructeurs. Il y a deux aspects à cela.
1) Un principe est généré pour chaque type inductif:
On utilise ce principe avec la tactique elim . Par exemple :
1) Un principe est généré pour chaque type inductif:
Check color_ind.
color_ind
: forall P : color -> Prop,
P White ->
P Black -> forall c : color, P c
On voit qu'il dit bien qu'une propriété vraie pour White et Black l'est sur tout le type color . Il n'y a donc pas d'autres valeur possible.
On utilise ce principe avec la tactique elim . Par exemple :
Lemma Black_or_White : forall x : color, x = White \/ x = Black.
Proof.
move => x.
elim: x.
...
Qed.
L'autre utilisation des types inductifs est le calcul. On peut définir une fonction sur un tel type par analyse de cas. A condition de bien considérer tous les cas possibles.
On peut calculer en Coq. En général, les calculs sont obtenus en appliquant des arguments à une fonction. La commande est la suivante :
On va maintenant donner une définition générique des triplets sur un type quelconque. Pour cela, une manière est d'ouvrir une Section dans laquelle on se donne une variable de type; c'est pour l'instant un type abstrait.
Section Triple.
Variable T : Type.
Les triplets sont aussi définis inductivement: il y a une seule manière canonique de construire un triplet, donc un seul constructeur.
Ce constructeurs prend en argument les trois composantes du triplet. Ici on veut des triplets uniformes, les trois arguments sont donc de type T .
Ce constructeurs prend en argument les trois composantes du triplet. Ici on veut des triplets uniformes, les trois arguments sont donc de type T .
Définir la fonction qui à x associe le triplet (x,x,x).
Definition full x :=
Pour définir quelques fonctions génériques utiles sur les triplets, on se donne une autre variable abstraite:
Variable f : T -> T.
On peut alors définir la fonctionnelle qui applique f à chaque composante d'un triplet:
Definition map (t:triple) : triple :=
...
On veut être capable de parler de chacune des trois positions possibles d'un objet dans un triplet. Pour cela on définit le type énuméré à trois valeurs possibles:
Inductive pos := p1 | p2 | p3.
On définit la fonction qui effectue la p-ième projection sur un triplet.
Definition proj_triple (t:triple) (p:pos) :=
...
On veut appliquer f uniquement à la p-ième position d'un triplet.
Definition map_p (p:pos) (t:triple) :=
On ferme maintenant la section.
End Triple.
Cette opération a eu un effet sur les définitions effectuées à l'intérieur de la section.
Pour le comprendre, regardez les (nouveaux) types des différents objets définis dans la section - y compris triple .
Pour le comprendre, regardez les (nouveaux) types des différents objets définis dans la section - y compris triple .
On peut voir maintenant une rangée comme un triplet de couleur, et un damier comme un triplet de triplets de couleurs.
Definition board : Type := ...
Un coup joué est décrit par un position et un booléen (ce dernier indiquant si on retourne la ligne ou la colonne correspondant à la position.
Definition move := (pos * bool)%type.
Jouer un coup donner transforme un damier en un autre.
Definition play_move (b:board)(m:move) :=
...
On va utiliser la bibliothèque générique des listes.
Require Import List.
Vérifiez la définition de list par Print .
Une suite de coup est une liste de coups.
Definition moves := list move....
Effectuer une liste de coups. C'est notre première fonction récursive.
Fixpoint play_moves (l:moves)(b:board) :=
....
On peut atteindre un damier à partir d'un autre si on passe de l'un à l'autre par une liste de coups.
Definition reachable b1 b2 : Prop :=
...
Les damiers noirs et blancs (utilisez full ).
Definition WB := ...
Definition BB := ...
Une preuve facile grace au calcul
Lemma white_to_black : reachable WB BB.
Proof.
....
L'atteignabilité est transitive. Pour le montrer on passe par le lemme suivant qui est la première preuve par récurrence.
Lemma play_app : forall b l1 l2, play_moves (l2 ++ l1) b = play_moves l1 (play_moves l2 b).
...
Lemma reachable_trans : ...
On se donne un autre damier
Definition mystere :=
mkt (mkt White Black Black)
(mkt White Black Black)
(mkt Black White Black).
Le 'XOR' sur les couleurs.
Definition add_color c1 c2 :=
match c1,c2 with
| White, White => Black
| Black, Black => Black
| _, _ => White
end.
On trouve un invariant qui discrimine entre le damier mystère et le damier blanc.
Definition invariant (b:board) := ...
Cette preuve est simple au fond. Mais on la fait un peu différemment de ce que serait l'explication intuitive.
Lemma invariant1 : forall b m, invariant b = invariant (play_move b m).
Proof.
...
Lemma invariant2 : forall b l, invariant b = invariant (play_moves l b).
Proof.
...
On en déduit notre résultat principal.
Lemma impossible : ~reachable WB mystere.
Proof.
...
On peut faire le même développement sans utniliser de listes, mais des prédicats inductifs.
D'abord la colture reflexive-transitive de play_move:
D'abord la colture reflexive-transitive de play_move:
Inductive reachable' (b : board) : board -> Prop :=
| reachable_refl : reachable' b b
| reachable_step : forall b1 m, reachable' b b1 -> reachable' b (play_move b1 m).
Lemma reachable_trans' : forall b c d, reachable' b c -> reachable' c d -> reachable' b d.
Proof.
move => b c d bc cd.
elim: cd.
...
La suite en exercice: refaire le développement mais avec reachable' .
apply Hl.
done.
simpl in e.