Library nombre
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div prime path.
Section Nombre.
(* Convertir une liste d'entiers en un entier *)
Definition l2nat l := foldl (fun v i => i + 10 * v) 0 l.
Lemma l2nat_rcons l n : l2nat (rcons l n) = l2nat l * 10 + n.
(* Convertir un entier en une liste d'entiers *)
Fixpoint nat2l2 m n :=
if n < 10 then [:: n] else
if m is m1.+1 then rcons (nat2l2 m1 (n %/ 10)) (n %% 10) else [::n].
Definition nat2l n := nat2l2 n n.
Lemma nat2l2K m n : n < 10 ^ m -> l2nat (nat2l2 m n) = n.
Lemma nat2l2_eq m1 m2 n :
n < 10 ^ m1 -> n < 10 ^ m2 -> nat2l2 m1 n = nat2l2 m2 n.
Lemma nat2lK n : l2nat (nat2l n) = n.
(******************************************************************************)
(* *)
(* Modélisation des différentes propositions *)
(* *)
(******************************************************************************)
(* Chiffres décroissants *)
Definition prop1 l := (1 \in l) == sorted (fun x y => x >= y) l.
(* Au moins deux chiffres impairs *)
Definition prop2 l := (2 \in l) == (count odd l >= 2).
(* Tous les chiffres différents *)
Definition prop3 l := (3 \in l) == uniq l.
(* Quatrième chiffre en partant de la gauche est pair *)
Definition prop4 l := (4 \in l) == ~~ odd (nth 0 l 3).
(* Produit non divisible par 5 *)
Definition prop5 l := (5 \in l) == ~~ (5 %| foldr muln 1 l).
(* Trois chiffres impairs à la suite *)
Fixpoint todd l := if l is a :: l1 then
if l1 is b :: c :: l2 then
[&& odd a, odd b & odd c] || todd l1
else false
else false.
Definition prop6 l := (6 \in l) == todd l.
(* Est un nombre premier *)
Definition prop7 l := (7 \in l) == prime (l2nat l).
(* Pas plus 2 nombres pairs à la suite *)
Fixpoint teven l := if l is a :: l1 then
if l1 is b :: c :: _ then
[&& ~~ odd a, ~~ odd b & ~~ odd c] || teven l1
else false
else false.
Definition prop8 l := (8 \in l) == ~~ teven l.
(* Produit des impairs est un carré parfait *)
Definition perfect_square n :=
all (fun p => ~~ odd p.2) (prime_decomp n).
Definition iprod l := foldr (fun i v => if odd i then i * v else v) 1 l.
Definition prop9 l := (9 \in l) == perfect_square (iprod l).
(* Un élément distinct est la somme des autres *)
Definition prop0 l := (0 \in l) ==
(let sum := foldr addn 0 l in
~~ odd sum && (count (pred1 sum./2) l == 1)).
(* Toutes les propositions *)
Definition check_prop n :=
let l := nat2l n in
[&& prop1 l, prop2 l, prop3 l, prop4 l, prop5 l,
prop6 l, prop7 l, prop8 l, prop9 l& prop0 l].
(* Une version plus rapide *)
Definition fcheck_prop n :=
let l := nat2l n in
if prop9 l then if prop8 l then if prop0 l then if prop6 l then if prop5 l
then if prop4 l then if prop3 l then if prop2 l then if prop1 l then prop7 l
else false else false else false else false else false else false else false
else false else false.
Lemma Pfcheck_prop n : fcheck_prop n = check_prop n.
(* Le résultat *)
Definition result := l2nat [:: 9; 4; 2; 2; 1; 0].
(* Le résultat vérifie les 10 propositions *)
Fact Presult : check_prop result.
(******************************************************************************)
(* *)
(* Tester tous les nombres plus petits que 942210 *)
(* *)
(******************************************************************************)
(* Test à zero sur une liste *)
Definition is_zero l := all (pred1 0) l.
Lemma is_zero_rcons l a : is_zero (rcons l a) = (is_zero l && (a == 0)).
Lemma head_nat2l2_eq0 m n :
n < 10 ^ m -> (nth 1 (nat2l2 m n) 0 == 0) == (n == 0).
Lemma is_zero_nat2l2 m n : n < 10 ^ m -> is_zero (nat2l2 m n) == (n == 0).
(* Remplacer tous les chiffres par des 9 *)
Definition to_nine l := map (fun i : nat => 9) l.
(* Décrémenter de 1 une liste *)
Fixpoint decrr l :=
if l is a :: l1 then
if is_zero l1 then
if a == 0 then to_nine l else a.-1 :: to_nine l1
else a :: decrr l1
else [::].
Definition decr l :=
if is_zero l then [:: 0] else
let l1 := decrr l in
if l1 is 0 :: a :: l2 then a :: l2 else l1.
Lemma decrr_rcons l a :
decrr (rcons l a) =
if (a == 0) then rcons (decrr l) 9 else rcons l a.-1.
Lemma Pdecrr m n : n < 10 ^ m -> 0 < n ->
let l1 := decrr (nat2l2 m n) in
(if l1 is 0 :: a :: l2 then a :: l2 else l1) = nat2l2 m n.-1.
Lemma Pdecr n : decr (nat2l n) = nat2l n.-1.
(* Une version plus efficace pour vérifier les propositions *)
Definition check_propl l :=
if prop9 l then
if prop8 l then
if prop0 l then
if prop6 l then
if prop5 l then
if prop4 l then
if prop3 l then
if prop2 l then
if prop1 l then prop7 l else false
else false else false else false else false else false else false
else false else false.
Lemma Pcheck_propl n : check_prop n = check_propl (nat2l n).
(* Vérifier en décrémentant progressivement *)
Fixpoint check_less l n :=
let l1 := decr l in
if n is n1.+1 then check_propl l1 || check_less l1 n1
else false.
Lemma Pcheck_less n m :
check_less (nat2l n) m = false -> forall k, n - m <= k < n -> ~ check_prop k.
(* Tous les nombres plus petits ne vérifient pas les 10 propositions *)
Fact Lresult : forall m, m < result -> ~ check_prop m.
End Nombre.
Section Nombre.
(* Convertir une liste d'entiers en un entier *)
Definition l2nat l := foldl (fun v i => i + 10 * v) 0 l.
Lemma l2nat_rcons l n : l2nat (rcons l n) = l2nat l * 10 + n.
(* Convertir un entier en une liste d'entiers *)
Fixpoint nat2l2 m n :=
if n < 10 then [:: n] else
if m is m1.+1 then rcons (nat2l2 m1 (n %/ 10)) (n %% 10) else [::n].
Definition nat2l n := nat2l2 n n.
Lemma nat2l2K m n : n < 10 ^ m -> l2nat (nat2l2 m n) = n.
Lemma nat2l2_eq m1 m2 n :
n < 10 ^ m1 -> n < 10 ^ m2 -> nat2l2 m1 n = nat2l2 m2 n.
Lemma nat2lK n : l2nat (nat2l n) = n.
(******************************************************************************)
(* *)
(* Modélisation des différentes propositions *)
(* *)
(******************************************************************************)
(* Chiffres décroissants *)
Definition prop1 l := (1 \in l) == sorted (fun x y => x >= y) l.
(* Au moins deux chiffres impairs *)
Definition prop2 l := (2 \in l) == (count odd l >= 2).
(* Tous les chiffres différents *)
Definition prop3 l := (3 \in l) == uniq l.
(* Quatrième chiffre en partant de la gauche est pair *)
Definition prop4 l := (4 \in l) == ~~ odd (nth 0 l 3).
(* Produit non divisible par 5 *)
Definition prop5 l := (5 \in l) == ~~ (5 %| foldr muln 1 l).
(* Trois chiffres impairs à la suite *)
Fixpoint todd l := if l is a :: l1 then
if l1 is b :: c :: l2 then
[&& odd a, odd b & odd c] || todd l1
else false
else false.
Definition prop6 l := (6 \in l) == todd l.
(* Est un nombre premier *)
Definition prop7 l := (7 \in l) == prime (l2nat l).
(* Pas plus 2 nombres pairs à la suite *)
Fixpoint teven l := if l is a :: l1 then
if l1 is b :: c :: _ then
[&& ~~ odd a, ~~ odd b & ~~ odd c] || teven l1
else false
else false.
Definition prop8 l := (8 \in l) == ~~ teven l.
(* Produit des impairs est un carré parfait *)
Definition perfect_square n :=
all (fun p => ~~ odd p.2) (prime_decomp n).
Definition iprod l := foldr (fun i v => if odd i then i * v else v) 1 l.
Definition prop9 l := (9 \in l) == perfect_square (iprod l).
(* Un élément distinct est la somme des autres *)
Definition prop0 l := (0 \in l) ==
(let sum := foldr addn 0 l in
~~ odd sum && (count (pred1 sum./2) l == 1)).
(* Toutes les propositions *)
Definition check_prop n :=
let l := nat2l n in
[&& prop1 l, prop2 l, prop3 l, prop4 l, prop5 l,
prop6 l, prop7 l, prop8 l, prop9 l& prop0 l].
(* Une version plus rapide *)
Definition fcheck_prop n :=
let l := nat2l n in
if prop9 l then if prop8 l then if prop0 l then if prop6 l then if prop5 l
then if prop4 l then if prop3 l then if prop2 l then if prop1 l then prop7 l
else false else false else false else false else false else false else false
else false else false.
Lemma Pfcheck_prop n : fcheck_prop n = check_prop n.
(* Le résultat *)
Definition result := l2nat [:: 9; 4; 2; 2; 1; 0].
(* Le résultat vérifie les 10 propositions *)
Fact Presult : check_prop result.
(******************************************************************************)
(* *)
(* Tester tous les nombres plus petits que 942210 *)
(* *)
(******************************************************************************)
(* Test à zero sur une liste *)
Definition is_zero l := all (pred1 0) l.
Lemma is_zero_rcons l a : is_zero (rcons l a) = (is_zero l && (a == 0)).
Lemma head_nat2l2_eq0 m n :
n < 10 ^ m -> (nth 1 (nat2l2 m n) 0 == 0) == (n == 0).
Lemma is_zero_nat2l2 m n : n < 10 ^ m -> is_zero (nat2l2 m n) == (n == 0).
(* Remplacer tous les chiffres par des 9 *)
Definition to_nine l := map (fun i : nat => 9) l.
(* Décrémenter de 1 une liste *)
Fixpoint decrr l :=
if l is a :: l1 then
if is_zero l1 then
if a == 0 then to_nine l else a.-1 :: to_nine l1
else a :: decrr l1
else [::].
Definition decr l :=
if is_zero l then [:: 0] else
let l1 := decrr l in
if l1 is 0 :: a :: l2 then a :: l2 else l1.
Lemma decrr_rcons l a :
decrr (rcons l a) =
if (a == 0) then rcons (decrr l) 9 else rcons l a.-1.
Lemma Pdecrr m n : n < 10 ^ m -> 0 < n ->
let l1 := decrr (nat2l2 m n) in
(if l1 is 0 :: a :: l2 then a :: l2 else l1) = nat2l2 m n.-1.
Lemma Pdecr n : decr (nat2l n) = nat2l n.-1.
(* Une version plus efficace pour vérifier les propositions *)
Definition check_propl l :=
if prop9 l then
if prop8 l then
if prop0 l then
if prop6 l then
if prop5 l then
if prop4 l then
if prop3 l then
if prop2 l then
if prop1 l then prop7 l else false
else false else false else false else false else false else false
else false else false.
Lemma Pcheck_propl n : check_prop n = check_propl (nat2l n).
(* Vérifier en décrémentant progressivement *)
Fixpoint check_less l n :=
let l1 := decr l in
if n is n1.+1 then check_propl l1 || check_less l1 n1
else false.
Lemma Pcheck_less n m :
check_less (nat2l n) m = false -> forall k, n - m <= k < n -> ~ check_prop k.
(* Tous les nombres plus petits ne vérifient pas les 10 propositions *)
Fact Lresult : forall m, m < result -> ~ check_prop m.
End Nombre.
This page has been generated by coqdoc