Library palindrome
Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import choice fintype tuple div zmodp.
(* Définition d'un palindrome comme un type *)
Section Def.
Variables (n : nat).
(* Un palindrome est un sous-type de n.-tuple *)
(* Predicat qui définit la propriété d'être un palindrome *)
Definition is_pal (pval : n.-tuple 'I_10) :=
((n == 1) || (nth ord0 pval 0 != ord0)) && (rev pval == pval).
(* Le sous-type *)
Inductive pal_type : predArgType :=
Pal (pval : n.-tuple 'I_10) & is_pal pval.
Coercion pval p := let: Pal f _ := p in f.
(* Les structures canoniques associées *)
Canonical pal_subType := Eval hnf in [subType for pval].
Definition pal_eqMixin := Eval hnf in [eqMixin of pal_type by <:].
Canonical pal_eqType := Eval hnf in EqType pal_type pal_eqMixin.
Definition pal_choiceMixin := [choiceMixin of pal_type by <:].
Canonical pal_choiceType := Eval hnf in ChoiceType pal_type pal_choiceMixin.
Definition pal_countMixin := [countMixin of pal_type by <:].
Canonical pal_countType := Eval hnf in CountType pal_type pal_countMixin.
Canonical pal_subCountType := Eval hnf in [subCountType of pal_type].
Definition pal_finMixin := [finMixin of pal_type by <:].
Canonical pal_finType := Eval hnf in FinType pal_type pal_finMixin.
Canonical pal_for_subFinType := Eval hnf in [subFinType of pal_type].
End Def.
(* Une notation pour le type *)
Notation "n .-palindrome" := (pal_type n)
(at level 2, format "n .-palindrome") : type_scope.
(* Une notation pour les palindromes explicites *)
Notation "[ 'palindrome' x1 ; .. ; xn ]" :=
(@Pal _ [tuple of (inZp x1) :: .. [:: (inZp xn)] ..] is_true_true)
(at level 0, format "[ 'palindrome' '[' x1 ; '/' .. ; '/' xn ']' ]")
: form_scope.
(* Un exemple *)
Check [palindrome 1; 2; 3; 3; 2; 1].
(* Ceci échoue *)
(* Check palindrome 1; 4; 3; 3; 2; 1. *)
(* Ceci échoue *)
(* Check palindrome 0; 2; 3; 3; 2; 0. *)
(******************************************************************************)
(* On s'intéresse tout d'abord à la cardinalité *)
(******************************************************************************)
Lemma card_p0 : #|{:0.-palindrome}| = 0.
Lemma card_p1 : #|{:1.-palindrome}| = 10.
(******************************************************************************)
(* Construction d'un palindrome à 2 * (n + 1) éléments à partir d'un élément *)
(* de 0 .. 8 et d'un n.tuple de chiffres *)
(******************************************************************************)
Definition mk_2n1 n (h : 'I_9) (t : n.-tuple 'I_10) :=
let x := lift ord0 h in [tuple of (x :: t) ++ rev (x :: t)].
(* On construit bien un palindrome *)
Lemma Pmk_2n1 n h (t : n.-tuple _) : is_pal (mk_2n1 h t).
(* C'est une fonction injective *)
Lemma mk_2n1_inj n : injective (fun x => Pal (@Pmk_2n1 n x.1 x.2)).
(* C'est une fonction surjective *)
Lemma mk_2n1E n (p : (n.+1 + n.+1).-palindrome) : {x | mk_2n1 x.1 x.2 = p}.
(* On en déduit la cardinalité pour les pairs non nuls *)
Lemma card_p2n1 n : #|{:n.+1.*2.-palindrome}| = 9 * 10 ^ n.
(******************************************************************************)
(* Construction d'un palindrome à 2 * (n + 1) + 1 éléments à partir d'un *)
(* chiffre de 0 .. 8 d'un n tuple et d'un chiffre *)
(******************************************************************************)
Definition mk_1n2 n (h : 'I_9) (m : n.-tuple 'I_10) (t : 'I_ 10) :=
let x := lift ord0 h in [tuple of (x :: m) ++ t :: rev (x :: m)].
(* On construit bien un palindrome *)
Lemma Pmk_1n2 n h (m : n.-tuple _) t : is_pal (mk_1n2 h m t).
(* C'est une fonction injective *)
Lemma mk_1n2_inj n : injective (fun x => Pal (@Pmk_1n2 n x.1.1 x.1.2 x.2)).
(* C'est une fonction surjective *)
Lemma mk_1n2E n (p : (n.+1 + n.+2).-palindrome) :
{x | mk_1n2 x.1.1 x.1.2 x.2 = p}.
(* On en déduit la cardinalité pour les impairs à plus d'un chiffre *)
Lemma card_p1n2 n : #|{:n.+1.*2.+1.-palindrome}| = 9 * 10 ^ n.+1.
(* La solution du problème *)
Fact card_p351 : #|{:351.-palindrome}| = 9 * 10 ^ 175.
(******************************************************************************)
(* On définit la traduction d'un palindrome vers une valeur entière *)
(******************************************************************************)
Section Number.
Variable b : nat.
Let number := seq 'I_b.
Fixpoint num2nat (n : number) :=
if n is i :: n' then i + b * num2nat n' else 0.
Local Notation "`[ n ]" := (num2nat n).
Lemma num2nat_rcons i n :
`[rcons n i] = num2nat n + b ^ size n * i.
Lemma num2nat_lt_size n : `[n] < b ^ size n.
Lemma num2nat_rcons_lt (i1 i2 : 'I_b) n1 n2 :
i1 < i2 -> size n1 = size n2 -> `[rcons n1 i1] < `[rcons n2 i2].
End Number.
Notation "`[ n ]" := (num2nat n).
(* On décompose un palindrome par une paire de sa tête et son corps *)
Lemma rev_tupleE m (n : m.+2.-tuple 'I_10) (Hr : rev n = n) :
{p : _ * m.-tuple _ |
let (a,n1) := p in n = [tuple of a :: rcons n1 a] /\ rev n1 = n1}.
(* Une première borne pour tous les tuples >= 2 *)
Lemma lbound_2p m (n1 n2 : m.+2.-tuple 'I_10) :
rev n1 = n1 -> rev n2 = n2 -> `[n1] < `[n2] -> 9 + `[n1] < `[n2].
(* La même preuve avec une borne de 1 plus large *)
Lemma lbound_2p1 m (n1 n2 : m.+2.-tuple 'I_10) :
rev n1 = n1 -> rev n2 = n2 -> `[n1] < `[n2] -> 9 + (m != 1) + `[n1] < `[n2].
(* Propriété d'être un palindrome pour a.+1 b ... b a.+1 *)
Lemma pmk_prop n (a : 'I_9) b :
let a' := lift ord0 a in is_pal [tuple of a' :: rcons (nseq n b) a'].
(******************************************************************************)
(* Distance entre deux palindromes *)
(******************************************************************************)
Definition dist_pal n (p1 p2 : n.-palindrome) := `[p2] - `[p1].
Notation " `d[ p1 , p2 ] " := (dist_pal p1 p2).
(* Pour calculer la distance minimale, on exhibe d'abord deux palindromes qui *)
(* se trouvent à cette distance *)
(* Premier palindrome défini par cas: *)
(* palindrome 1 : 1.-palindrome *)
(* palindrome 1; 1 : 2.-palindrome *)
(* palindrome 1; 0; 1 : 3.-palindrome *)
(* palindrome 1; 9; 9 ; 1 : 4.-palindrome *)
(* palindrome 1; 9; ...; 9 ; 1 : n.-palindrome *)
Definition p1 n : n.+1.-palindrome :=
if n is n1.+1 then
Pal (pmk_prop n1 (inZp 0) (inZp (9 * (n != 2)))) else [palindrome 1].
(* Deuxième palindrome défini par cas: *)
(* palindrome 2 : 1.-palindrome *)
(* palindrome 2; 2 : 2.-palindrome *)
(* palindrome 1; 1; 1 : 3.-palindrome *)
(* palindrome 2; 0; 0 ; 2 : 4.-palindrome *)
(* palindrome 2; 0; ...; 0 ; 2 : n.-palindrome *)
Definition p2 n : n.+1.-palindrome :=
if n is n1.+1 then
Pal (pmk_prop n1 (inZp (n != 2)) (inZp (n == 2))) else [palindrome 2].
(* Distance entre p1 et p2: *)
(* pour le 1.-palindrome = 1 *)
(* pour le 2.-palindrome = 11 *)
(* pour le 3.-palindrome = 10 *)
(* pour le k.-palindrome = 11 *)
Lemma dist_p1_p2E n :
`d[p1 n, p2 n] = if n is n1.+1 then if n != 2 then 11 else 10 else 1.
(* La distance entre p1 et p2 est bien la distance minimale *)
Lemma dist_pal_max_min_bound n (p q : n.+1.-palindrome) :
0 < `d[p, q] -> `d[p1 n, p2 n] <= `d[p, q].
(* La solution *)
Fact dist351 :
(exists p q : 351.-palindrome, `d[p, q] = 11) /\
(forall p q : 351.-palindrome, 0 < `d[p, q] -> 11 <= `d[p, q]).
Require Import choice fintype tuple div zmodp.
(* Définition d'un palindrome comme un type *)
Section Def.
Variables (n : nat).
(* Un palindrome est un sous-type de n.-tuple *)
(* Predicat qui définit la propriété d'être un palindrome *)
Definition is_pal (pval : n.-tuple 'I_10) :=
((n == 1) || (nth ord0 pval 0 != ord0)) && (rev pval == pval).
(* Le sous-type *)
Inductive pal_type : predArgType :=
Pal (pval : n.-tuple 'I_10) & is_pal pval.
Coercion pval p := let: Pal f _ := p in f.
(* Les structures canoniques associées *)
Canonical pal_subType := Eval hnf in [subType for pval].
Definition pal_eqMixin := Eval hnf in [eqMixin of pal_type by <:].
Canonical pal_eqType := Eval hnf in EqType pal_type pal_eqMixin.
Definition pal_choiceMixin := [choiceMixin of pal_type by <:].
Canonical pal_choiceType := Eval hnf in ChoiceType pal_type pal_choiceMixin.
Definition pal_countMixin := [countMixin of pal_type by <:].
Canonical pal_countType := Eval hnf in CountType pal_type pal_countMixin.
Canonical pal_subCountType := Eval hnf in [subCountType of pal_type].
Definition pal_finMixin := [finMixin of pal_type by <:].
Canonical pal_finType := Eval hnf in FinType pal_type pal_finMixin.
Canonical pal_for_subFinType := Eval hnf in [subFinType of pal_type].
End Def.
(* Une notation pour le type *)
Notation "n .-palindrome" := (pal_type n)
(at level 2, format "n .-palindrome") : type_scope.
(* Une notation pour les palindromes explicites *)
Notation "[ 'palindrome' x1 ; .. ; xn ]" :=
(@Pal _ [tuple of (inZp x1) :: .. [:: (inZp xn)] ..] is_true_true)
(at level 0, format "[ 'palindrome' '[' x1 ; '/' .. ; '/' xn ']' ]")
: form_scope.
(* Un exemple *)
Check [palindrome 1; 2; 3; 3; 2; 1].
(* Ceci échoue *)
(* Check palindrome 1; 4; 3; 3; 2; 1. *)
(* Ceci échoue *)
(* Check palindrome 0; 2; 3; 3; 2; 0. *)
(******************************************************************************)
(* On s'intéresse tout d'abord à la cardinalité *)
(******************************************************************************)
Lemma card_p0 : #|{:0.-palindrome}| = 0.
Lemma card_p1 : #|{:1.-palindrome}| = 10.
(******************************************************************************)
(* Construction d'un palindrome à 2 * (n + 1) éléments à partir d'un élément *)
(* de 0 .. 8 et d'un n.tuple de chiffres *)
(******************************************************************************)
Definition mk_2n1 n (h : 'I_9) (t : n.-tuple 'I_10) :=
let x := lift ord0 h in [tuple of (x :: t) ++ rev (x :: t)].
(* On construit bien un palindrome *)
Lemma Pmk_2n1 n h (t : n.-tuple _) : is_pal (mk_2n1 h t).
(* C'est une fonction injective *)
Lemma mk_2n1_inj n : injective (fun x => Pal (@Pmk_2n1 n x.1 x.2)).
(* C'est une fonction surjective *)
Lemma mk_2n1E n (p : (n.+1 + n.+1).-palindrome) : {x | mk_2n1 x.1 x.2 = p}.
(* On en déduit la cardinalité pour les pairs non nuls *)
Lemma card_p2n1 n : #|{:n.+1.*2.-palindrome}| = 9 * 10 ^ n.
(******************************************************************************)
(* Construction d'un palindrome à 2 * (n + 1) + 1 éléments à partir d'un *)
(* chiffre de 0 .. 8 d'un n tuple et d'un chiffre *)
(******************************************************************************)
Definition mk_1n2 n (h : 'I_9) (m : n.-tuple 'I_10) (t : 'I_ 10) :=
let x := lift ord0 h in [tuple of (x :: m) ++ t :: rev (x :: m)].
(* On construit bien un palindrome *)
Lemma Pmk_1n2 n h (m : n.-tuple _) t : is_pal (mk_1n2 h m t).
(* C'est une fonction injective *)
Lemma mk_1n2_inj n : injective (fun x => Pal (@Pmk_1n2 n x.1.1 x.1.2 x.2)).
(* C'est une fonction surjective *)
Lemma mk_1n2E n (p : (n.+1 + n.+2).-palindrome) :
{x | mk_1n2 x.1.1 x.1.2 x.2 = p}.
(* On en déduit la cardinalité pour les impairs à plus d'un chiffre *)
Lemma card_p1n2 n : #|{:n.+1.*2.+1.-palindrome}| = 9 * 10 ^ n.+1.
(* La solution du problème *)
Fact card_p351 : #|{:351.-palindrome}| = 9 * 10 ^ 175.
(******************************************************************************)
(* On définit la traduction d'un palindrome vers une valeur entière *)
(******************************************************************************)
Section Number.
Variable b : nat.
Let number := seq 'I_b.
Fixpoint num2nat (n : number) :=
if n is i :: n' then i + b * num2nat n' else 0.
Local Notation "`[ n ]" := (num2nat n).
Lemma num2nat_rcons i n :
`[rcons n i] = num2nat n + b ^ size n * i.
Lemma num2nat_lt_size n : `[n] < b ^ size n.
Lemma num2nat_rcons_lt (i1 i2 : 'I_b) n1 n2 :
i1 < i2 -> size n1 = size n2 -> `[rcons n1 i1] < `[rcons n2 i2].
End Number.
Notation "`[ n ]" := (num2nat n).
(* On décompose un palindrome par une paire de sa tête et son corps *)
Lemma rev_tupleE m (n : m.+2.-tuple 'I_10) (Hr : rev n = n) :
{p : _ * m.-tuple _ |
let (a,n1) := p in n = [tuple of a :: rcons n1 a] /\ rev n1 = n1}.
(* Une première borne pour tous les tuples >= 2 *)
Lemma lbound_2p m (n1 n2 : m.+2.-tuple 'I_10) :
rev n1 = n1 -> rev n2 = n2 -> `[n1] < `[n2] -> 9 + `[n1] < `[n2].
(* La même preuve avec une borne de 1 plus large *)
Lemma lbound_2p1 m (n1 n2 : m.+2.-tuple 'I_10) :
rev n1 = n1 -> rev n2 = n2 -> `[n1] < `[n2] -> 9 + (m != 1) + `[n1] < `[n2].
(* Propriété d'être un palindrome pour a.+1 b ... b a.+1 *)
Lemma pmk_prop n (a : 'I_9) b :
let a' := lift ord0 a in is_pal [tuple of a' :: rcons (nseq n b) a'].
(******************************************************************************)
(* Distance entre deux palindromes *)
(******************************************************************************)
Definition dist_pal n (p1 p2 : n.-palindrome) := `[p2] - `[p1].
Notation " `d[ p1 , p2 ] " := (dist_pal p1 p2).
(* Pour calculer la distance minimale, on exhibe d'abord deux palindromes qui *)
(* se trouvent à cette distance *)
(* Premier palindrome défini par cas: *)
(* palindrome 1 : 1.-palindrome *)
(* palindrome 1; 1 : 2.-palindrome *)
(* palindrome 1; 0; 1 : 3.-palindrome *)
(* palindrome 1; 9; 9 ; 1 : 4.-palindrome *)
(* palindrome 1; 9; ...; 9 ; 1 : n.-palindrome *)
Definition p1 n : n.+1.-palindrome :=
if n is n1.+1 then
Pal (pmk_prop n1 (inZp 0) (inZp (9 * (n != 2)))) else [palindrome 1].
(* Deuxième palindrome défini par cas: *)
(* palindrome 2 : 1.-palindrome *)
(* palindrome 2; 2 : 2.-palindrome *)
(* palindrome 1; 1; 1 : 3.-palindrome *)
(* palindrome 2; 0; 0 ; 2 : 4.-palindrome *)
(* palindrome 2; 0; ...; 0 ; 2 : n.-palindrome *)
Definition p2 n : n.+1.-palindrome :=
if n is n1.+1 then
Pal (pmk_prop n1 (inZp (n != 2)) (inZp (n == 2))) else [palindrome 2].
(* Distance entre p1 et p2: *)
(* pour le 1.-palindrome = 1 *)
(* pour le 2.-palindrome = 11 *)
(* pour le 3.-palindrome = 10 *)
(* pour le k.-palindrome = 11 *)
Lemma dist_p1_p2E n :
`d[p1 n, p2 n] = if n is n1.+1 then if n != 2 then 11 else 10 else 1.
(* La distance entre p1 et p2 est bien la distance minimale *)
Lemma dist_pal_max_min_bound n (p q : n.+1.-palindrome) :
0 < `d[p, q] -> `d[p1 n, p2 n] <= `d[p, q].
(* La solution *)
Fact dist351 :
(exists p q : 351.-palindrome, `d[p, q] = 11) /\
(forall p q : 351.-palindrome, 0 < `d[p, q] -> 11 <= `d[p, q]).
This page has been generated by coqdoc