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]).


This page has been generated by coqdoc