Library allumette
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq finfun.
Require Import choice fintype tuple div zmodp bigop ssralg perm fingroup.
Import GRing.Theory.
Section Allumette.
(******************************************************************************)
(* *)
(* *)
(* MODÉLISATION *)
(* *)
(* *)
(******************************************************************************)
(* Les tas d'allumette sont représentés par une suite de nombres *)
Definition val := nat.
Definition heaps := seq val.
(* L'exemple *)
Definition heaps0 : heaps := [:: 5; 6 ; 4].
(* Une suite de tas vides *)
Definition empty (h : heaps) := h == nseq (size h) 0.
(* Un coup est représenté par un numéro de tas et le nombre d'allumettes *)
(* restante *)
Definition move := (nat * val)%type.
(* Laisser 4 allumettes dans le deuxième tas *)
Definition move0 : move := (1, 4).
(* Effectuer un coup *)
Definition make_move (h : heaps) (m : move) : heaps :=
let (i, v) := m in take i h ++ v :: drop i.+1 h.
(* Un coup est valide si le nombre d'allumettes restantes diminue strictement *)
Definition valid_move (h : heaps) (m : move) :=
let (i, v) := m in v < nth 0 h i.
(* Une partie est une suite de coups *)
Definition game := seq move.
Definition game0 := [:: (0, 0); (1, 1); (1, 0); (2, 0)].
(* Une partie est valide si chacun de ses coups est valide et se termine par *)
(* un tas vide *)
Fixpoint valid_game (h : heaps) (g : game) :=
if g is m :: g1 then valid_move h m && valid_game (make_move h m) g1
else empty h.
(* Une strategie est une fonction qui retourne un coup valide *)
Inductive strategy :=
Strategy (f : heaps -> move) of forall h, ~~ empty h -> valid_move h (f h).
Definition fun_of_strategy s := let: Strategy f _ := s in f.
Coercion fun_of_strategy : strategy >-> Funclass.
(* La stratégie qui vide le premier tas non vide *)
Definition pick_first (h : heaps) : move := (find (predC1 0) h, 0).
Lemma valid_pick_first h : ~~ empty h -> valid_move h (pick_first h).
Definition strat0 := Strategy valid_pick_first.
(* On s'intéresse au premier joueur. Une partie suit une stratégie si tout *)
(* coup pair est effectué par la stratégie *)
Fixpoint follow_strategy (s : strategy) (h : heaps) (g : game) :=
if g is m1 :: g1 then (m1 == s h) &&
if g1 is m2 :: g2 then
let h2 := make_move (make_move h m1) m2 in follow_strategy s h2 g2
else true
else true.
(* Une stratégie est gagnante si, en suivant la stratégie, toutes les parties *)
(* sont de longueur impaire *)
Definition winning_strategy s h :=
forall g, valid_game h g -> follow_strategy s h g -> odd (size g).
Lemma nw_strat0 : ~ winning_strategy strat0 heaps0.
(* Une stratégie gagnante va se servir de la représentation binaire des *)
(* nombres *)
(******************************************************************************)
(* *)
(* NOMBRES BINAIRES *)
(* *)
(******************************************************************************)
Section Nombre.
Variable n : nat.
(* On utilise la représentation des nombres comme un tuple de booléens *)
Local Notation number := (n.-tuple bool).
(* Un ou exclusif sur les nombres *)
Definition addm (m1 m2 : number) :=
[tuple of [seq x.1 (+) x.2 | x <- zip m1 m2]].
Notation "%[+]" := addm (at level 0).
Notation "x [+] y" := (addm x y) (at level 10).
(* Le nombre zéro *)
Definition falsem := [tuple of nseq n false].
Notation F := falsem.
Lemma diffF m : m != F -> true \in m.
(* Un ensemble de règles de réécriture *)
Definition rewL :=
((fun n => @tnth_nth n _ false), nth_map (false,false), nth_zip,
nth_nseq, ltn_ord, size_nseq, size_tuple, size_zip, minnn).
(* Propriétés génériques du ou exclusif sur les nombres *)
Lemma addFm : left_id F %[+].
Lemma addmm : self_inverse F %[+].
Lemma addmC : commutative %[+].
Lemma addmA : associative %[+].
Definition addm_zmodMixin := ZmodMixin addmA addmC addFm addmm.
Canonical addm_zmodType := ZmodType number addm_zmodMixin.
(* Conversion `_ de nombre vers entier naturel *)
Fixpoint num2nat (n : nat) (l : seq bool) :=
if n is m1.+1 then 2^ m1 * head false l + num2nat m1 (behead l)
else 0.
Notation "`[ m ]_ n" := (num2nat n m) (at level 40).
Lemma num2natE (m : n.-tuple bool) :
`[m]_n = \sum_(i < n) 2 ^ (n.-1 - i) * tnth m i.
Lemma num2natF : `[F]_n = 0.
Lemma num2nat_eqF0 (m : number) : (`[m]_n == 0) = (m == F).
(* Conversion `{_} de nombre vers entier naturel *)
Fixpoint nat2num (m : nat) (v : nat) : m.-tuple bool :=
if m is m1.+1 then [tuple of rcons (nat2num m1 v./2) (odd v)]
else [tuple of [::]].
Notation "`{ m }_ n " := (@nat2num n m) (at level 10).
Lemma nth_nat2num m (v : nat) i :
tnth (`{v}_m) i = odd (v %/ (2 ^ (m.-1 - i)))%N.
Lemma nat2numE m v :
v < 2 ^ m -> `{v}_m.+1 = [tuple of false :: `{v}_m].
Lemma nat2num0 : `{0}_n = F.
Lemma nat2numK v : v < 2 ^ n -> `[`{v}_n ]_n = v.
(* Un lemme pour calculer les sommes de puissances de 2 *)
Lemma sum_pow2 k n1 : \sum_(k <= j < n1) 2 ^ (n1.-1 - j) = (2 ^ (n1 - k)).-1.
Lemma num2natK (v : number) : `{`[v]_n }_n = v.
(* Bit de poids fort *)
Definition hbit (m : number) := index true m.
Lemma hbitF : hbit F = n.
Lemma hbit_ltn m : m != F -> hbit m < n.
Lemma hbit_true m (i : 'I_n) : hbit m = i -> tnth m i = true.
Lemma hbit_lt m (i : 'I_n) : i < hbit m -> tnth m i = false.
(* Lemme clé qui va assurer que le nombre d'allumettes décroit *)
Lemma ltn_num_addm m1 m2 (i : 'I_n) :
hbit m1 = i -> tnth m2 i = true -> `[m1 [+] m2]_n < `[m2]_n.
Lemma addm_nth_orb (m1 m2 : number) i :
tnth (m1 [+] m2) i -> tnth m1 i || tnth m2 i.
Lemma addm_nth_exists (l : seq number) i :
tnth (\sum_(i <- l) i)%R i -> {j | j < size l /\ tnth (nth F l j) i}.
End Nombre.
Notation "%[+]" := (@addm _).
Notation "x [+] y" := (addm x y) (at level 10).
Notation F := (@falsem _).
Notation "`[ m ]_ n " := (num2nat n m) (at level 10).
Notation "`{ m }_ n " := (nat2num n m) (at level 10).
(******************************************************************************)
(* *)
(* STRATÉGIE GAGNANTE *)
(* *)
(******************************************************************************)
Definition pick_best (h : heaps) : move :=
(* nombres de bits nécessaires pour coder les entiers dans la liste *)
let n := foldr maxn 0 h in
(* conversion de la suite d'entiers en une suite de nombres binaires *)
let l := [seq (nat2num n i) | i <- h] in
(* le ou exclusif de tous les éléments de la suite *)
let v := foldr %[+] F l in
(* Si le ou exclusif est nul, prendre la stratégie first_pick *)
if v == F then pick_first h else
(* Sinon on cherche le tas dont le ou exclusif fait baisser la valeur *)
let i := find (fun a => `[v [+] a]_n < `[a]_n) l in
let x := `[v [+] (nth F l i)]_n in (i, x).
(* pick_best génère que des coups valides *)
Lemma valid_pick_best h : ~~ empty h -> valid_move h (pick_best h).
(* La stratégie gagnante *)
Definition strat_best := Strategy valid_pick_best.
Definition is_winning (h : heaps) :=
let n := foldr maxn 0 h in
let l := [seq (nat2num n i) | i <- h] in
let v := foldr %[+] F l in v != F.
Lemma is_winningE h :
let n := foldr maxn 0 h in
is_winning h = (`[\sum_(i <- h) (nat2num (foldr maxn 0%N h) i)]_n != 0%N)%R.
Lemma is_winning_not_empty h : is_winning h -> ~ empty h.
Lemma big_nat2num_eq n1 n2 h :
all (fun i => i < 2 ^ n1) h -> all (fun i => i < 2 ^ n2) h ->
(`[\sum_(i <- h) `{i}_n1]_n1 = `[\sum_(i <- h) `{i}_n2]_n2)%R.
(* On peut évaluer la somme dans la position précédente *)
Lemma sum_make_move h m :
let h1 := make_move h m in
let n1 := foldr maxn 0 h in let n2 := foldr maxn 0 h1 in
valid_move h m ->
(`[\sum_(i <- h1) `{i}_n2 ]_n2 = `[\sum_(i <- h1) `{i}_n1]_n1)%R.
(* Après un coup d'une position perdante on obtient une position gagnante *)
Lemma nis_winning_is_winning h m :
valid_move h m -> ~ is_winning h -> is_winning (make_move h m).
(* Après un coup d'une position gagne en suivant la stratégie on obtient une *)
(* position perdante *)
Lemma is_winning_nis_winning h :
is_winning h -> ~ is_winning (make_move h (strat_best h)).
(* En combinant les deux propriétés précédentes, la stratégie est gagnante! *)
Lemma w_strat_best h : is_winning h -> winning_strategy strat_best h.
(* Notre exemple est gagnant *)
Fact w_strat_best0 : winning_strategy strat_best heaps0.
(* Pour finir, une petite partie *)
(* Premier coup *)
Definition m0 := strat_best heaps0.
Definition heaps1 := make_move heaps0 m0.
(* Deuxième coup : on laisse 3 allumettes dans le deuxième tas *)
Definition m1 := (1, 3).
Definition heaps2 := make_move heaps1 m1.
(* Troisième coup *)
Definition m2 := strat_best heaps2.
Definition heaps3 := make_move heaps2 m2.
(* Quatrième coup : on laisse 1 allumette dans le deuxième tas *)
Definition m3 := (1, 1).
Definition heaps4 := make_move heaps3 m3.
(* Cinquième coup *)
Definition m4 := strat_best heaps4.
Definition heaps5 := make_move heaps4 m4.
(* Sixième coup : on laisse 0 allumette dans le dernier tas *)
Definition m5 := (2, 0).
Definition heaps6 := make_move heaps5 m5.
(* Dernier coup *)
Definition m6 := strat_best heaps5.
Definition heaps7 := make_move heaps6 m6.
(* Gagné! *)
End Allumette.
Require Import choice fintype tuple div zmodp bigop ssralg perm fingroup.
Import GRing.Theory.
Section Allumette.
(******************************************************************************)
(* *)
(* *)
(* MODÉLISATION *)
(* *)
(* *)
(******************************************************************************)
(* Les tas d'allumette sont représentés par une suite de nombres *)
Definition val := nat.
Definition heaps := seq val.
(* L'exemple *)
Definition heaps0 : heaps := [:: 5; 6 ; 4].
(* Une suite de tas vides *)
Definition empty (h : heaps) := h == nseq (size h) 0.
(* Un coup est représenté par un numéro de tas et le nombre d'allumettes *)
(* restante *)
Definition move := (nat * val)%type.
(* Laisser 4 allumettes dans le deuxième tas *)
Definition move0 : move := (1, 4).
(* Effectuer un coup *)
Definition make_move (h : heaps) (m : move) : heaps :=
let (i, v) := m in take i h ++ v :: drop i.+1 h.
(* Un coup est valide si le nombre d'allumettes restantes diminue strictement *)
Definition valid_move (h : heaps) (m : move) :=
let (i, v) := m in v < nth 0 h i.
(* Une partie est une suite de coups *)
Definition game := seq move.
Definition game0 := [:: (0, 0); (1, 1); (1, 0); (2, 0)].
(* Une partie est valide si chacun de ses coups est valide et se termine par *)
(* un tas vide *)
Fixpoint valid_game (h : heaps) (g : game) :=
if g is m :: g1 then valid_move h m && valid_game (make_move h m) g1
else empty h.
(* Une strategie est une fonction qui retourne un coup valide *)
Inductive strategy :=
Strategy (f : heaps -> move) of forall h, ~~ empty h -> valid_move h (f h).
Definition fun_of_strategy s := let: Strategy f _ := s in f.
Coercion fun_of_strategy : strategy >-> Funclass.
(* La stratégie qui vide le premier tas non vide *)
Definition pick_first (h : heaps) : move := (find (predC1 0) h, 0).
Lemma valid_pick_first h : ~~ empty h -> valid_move h (pick_first h).
Definition strat0 := Strategy valid_pick_first.
(* On s'intéresse au premier joueur. Une partie suit une stratégie si tout *)
(* coup pair est effectué par la stratégie *)
Fixpoint follow_strategy (s : strategy) (h : heaps) (g : game) :=
if g is m1 :: g1 then (m1 == s h) &&
if g1 is m2 :: g2 then
let h2 := make_move (make_move h m1) m2 in follow_strategy s h2 g2
else true
else true.
(* Une stratégie est gagnante si, en suivant la stratégie, toutes les parties *)
(* sont de longueur impaire *)
Definition winning_strategy s h :=
forall g, valid_game h g -> follow_strategy s h g -> odd (size g).
Lemma nw_strat0 : ~ winning_strategy strat0 heaps0.
(* Une stratégie gagnante va se servir de la représentation binaire des *)
(* nombres *)
(******************************************************************************)
(* *)
(* NOMBRES BINAIRES *)
(* *)
(******************************************************************************)
Section Nombre.
Variable n : nat.
(* On utilise la représentation des nombres comme un tuple de booléens *)
Local Notation number := (n.-tuple bool).
(* Un ou exclusif sur les nombres *)
Definition addm (m1 m2 : number) :=
[tuple of [seq x.1 (+) x.2 | x <- zip m1 m2]].
Notation "%[+]" := addm (at level 0).
Notation "x [+] y" := (addm x y) (at level 10).
(* Le nombre zéro *)
Definition falsem := [tuple of nseq n false].
Notation F := falsem.
Lemma diffF m : m != F -> true \in m.
(* Un ensemble de règles de réécriture *)
Definition rewL :=
((fun n => @tnth_nth n _ false), nth_map (false,false), nth_zip,
nth_nseq, ltn_ord, size_nseq, size_tuple, size_zip, minnn).
(* Propriétés génériques du ou exclusif sur les nombres *)
Lemma addFm : left_id F %[+].
Lemma addmm : self_inverse F %[+].
Lemma addmC : commutative %[+].
Lemma addmA : associative %[+].
Definition addm_zmodMixin := ZmodMixin addmA addmC addFm addmm.
Canonical addm_zmodType := ZmodType number addm_zmodMixin.
(* Conversion `_ de nombre vers entier naturel *)
Fixpoint num2nat (n : nat) (l : seq bool) :=
if n is m1.+1 then 2^ m1 * head false l + num2nat m1 (behead l)
else 0.
Notation "`[ m ]_ n" := (num2nat n m) (at level 40).
Lemma num2natE (m : n.-tuple bool) :
`[m]_n = \sum_(i < n) 2 ^ (n.-1 - i) * tnth m i.
Lemma num2natF : `[F]_n = 0.
Lemma num2nat_eqF0 (m : number) : (`[m]_n == 0) = (m == F).
(* Conversion `{_} de nombre vers entier naturel *)
Fixpoint nat2num (m : nat) (v : nat) : m.-tuple bool :=
if m is m1.+1 then [tuple of rcons (nat2num m1 v./2) (odd v)]
else [tuple of [::]].
Notation "`{ m }_ n " := (@nat2num n m) (at level 10).
Lemma nth_nat2num m (v : nat) i :
tnth (`{v}_m) i = odd (v %/ (2 ^ (m.-1 - i)))%N.
Lemma nat2numE m v :
v < 2 ^ m -> `{v}_m.+1 = [tuple of false :: `{v}_m].
Lemma nat2num0 : `{0}_n = F.
Lemma nat2numK v : v < 2 ^ n -> `[`{v}_n ]_n = v.
(* Un lemme pour calculer les sommes de puissances de 2 *)
Lemma sum_pow2 k n1 : \sum_(k <= j < n1) 2 ^ (n1.-1 - j) = (2 ^ (n1 - k)).-1.
Lemma num2natK (v : number) : `{`[v]_n }_n = v.
(* Bit de poids fort *)
Definition hbit (m : number) := index true m.
Lemma hbitF : hbit F = n.
Lemma hbit_ltn m : m != F -> hbit m < n.
Lemma hbit_true m (i : 'I_n) : hbit m = i -> tnth m i = true.
Lemma hbit_lt m (i : 'I_n) : i < hbit m -> tnth m i = false.
(* Lemme clé qui va assurer que le nombre d'allumettes décroit *)
Lemma ltn_num_addm m1 m2 (i : 'I_n) :
hbit m1 = i -> tnth m2 i = true -> `[m1 [+] m2]_n < `[m2]_n.
Lemma addm_nth_orb (m1 m2 : number) i :
tnth (m1 [+] m2) i -> tnth m1 i || tnth m2 i.
Lemma addm_nth_exists (l : seq number) i :
tnth (\sum_(i <- l) i)%R i -> {j | j < size l /\ tnth (nth F l j) i}.
End Nombre.
Notation "%[+]" := (@addm _).
Notation "x [+] y" := (addm x y) (at level 10).
Notation F := (@falsem _).
Notation "`[ m ]_ n " := (num2nat n m) (at level 10).
Notation "`{ m }_ n " := (nat2num n m) (at level 10).
(******************************************************************************)
(* *)
(* STRATÉGIE GAGNANTE *)
(* *)
(******************************************************************************)
Definition pick_best (h : heaps) : move :=
(* nombres de bits nécessaires pour coder les entiers dans la liste *)
let n := foldr maxn 0 h in
(* conversion de la suite d'entiers en une suite de nombres binaires *)
let l := [seq (nat2num n i) | i <- h] in
(* le ou exclusif de tous les éléments de la suite *)
let v := foldr %[+] F l in
(* Si le ou exclusif est nul, prendre la stratégie first_pick *)
if v == F then pick_first h else
(* Sinon on cherche le tas dont le ou exclusif fait baisser la valeur *)
let i := find (fun a => `[v [+] a]_n < `[a]_n) l in
let x := `[v [+] (nth F l i)]_n in (i, x).
(* pick_best génère que des coups valides *)
Lemma valid_pick_best h : ~~ empty h -> valid_move h (pick_best h).
(* La stratégie gagnante *)
Definition strat_best := Strategy valid_pick_best.
Definition is_winning (h : heaps) :=
let n := foldr maxn 0 h in
let l := [seq (nat2num n i) | i <- h] in
let v := foldr %[+] F l in v != F.
Lemma is_winningE h :
let n := foldr maxn 0 h in
is_winning h = (`[\sum_(i <- h) (nat2num (foldr maxn 0%N h) i)]_n != 0%N)%R.
Lemma is_winning_not_empty h : is_winning h -> ~ empty h.
Lemma big_nat2num_eq n1 n2 h :
all (fun i => i < 2 ^ n1) h -> all (fun i => i < 2 ^ n2) h ->
(`[\sum_(i <- h) `{i}_n1]_n1 = `[\sum_(i <- h) `{i}_n2]_n2)%R.
(* On peut évaluer la somme dans la position précédente *)
Lemma sum_make_move h m :
let h1 := make_move h m in
let n1 := foldr maxn 0 h in let n2 := foldr maxn 0 h1 in
valid_move h m ->
(`[\sum_(i <- h1) `{i}_n2 ]_n2 = `[\sum_(i <- h1) `{i}_n1]_n1)%R.
(* Après un coup d'une position perdante on obtient une position gagnante *)
Lemma nis_winning_is_winning h m :
valid_move h m -> ~ is_winning h -> is_winning (make_move h m).
(* Après un coup d'une position gagne en suivant la stratégie on obtient une *)
(* position perdante *)
Lemma is_winning_nis_winning h :
is_winning h -> ~ is_winning (make_move h (strat_best h)).
(* En combinant les deux propriétés précédentes, la stratégie est gagnante! *)
Lemma w_strat_best h : is_winning h -> winning_strategy strat_best h.
(* Notre exemple est gagnant *)
Fact w_strat_best0 : winning_strategy strat_best heaps0.
(* Pour finir, une petite partie *)
(* Premier coup *)
Definition m0 := strat_best heaps0.
Definition heaps1 := make_move heaps0 m0.
(* Deuxième coup : on laisse 3 allumettes dans le deuxième tas *)
Definition m1 := (1, 3).
Definition heaps2 := make_move heaps1 m1.
(* Troisième coup *)
Definition m2 := strat_best heaps2.
Definition heaps3 := make_move heaps2 m2.
(* Quatrième coup : on laisse 1 allumette dans le deuxième tas *)
Definition m3 := (1, 1).
Definition heaps4 := make_move heaps3 m3.
(* Cinquième coup *)
Definition m4 := strat_best heaps4.
Definition heaps5 := make_move heaps4 m4.
(* Sixième coup : on laisse 0 allumette dans le dernier tas *)
Definition m5 := (2, 0).
Definition heaps6 := make_move heaps5 m5.
(* Dernier coup *)
Definition m6 := strat_best heaps5.
Definition heaps7 := make_move heaps6 m6.
(* Gagné! *)
End Allumette.
This page has been generated by coqdoc