文字列と自然数の相互変換(証明付き)。

string_nat_with_proof.v

(** numeral string <-> nat *)
Require Import Arith List Omega Ascii String.
Require Import Recdef Wf_nat Program.Wf Program.Tactics.
Require Import ProofIrrelevance.

Set Implicit Arguments.
Unset Strict Implicit.

(** * 0. Utilities  *)
Notation "x .!" := (proj1_sig x) (at level 2, left associativity, format "x .!").

Notation "x .p" := (proj2_sig x) (at level 2, left associativity, format "x .p").

Notation "x .1" := (fst x) (at level 2, left associativity, format "x .1").
Notation "x .2" := (snd x) (at level 2, left associativity, format "x .2").

Lemma subset_eq:
  forall (X: Type)(P: X -> Prop)(x: X)(H1 H2: P x),
    exist P x H1 = exist P x H2.
Proof.
  now intros; apply subset_eq_compat.
Qed.

Lemma subset_eq_predicate:
  forall (X: Type)(P: X -> Prop)(Q: sig P -> Prop)(x y: sig P),
    x.! = y.! -> Q x -> Q y.
Proof.
  intros X P Q x y Heq; destruct x as [x Hx], y as [y Hy]; simpl in *.
  now rewrite (subset_eq_compat X P x y Hx Hy Heq).
Qed.
             
(** * 1. Predicates and Types *)
(** ** 1.1. decimal (< 10) type  *)
Notation lt_10 := (fun n => n < 10).

Definition decimal := (sig lt_10).

Definition make_decimal (n: nat)(Hn: lt_10 n): decimal :=
  exist _ n Hn.
Arguments make_decimal n Hn /.

Obligation Tactic := simpl; auto with arith.

Program Definition dc0: decimal := exist lt_10 0 _.
Program Definition dc1: decimal := exist lt_10 1 _.
Program Definition dc2: decimal := exist lt_10 2 _.
Program Definition dc3: decimal := exist lt_10 3 _.
Program Definition dc4: decimal := exist lt_10 4 _.
Program Definition dc5: decimal := exist lt_10 5 _.
Program Definition dc6: decimal := exist lt_10 6 _.
Program Definition dc7: decimal := exist lt_10 7 _.
Program Definition dc8: decimal := exist lt_10 8 _.
Program Definition dc9: decimal := exist lt_10 9 _.

Obligation Tactic := program_simpl.

Lemma decimal_ind:
  forall (P: decimal -> Prop),
    P dc0 ->
    P dc1 ->
    P dc2 ->
    P dc3 ->
    P dc4 ->
    P dc5 ->
    P dc6 ->
    P dc7 ->
    P dc8 ->
    P dc9 ->
    forall d, P d.
Proof.
  intros H; intros; rename H into P.
  destruct d as [n Hn].
  destruct n as [|[|[|[|[|[|[|[|[|[| n]]]]]]]]]]; try omega.
  - now revert H0; apply subset_eq_predicate.
  - now revert H1; apply subset_eq_predicate.
  - now revert H2; apply subset_eq_predicate.
  - now revert H3; apply subset_eq_predicate.
  - now revert H4; apply subset_eq_predicate.
  - now revert H5; apply subset_eq_predicate.
  - now revert H6; apply subset_eq_predicate.
  - now revert H7; apply subset_eq_predicate.
  - now revert H8; apply subset_eq_predicate.
  - now revert H9; apply subset_eq_predicate.
Qed.  

Coercion id_decimal_nat (d: decimal) := d.!.
Arguments id_decimal_nat _ /.


(** ** 1.2. numeral and numerals  *)
Open Scope string_scope.
Infix "::" := String: string_scope.

Fixpoint contain (c: ascii)(s: string) :=
  match s with
  | "" => False
  | c' :: s' => c = c' \/ contain c s'
  end.

Definition numeral (c: ascii) := contain c "0123456789".

Definition nchar := (sig numeral).

Definition make_nchar (c: ascii)(Hc: numeral c) :=
  exist numeral c Hc.
Arguments make_nchar c Hc /.

Open Scope char_scope.
Obligation Tactic := repeat ((now left) ||right).

Program Definition nc0: nchar := exist numeral "0" _.
Program Definition nc1: nchar := exist numeral "1" _.
Program Definition nc2: nchar := exist numeral "2" _.
Program Definition nc3: nchar := exist numeral "3" _.
Program Definition nc4: nchar := exist numeral "4" _.
Program Definition nc5: nchar := exist numeral "5" _.
Program Definition nc6: nchar := exist numeral "6" _.
Program Definition nc7: nchar := exist numeral "7" _.
Program Definition nc8: nchar := exist numeral "8" _.
Program Definition nc9: nchar := exist numeral "9" _.

Obligation Tactic := program_simpl.

Lemma nchar_ind:
  forall (P: nchar -> Prop),
    P nc0 ->
    P nc1 ->
    P nc2 ->
    P nc3 ->
    P nc4 ->
    P nc5 ->
    P nc6 ->
    P nc7 ->
    P nc8 ->
    P nc9 ->
    forall c, P c.
Proof.
  intros H; intros; rename H into P.
  destruct c as [c Hc].
  repeat destruct Hc as [Heq | Hc]; subst; try (now elim Hc); auto.
Qed.

Coercion id_nchar_ascii (c: nchar) := c.!.
Arguments id_nchar_ascii _ /.

Inductive numerals: string -> Prop :=
| numerals_numeral
  : forall (c: ascii), numeral c -> numerals (c :: "")
| numerals_String
  : forall (c: ascii)(s: string),
    numeral c -> numerals s -> numerals (c :: s).
Hint Constructors numerals.

Definition nstring := (sig numerals).

Definition make_nstring (s: string)(Hs: numerals s) :=
  exist numerals s Hs.
Arguments make_nstring s Hs /.

Coercion id_nstring_string (s: nstring) := s.!.
Arguments id_nstring_string _ /.


Definition nstring_nchar (c: nchar): nstring :=
  make_nstring (numerals_numeral c.p).
Arguments nstring_nchar c /.

Definition nstring_cons (c: nchar)(s: nstring): nstring :=
  make_nstring (numerals_String c.p s.p).
Arguments nstring_cons c s /.

Lemma nstring_ind:
  forall (P: nstring -> Prop),
    (forall (c: nchar), P (nstring_nchar c)) ->
    (forall (c: nchar)(s: nstring),
        P s -> P (nstring_cons c s)) ->
    forall (s: nstring), P s.
Proof.
  intros P IHc IHcs [s Hs].
  revert P IHc IHcs Hs; induction s as [| c s IH]; [inversion Hs |].
  intros; inversion Hs.
  - subst; rename H0 into Hc.
    generalize (IHc (make_nchar Hc)).
    now apply subset_eq_predicate.
  - subst c0 s0.
    rewrite (proof_irrelevance _ _ (numerals_String H1 H2)); clear Hs.
    rename c into c', s into s', H1 into Hc, H2 into Hs.
    remember (make_nchar Hc) as c.
    remember (make_nstring Hs) as s.
    replace (exist numerals (c' :: s') (numerals_String Hc Hs)) with (nstring_cons c s); [| apply subset_eq_compat; subst; auto].
    clear Hc Heqc c'.
    assert (Heqs': s' = s.!); [subst; auto |].
    rewrite Heqs' in IH.
    now apply (IH (fun s => forall c, P (nstring_cons c s))); auto.
Qed.  

(** Renaming  *)
Notation len := List.length.
Notation size := String.length.

(** * 2. Basic Definitions  *)
(** ** 2.1. div10  *)
(**
   div10 n = (q, r)
   s.t. n = r + 10 * q
 *)

Fixpoint div10 (n: nat): nat * nat :=
  match n with
  | S (S (S (S (S (S (S (S (S (S n'))))))))) =>
    let (q, r) := div10 n' in (S q, r)
  | d => (0, d)
  end.
Functional Scheme div10_ind := Induction for div10 Sort Prop.

Lemma div10_quo_lt:
  forall (n: nat), (div10 n).1 < n \/ n = 0.
Proof.
  intros n; functional induction div10 n; auto with arith.
  left; rewrite e9 in IHp; simpl in *.
  destruct IHp as [Hlt | Heq];
    [| subst; simpl in e9; inversion e9; subst]; omega.
Qed.

Lemma div10_rem_lt:
  forall (n: nat), (div10 n).2 < 10.
Proof.
  intros n.
  functional induction div10 n; simpl; auto with arith.
  now rewrite e9 in IHp.
Qed.

Definition div10_quo (n: nat): nat :=
  (div10 n).1.
Definition div10_rem (n: nat): decimal :=
  exist lt_10 _ (div10_rem_lt n).

Definition sep10 (n: nat): nat * decimal :=
  (div10_quo n, div10_rem n).

(** sep10s specification  *)
Lemma div10_decomp_aux:
  forall (n q: nat)(r: decimal),
    n = r + 10 * q ->
    div10 n = (q, r.!).
Proof.
  intros n; functional induction div10 n;
    try (now intros q [r Hlt] Heq; assert (q = 0); [omega | subst];
         simpl in *; rewrite plus_comm in Heq;
         simpl in Heq; subst; auto).
  rename n' into n; rewrite e9 in IHp; clear e9.
  intros q' r' Heq; simpl (exist _ _ _).! in *.
  destruct q' as [| q']; [destruct r'; simpl in Heq; omega |].
  rewrite <- mult_n_Sm, (plus_comm _ 10), Nat.add_shuffle3 in Heq.
  set (r' + 10 * q') as n' in Heq.
  simpl in Heq; do 10 apply eq_add_S in Heq; subst n'.
  apply IHp in Heq; auto.
  now inversion Heq; subst.
Qed.

Lemma div10_decomp:
  forall (q: nat)(r: decimal),
    div10 (r + 10 * q) = (q, r.!).
Proof.
  now intros; apply div10_decomp_aux.
Qed.

Lemma div10_quo_decomp:
  forall (q: nat)(r: decimal),
    div10_quo (r + 10 * q) = q.
Proof.
  now intros; unfold div10_quo; rewrite div10_decomp.
Qed.

Lemma div10_rem_decomp:
  forall (q: nat)(r: decimal),
    div10_rem (r + 10 * q) = r.
Proof.
  intros q [r Hltr]; unfold div10_rem.
  apply subset_eq_compat.
  now rewrite div10_decomp.
Qed.

Lemma sep10_decomp:
  forall (q: nat)(r: decimal),
    sep10 (r + 10 * q) = (q, r).
Proof.
  intros; unfold sep10.
  now rewrite div10_quo_decomp, div10_rem_decomp.
Qed.

Lemma div10_decomp_inv:
  forall (n q: nat)(r: decimal),
    div10 n = (q, r.!) -> n = r + 10 * q.
Proof.
  intros n; functional induction div10 n;
    try (now intros q [r Hltr] Heq; inversion Heq; subst; auto with arith).
  rename n' into n.
  intros q' r' Heq; inversion Heq; subst.
  rewrite (IHp _ _ e9); ring.
Qed.

Lemma div10_decomp_exists:
  forall (n: nat),
  exists (q: nat)(r: decimal), (n = r + 10 * q).
Proof.
  intros; exists (div10_quo n), (div10_rem n).
  apply div10_decomp_inv.
  unfold div10_quo, div10_rem; simpl.
  now destruct (div10 n).
Qed.

Lemma nat_decomp_div10:
  forall (n: nat), n = (div10_rem n) + 10 * (div10_quo n).
Proof.
  intros n.
  destruct (div10_decomp_exists n) as [q [r Heq]].
  now subst n; rewrite div10_quo_decomp, div10_rem_decomp.
Qed.

Lemma sep10_decomp_inv:
  forall (n q: nat)(r: decimal),
    sep10 n = (q, r) -> n = r + 10 * q.
Proof.
  intros n q r Heq; apply div10_decomp_inv.
  unfold sep10 in Heq.
  inversion Heq; clear.
  now rewrite <- div10_decomp, <- nat_decomp_div10.
Qed.

Lemma lt_ind:
  forall (P: nat -> Prop),
    P 0 ->
    (forall n, (forall m, m < n -> P m) -> P n) ->
    forall n, P n.
Proof.
  intros P IHz IHlt n; revert P IHz IHlt.
  induction n as [| n IHn]; auto.
  intros; apply (IHn (fun x => P (S x))).
  - apply IHlt.
    intros m Hltm.
    now assert (Heqm: m = 0); [omega | subst; auto].
  - intros n' H.
    apply IHlt; intros m Hltm.
    apply le_S_n in Hltm.
    apply le_lt_or_eq in Hltm.
    destruct Hltm as [Hltm | Heqm].
    + destruct m as [| m]; auto.
      apply H; omega.
    + subst.
      destruct n' as [| n']; auto.
Qed.
      
Lemma decimals_ind_aux:
  forall (P: nat -> decimal -> Prop),
    (forall (r: decimal), P 0 r) ->
    (forall (q: nat)(r: decimal),
        P q r ->
        forall (r': decimal), P (r + 10 * q) r') ->
    forall (q: nat)(r: decimal), P q r.
Proof.
  intros P Hrem Hquo q r; revert P Hrem Hquo r.
  pattern q.
  apply lt_ind; auto.
  clear q; intros q IH; intros.
  rewrite (nat_decomp_div10 q).
  apply Hquo.
  destruct (div10_quo_lt q) as [Hltq | Heqq]; [| subst; auto].
  now apply IH; auto.
Qed.  

Lemma decimals_ind:
  forall (P: nat -> Prop),
    (forall (r: decimal), P r) ->
    (forall q, 0 < q -> P q -> forall (r: decimal), P (r + 10 * q)) ->
    forall n, P n.
Proof.
  intros P Hrem Hquo n.
  rewrite nat_decomp_div10.
  pattern (div10_quo n), (div10_rem n).
  apply decimals_ind_aux.
  - now intros; rewrite plus_0_r.
  - intros q r Hp.
    assert (H: r + 10 * q = 0 \/ 0 < r + 10 * q); [omega |].
    destruct H as [Heq | Hlt].
    + now intros; rewrite Heq, plus_0_r; apply Hrem. 
    + now intros; apply Hquo; auto.
Qed.    

(** ** 1.2. decompose into decimals  *)
Open Scope list_scope.
Notation dlist := (list decimal).

Function decimals_aux (acc: dlist)(n: nat){wf lt n}: dlist :=
  let (q, r) := sep10 n in
  match q with
  | O => r :: acc
  | S q' => decimals_aux (r :: acc) q
  end.
Proof.
  - intros _ n q r q' Heqq Heqn.
    unfold sep10, div10_quo in Heqn.
    generalize (div10_quo_lt n).
    inversion Heqn.
    intros [Hlt | Heq]; auto.
    subst; simpl in *; discriminate.
  - now apply lt_wf.
Defined.

Definition decimals: nat -> dlist := decimals_aux nil.

Lemma decimals_aux_decomp:
  forall (acc: dlist)(q: nat)(r: decimal),
    0 < q ->
    decimals_aux acc (r + 10 * q) = decimals_aux (r :: acc) q.
Proof.
  intros acc q r Hltq.
  rewrite decimals_aux_equation, sep10_decomp.
  now destruct q; [omega |].
Qed.

Lemma sep10_eq_rem:
  forall (n: nat)(r: decimal),
    sep10 n = (0, r) -> n = r.
Proof.
  intros n r Heq.
  apply sep10_decomp_inv in Heq; omega.
Qed.  

Lemma sep10_decimal:
  forall (r: decimal),
    sep10 r = (0, r).
Proof.
  now intros r; rewrite <- sep10_decomp, plus_0_r.
Qed.  

Lemma decimals_aux_decomp_rem:
  forall (acc: dlist)(r: decimal),
    decimals_aux acc r = r :: acc.
Proof.
  intros acc r.
  now rewrite decimals_aux_equation, sep10_decimal.
Qed.    

Lemma decimals_decomp_rem:
  forall (r: decimal), decimals r = r :: nil.
Proof.
  intros n; unfold decimals.
  now apply decimals_aux_decomp_rem.
Qed.
  
Lemma decimals_aux_app_aux:
  forall (acc acc1 acc2: dlist)(n: nat),
    acc = acc1 ++ acc2 ->
    decimals_aux acc n = decimals_aux acc1 n ++ acc2.
Proof.
  intros acc acc1 acc2 n; revert acc1 acc2.
  functional induction decimals_aux acc n.
  - intros acc1 acc2 Heq; subst.
    apply sep10_decomp_inv in e; rewrite plus_0_r in e; subst.
    now rewrite decimals_aux_decomp_rem.
  - intros acc1 acc2 Heq; subst.
    rewrite (IHl (r :: acc1) acc2); auto; clear IHl.
    now rewrite (sep10_decomp_inv e), decimals_aux_decomp;
      auto with arith.
Qed.

Lemma decimals_aux_app:
  forall (acc1 acc2: dlist)(n: nat),
    decimals_aux (acc1 ++ acc2) n = decimals_aux acc1 n ++ acc2.
Proof.
  now intros; apply decimals_aux_app_aux.
Qed.

Lemma decimals_decomp:
  forall (q: nat)(r: decimal),
    0 < q ->
    decimals (r + 10 * q) = decimals q ++ (r :: nil).
Proof.
  intros q r Hltq; unfold decimals.
  now rewrite decimals_aux_decomp, <- decimals_aux_app.
Qed.

Definition sum10 (x: nat)(nl: dlist) :=
  fold_left (fun (q: nat)(r: decimal) => r + 10 * q) nl x.

Lemma sum10_cons:
  forall (x: nat)(d: decimal)(nl: dlist),
    sum10 x (d :: nl) = sum10 (d + 10 * x) nl.
Proof.
  now intros; unfold sum10.
Qed.  

Lemma fold_left_cons:
  forall (A B: Type)(f: A -> B -> A)(l: list B)(e: A)(x: B),
    fold_left f (x :: l) e = fold_left f l (f e x).
Proof.
  reflexivity.
Qed.

Lemma fold_left_map:
  forall (A B C: Type)(f: B -> C)(op: A -> C -> A)(l: list B)(e: A),
    fold_left op (map f l) e = fold_left (fun x y => op x (f y)) l e.
Proof.
  induction l as [| b l IH]; auto.
  simpl; intros.
  now rewrite IH.
Qed.

Lemma sum10_decimals_aux:
  forall (n: nat)(acc: dlist),
    sum10 0 (decimals_aux acc n) = sum10 n acc.
Proof.
  intros n acc.
  functional induction decimals_aux acc n.
  - apply sep10_decomp_inv in e; rewrite plus_0_r in e; subst n.
    now rewrite sum10_cons, plus_0_r.
  - apply sep10_decomp_inv in e; subst n.
    rewrite IHl; clear IHl.
    now rewrite sum10_cons.
Qed.

Lemma sum10_decompose:
  forall (n: nat)(acc: dlist),
    sum10 n acc = 10 ^ len acc * n + sum10 0 acc.
Proof.
  intros n acc; revert n.
  induction acc as [| x acc IH]; [simpl; intros; ring |].
  intros r; rewrite !sum10_cons, plus_0_r.
  simpl (len _).
  rewrite Nat.pow_succ_r'.
  rewrite (IH (_ + _)), (IH x), mult_plus_distr_l.
  ring.
Qed.

Lemma decimals_aux_valid:
  forall (n: nat)(acc: dlist),
    sum10 0 (decimals_aux acc n) = 10 ^ len acc * n + sum10 0 acc.
Proof.
  intros n acc.
  now rewrite sum10_decimals_aux, sum10_decompose.
Qed.

Lemma decimals_valid:
  forall (n: nat),
    n = sum10 0 (decimals n).
Proof.
  intros n; unfold decimals.
  generalize (decimals_aux_valid n nil).
  now simpl; rewrite !plus_0_r.
Qed.


(** * 3. Translators  *)
(** ** 3.1. decimal -> nchar *)
Open Scope char_scope.
Obligation Tactic := try now unfold numeral, contain; tauto.

Program Definition decimal_to_nchar (n: decimal): nchar :=
  let (d, H) := n in
  match d as n return n < 10 -> nchar with
  | 0 => fun _ => "0"
  | 1 => fun _ => "1"
  | 2 => fun _ => "2"
  | 3 => fun _ => "3"
  | 4 => fun _ => "4"
  | 5 => fun _ => "5"
  | 6 => fun _ => "6"
  | 7 => fun _ => "7"
  | 8 => fun _ => "8"
  | 9 => fun _ => "9"
  | _ => fun (H: _ < 10) => match (_: False) with end
  end H.
Next Obligation.
  intros; omega.
Qed.
Obligation Tactic := program_simpl.

Notation Forall_inv_head := Forall_inv.

Lemma Forall_inv_tail:
  forall (X: Type)(P: X -> Prop)(x: X)(l: list X),
    Forall P (x :: l) -> Forall P l.
Proof.
  now intros X P x l H; inversion H.
Qed.                                     

Lemma Forall_inv_and:
  forall (X: Type)(P: X -> Prop)(x: X)(l: list X),
    Forall P (x :: l) -> P x /\ Forall P l.
Proof.
  now intros X P x l H; inversion H.
Qed.                                     

(** ** 3.2. nat -> numerals  *)
Program Fixpoint plist (X: Type)(l: list X)(P: X -> Prop)(H: Forall P l): list (sig P) :=
  match l as l return Forall P l -> list (sig P) with
  | nil => fun _ => nil
  | x :: xs =>
    fun (H: Forall P (x :: xs)) =>
      (exist P x (Forall_inv_head H)) :: plist (Forall_inv_tail H)
  end H.

Lemma plist_eq_compat:
  forall (X: Type)(l1 l2: list X)(P: X -> Prop)(H1: Forall P l1)(H2: Forall P l2),
    l1 = l2 ->
    plist H1 = plist H2.
Proof.
  intros X l1 l2 P H1 H2 Heq; revert H1 H2; rewrite Heq.
  now intros; rewrite (proof_irrelevance _ H1 H2).
Qed.

Lemma plist_eq:
  forall (X: Type)(l: list X)(P: X -> Prop)(H1 H2: Forall P l),
    plist H1 = plist H2.
Proof.
  now intros; apply plist_eq_compat.
Qed.

Notation nclist := (list nchar).

Definition nat_to_nstring_aux (n: nat): nclist :=
  map decimal_to_nchar (decimals n).

Lemma decimals_aux_not_nil:
  forall (acc: dlist)(n: nat),
    0 < len (decimals_aux acc n).
Proof.
  intros acc n; functional induction decimals_aux acc n.
  - now simpl; auto with arith.
  - now apply IHl.
Qed.

Lemma decimals_not_nil:
  forall (n: nat), 0 < len (decimals n).
Proof.
  now intros; apply decimals_aux_not_nil.
Qed.

Program Fixpoint nclist_to_nstring (l: nclist)(H: 0 < len l) {struct l}
  : nstring :=
  match l as l return 0 < len l -> nstring with
  | nil => fun (H: 0 < 0) => match (lt_irrefl _ H) with end
  | c :: xs =>
    fun (H: 0 < S (len xs)) =>
      let (c, Hc) := c in 
      match zerop (len xs) with
      | left _ => exist numerals (String c "") _
      | right Hlt =>
        let (s, Hs) := nclist_to_nstring Hlt in
        exist numerals (String c s) _
      end
  end H.

Lemma nclist_to_nstring_eq_compat:
  forall (l1 l2: nclist)(H1: 0 < len l1)(H2: 0 < len l2),
    l1 = l2 ->
    nclist_to_nstring H1 = nclist_to_nstring H2.
Proof.
  induction l1 as [| c1 l1 IH1].
  - now intros [|] H1 H2; [| discriminate];
      rewrite (proof_irrelevance _ _ H2).
  - intros [| c2 l2] H1 H2 Heq; [discriminate |].
    inversion Heq; subst; clear Heq.
    now rewrite (proof_irrelevance _ _ H2).
Qed.
  
Lemma nclist_to_nstring_eq:
  forall (l: nclist)(H1 H2: 0 < len l),
    nclist_to_nstring H1 = nclist_to_nstring H2.
Proof.
  now intros; apply nclist_to_nstring_eq_compat.
Qed.
  
Lemma plist_length:
  forall (X: Type)(P: X -> Prop)(l: list X)(H: Forall P l),
    len (plist H) = len l.
Proof.
  now induction l; simpl; auto.
Qed.

Lemma nat_to_nstring_aux_not_nil:
  forall (n: nat),
    0 < len (nat_to_nstring_aux n).
Proof.
  intros; unfold nat_to_nstring_aux.
  rewrite map_length.
  now apply decimals_aux_not_nil.
Qed.

(** nat `n`
    [decimals]
    -> nchar list of `n` (= decimals n)
    [map decimal_to_nchar]
    -> ascii list of `n`
    [nclist_to_nstring]
    -> numeral string
  *)
Definition nat_to_nstring (n: nat): nstring :=
  nclist_to_nstring (nat_to_nstring_aux_not_nil n).

Open Scope list_scope.
Lemma plist_app:
  forall (X: Type)(P: X -> Prop)(l1 l2: list X)
    (H1: Forall P l1)(H2: Forall P l2)(Happ: Forall P (l1 ++ l2)),
    plist Happ = plist H1 ++ plist H2.
Proof.
  induction l1 as [| x l1 IH]; simpl; intros; [now apply plist_eq |].
  apply f_equal2; [now apply subset_eq |].
  now apply IH.
Qed.

Open Scope list_scope.
Lemma Forall_app:
  forall (X: Type)(P: X -> Prop)(l1 l2: list X),
    Forall P l1 -> Forall P l2 ->
    Forall P (l1 ++ l2).
Proof.
  induction l1 as [| x l1 IH1]; auto.
  simpl; intros.
  apply Forall_inv_and in H; destruct H.
  now apply Forall_cons; auto.
Qed.  

Lemma plist_app':
  forall (X: Type)(P: X -> Prop)(l1 l2: list X)
    (H1: Forall P l1)(H2: Forall P l2),
    plist (Forall_app H1 H2) = plist H1 ++ plist H2.
Proof.
  now intros; apply plist_app.
Qed.

Lemma nat_to_nstring_aux_decomp:
  forall (q: nat)(r: decimal),
    0 < q ->
    nat_to_nstring_aux (r + 10 * q) =
    nat_to_nstring_aux q ++ (decimal_to_nchar r :: nil).
Proof.
  unfold nat_to_nstring_aux.
  intros q r Hltq.
  now rewrite decimals_decomp, map_app; auto.
Qed.  

Lemma nat_to_nstring_aux_decomp_rem:
  forall (r: decimal),
    nat_to_nstring_aux r =
    decimal_to_nchar r :: nil.
Proof.
  intros r.
  unfold nat_to_nstring_aux.
  now rewrite decimals_decomp_rem.
Qed.  

Lemma nstring_app_numerals:
  forall (s1 s2: nstring),
    numerals (s1 ++ s2).
Proof.
  induction s1 using nstring_ind; auto.
  - now destruct c; intros [s2 Hs2]; simpl; auto.
  - destruct c as [c Hc]; intros s2; simpl.
    now apply numerals_String.
Qed.

Open Scope string_scope.
Definition napp (s1 s2: nstring): nstring :=
  exist numerals (s1 ++ s2) (nstring_app_numerals s1 s2).

Lemma nstring_cons_napp:
  forall c s, nstring_cons c s = napp (nstring_nchar c) s.
Proof.
  now intros c s; unfold napp; simpl; apply subset_eq.
Qed.

Lemma app_length_lt:
  forall (X: Type)(l1 l2: list X),
    0 < len l1 -> 0 < len l2 ->
    0 < len (l1 ++ l2).
Proof.
  intros; rewrite app_length, <- (plus_0_r 0).
  now apply plus_lt_compat.
Qed.

Lemma nclist_to_nstring_cons:
  forall (c: nchar)(l: nclist)(H: 0 < len l),
    nclist_to_nstring (l := c :: l) (Nat.lt_lt_succ_r _ _ H)
    = nstring_cons c (nclist_to_nstring H).
Proof.
  intros c l; revert c.
  induction l as [| c' l IH]; intros.
  - now elim (lt_irrefl _ H).
  -
    simpl in H.
    generalize (le_lt_or_eq _ _ H); intros [Hlt | Heq].
    + apply lt_S_n in Hlt.
      generalize (IH c' Hlt); clear IH.
      rewrite (proof_irrelevance _ _ H).
      intros Heq; rewrite Heq; clear Heq.
      simpl (len _).
      simpl.
      assert (Heq: zerop (len l) = right Hlt).
      {
        destruct l; simpl.
        - now elim (lt_irrefl _ Hlt).
        - now rewrite (proof_irrelevance _ _ Hlt).
      }
      rewrite Heq.
      destruct c, c'.
      destruct (nclist_to_nstring Hlt).
      now simpl; apply subset_eq.
    + apply eq_add_S in Heq.
      assert (l = nil).
      {
        now destruct l; try discriminate.
      }
      subst l; simpl.
      destruct c as [c Hc], c' as [c' Hc']; simpl.
      now apply subset_eq.
Qed.    

Lemma napp_valid:
  forall (l1 l2: nclist)
     (H1: 0 < len l1)
     (H2: 0 < len l2),
    nclist_to_nstring (app_length_lt H1 H2) =
    napp (nclist_to_nstring H1) (nclist_to_nstring H2).
Proof.
  induction l1 as [| c l1 IH]; intros.
  - now elim (lt_irrefl _ H1).
  - simpl ((_ :: _) ++ l2)%list.
    assert (H: 0 < len (l1 ++ l2)).
    {
      rewrite app_length.
      now apply Nat.add_pos_r.
    }
    generalize (nclist_to_nstring_cons c H); intros Heq.
    rewrite (proof_irrelevance _ _ (app_length_lt H1 H2)) in Heq.
    rewrite Heq; clear Heq.
    revert c H1.
    case_eq (zerop (len l1)).
    + intros e Heq c Hlt; simpl.
      rewrite Heq.
      destruct c as [c Hc]; simpl.
      unfold nstring_cons, napp.
      apply subset_eq_compat.
      simpl.
      destruct l1; [| discriminate]; simpl in *.
      now rewrite (proof_irrelevance _ H2 H).
    + intros H1 Heq c Hlt.
      simpl.
      rewrite Heq; clear Heq.
      destruct c as [c Hc]; simpl.
      generalize (IH l2 H1 H2).
      rewrite (proof_irrelevance _ (app_length_lt H1 H2) H).
      intros Heq; rewrite Heq; clear Heq.
      unfold nstring_cons, napp.
      destruct (nclist_to_nstring H1); simpl.
      now apply subset_eq.
Qed.

Lemma nat_to_nstring_decomp_rem:
  forall (r: decimal),
    nat_to_nstring r = nstring_nchar (decimal_to_nchar r).
Proof.
  intros r; unfold nat_to_nstring.
  assert (Hlt: 0 < len (nat_to_nstring_aux r)).
  {
    apply (nat_to_nstring_aux_not_nil r).
  }
  rewrite (proof_irrelevance _ _ Hlt); revert Hlt.
  rewrite nat_to_nstring_aux_decomp_rem.
  set (decimal_to_nchar r) as c; destruct c as [c Hc].
  unfold nstring_nchar.
  simpl; intros _.
  now apply subset_eq.
Qed.

Lemma nat_to_nstring_decomp:
  forall (q: nat)(r: decimal),
    0 < q ->
    nat_to_nstring (r + 10 * q) =
    napp (nat_to_nstring q) (nstring_nchar (decimal_to_nchar r)).
Proof.
  intros q r Hltq.
  rewrite <- nat_to_nstring_decomp_rem.
  unfold nat_to_nstring; intros.
  rewrite <- napp_valid.
  apply nclist_to_nstring_eq_compat.
  rewrite (nat_to_nstring_aux_decomp r Hltq).
  now rewrite nat_to_nstring_aux_decomp_rem.
Qed.

(** ** 3.2. numerals -> nat *)
Open Scope char_scope.
Definition nchar_to_decimal (c: nchar): decimal.
  refine (let (c, Hc) := c in
          match c as c return numeral c -> decimal with
          | "0" => fun Hc => exist lt_10 0 _
          | "1" => fun Hc => exist lt_10 1 _
          | "2" => fun Hc => exist lt_10 2 _
          | "3" => fun Hc => exist lt_10 3 _
          | "4" => fun Hc => exist lt_10 4 _
          | "5" => fun Hc => exist lt_10 5 _
          | "6" => fun Hc => exist lt_10 6 _
          | "7" => fun Hc => exist lt_10 7 _
          | "8" => fun Hc => exist lt_10 8 _
          | "9" => fun Hc => exist lt_10 9 _
          | Ascii b0 b1 b2 b3 b4 b5 b6 b7 =>
            fun H => match (_:False) with end
          end Hc); auto with arith;
    unfold numeral, contain in H;
    destruct H as [H0 |[H1 |[H2 |[H3 |[H4 |[H5 |[H6 |[H7 |[H8 |[H9 | F]]]]]]]]]]; try discriminate; contradiction.
Defined.

Open Scope string_scope.
Fixpoint string_to_ascii_list (s: string): list ascii :=
  match s with
  | "" => nil
  | String c s' => c :: string_to_ascii_list s'
  end.

Lemma nstring_all_numeral:
  forall (s: nstring),
    Forall numeral (string_to_ascii_list s).
Proof.
  induction s using nstring_ind.
  - now destruct c; simpl; auto.
  - simpl; apply Forall_cons; auto.
    now destruct c; simpl; auto.
Qed.

Definition nstring_to_nclist (s: nstring): nclist :=
  plist (nstring_all_numeral s).

Lemma nstring_to_nclist_cons:
  forall (c: nchar)(s: nstring),
    nstring_to_nclist (nstring_cons c s) =
    (c :: nstring_to_nclist s)%list.
Proof.
  unfold nstring_to_nclist; simpl.
  intros; apply f_equal2;
    [destruct c; apply subset_eq | apply plist_eq].
Qed.

Open Scope list_scope.
Lemma string_to_ascii_list_app:
  forall (s1 s2: string),
    string_to_ascii_list (append s1 s2) =
    string_to_ascii_list s1 ++ string_to_ascii_list s2.
Proof.
  induction s1 as [| c s1 IH]; simpl; auto.
  now intros s2; rewrite IH.
Qed.

Lemma nstring_to_nclist_app:
  forall (s1 s2: nstring),
    nstring_to_nclist (napp s1 s2) =
    nstring_to_nclist s1 ++ nstring_to_nclist s2.
Proof.
  intros s1 s2.
  unfold napp, nstring_to_nclist; simpl.
  etransitivity; [| apply plist_app'].
  now apply plist_eq_compat, string_to_ascii_list_app.
Qed.  
  
(* numeral string -> nat *)
Definition nstring_to_nat_aux (m: nat)(s : nstring): nat :=
  sum10 m (map nchar_to_decimal (nstring_to_nclist s)).

Definition nstring_to_nat (s : nstring): nat :=
  nstring_to_nat_aux 0 s.

(* Lemma test: numerals "2361". *)
(* Proof. *)
(*   do 3 (apply numerals_String; [unfold numeral; simpl; tauto |]). *)
(*   apply numerals_numeral; unfold numeral; simpl; tauto. *)
(* Qed. *)

(* Eval compute in nstring_to_nat (exist numerals _ test). *)

Lemma Forall_app_inv:
  forall (X: Type)(P: X -> Prop)(l1 l2: list X),
    Forall P (l1 ++ l2) -> Forall P l1 /\ Forall P l2.
Proof.
  induction l1 as [| x l1 IH1]; auto.
  simpl; intros l2 Hf.
  inversion Hf; subst.
  now split;
    [apply Forall_cons; auto; apply IH1 with l2 | apply IH1].
Qed.

Lemma nstring_to_nat_aux_app:
  forall (m: nat)(s1 s2: nstring),
    nstring_to_nat_aux m (napp s1 s2) =
    nstring_to_nat_aux (nstring_to_nat_aux m s1) s2.
Proof.
  intros m s1 s2; simpl.
  unfold nstring_to_nat_aux.
  rewrite nstring_to_nclist_app, map_app.
  unfold sum10.
  now rewrite fold_left_app.
Qed.

Lemma nstring_length:
  forall (s: nstring), 0 < size s.
Proof.
  intros [s Hs]; destruct s; [inversion Hs |].
  simpl in *; auto with arith.
Qed.

Lemma nclist_to_nstring_length:
  forall (l: nclist)(H: 0 < len l),
    len l = length (nclist_to_nstring H).
Proof.
  induction l as [| x l IH]; intros Hlt; [now elim (lt_n_0 _ Hlt) |].
  simpl in Hlt.
  destruct (le_lt_or_eq _ _ Hlt).
  - apply lt_S_n in H.
    generalize (nclist_to_nstring_cons x H); intros Heq.
    rewrite (proof_irrelevance _ _ Hlt) in Heq; rewrite Heq.
    now simpl; rewrite (IH H).
  - destruct l as [| y l]; [| discriminate].
    now destruct x; simpl.
Qed.

Lemma nstring_to_nat_aux_decomp_nchar:
  forall (m: nat)(c: nchar),
    nstring_to_nat_aux m (nstring_nchar c) = nstring_to_nat_aux 0 (nstring_nchar c) + 10 * m.
Proof.
  intros m c.
  unfold nstring_to_nat_aux.
  now rewrite sum10_decompose, plus_comm.
Qed.

Lemma nstring_to_nat_aux_decomp:
  forall (m: nat)(s: nstring),
    nstring_to_nat_aux m s = nstring_to_nat_aux 0 s + 10 ^ size s * m.
Proof.
  intros m s; revert m.
  induction s using nstring_ind.
  - intros m.
    rewrite nstring_to_nat_aux_decomp_nchar.
    now simpl (size _); simpl (_ ^ _).
  - intros m.
    simpl (size _).
    rewrite nstring_cons_napp.
    rewrite !nstring_to_nat_aux_app.
    rewrite IHs, (IHs (nstring_to_nat_aux 0 _)).
    simpl (size _).
    rewrite nstring_to_nat_aux_decomp_nchar.
    rewrite <- !plus_assoc.
    now rewrite Nat.pow_succ_r', (mult_comm 10 (_ ^ _)), <- mult_assoc, <- mult_plus_distr_l.
Qed.
  
Lemma nstring_to_nat_app:
  forall (s1 s2: nstring),
    nstring_to_nat (napp s1 s2) =
    10 ^ size s2 * nstring_to_nat s1 + nstring_to_nat s2.
Proof.
  intros s1 s2; unfold nstring_to_nat.
  rewrite nstring_to_nat_aux_app.
  now rewrite nstring_to_nat_aux_decomp, plus_comm.
Qed.

Lemma napp_length:
  forall s1 s2, length (napp s1 s2) = length s1 + length s2.
Proof.
  intros [s1 Hs1] [s2 Hs2]; simpl; clear.
  induction s1; auto.
  now simpl; rewrite IHs1.
Qed.

Lemma nchar_to_decimal_to_nchar:
  forall c, decimal_to_nchar (nchar_to_decimal c) = c.
Proof.
  now induction c using nchar_ind; simpl; apply subset_eq.
Qed.

Lemma decimal_to_nchar_to_decimal:
  forall r, nchar_to_decimal (decimal_to_nchar r) = r.
Proof.
  now induction r using decimal_ind; auto.
Qed.

Lemma nat_to_nstring_to_nat_aux_rem:
  forall (m: nat)(r: decimal),
    nstring_to_nat_aux m (nat_to_nstring r) = r + 10 * m.
Proof.
  intros m r.
  rewrite nat_to_nstring_decomp_rem.
  set (decimal_to_nchar r) as c.
  rewrite nstring_to_nat_aux_decomp_nchar.
  apply f_equal2_plus; auto.
  unfold nstring_to_nat_aux.
  unfold nstring_nchar, nstring_to_nclist.
  simpl (plist _).
  rewrite (proof_irrelevance _ _ c.p).
  replace (exist numeral c.! c.p) with c;
    [| destruct c; apply subset_eq].
  simpl; subst c.
  now rewrite plus_0_r, decimal_to_nchar_to_decimal.
Qed.

Lemma nstring_rem_length:
  forall (r: decimal), length (nat_to_nstring r) = 1.
Proof.
  intros r.
  now rewrite nat_to_nstring_decomp_rem; simpl.
Qed.

Lemma nat_to_nstring_to_nat_aux:
  forall (n m: nat),
    nstring_to_nat_aux m (nat_to_nstring n) =
    n + 10 ^ length (nat_to_nstring n) * m. 
Proof.
  induction n using decimals_ind; intros.
  - now rewrite nat_to_nstring_to_nat_aux_rem, nstring_rem_length.
  - rewrite (nat_to_nstring_decomp r H).
    rewrite <- nat_to_nstring_decomp_rem.
    rewrite napp_length, nstring_rem_length.
    rewrite nstring_to_nat_aux_app.
    rewrite IHn.
    rewrite nat_to_nstring_to_nat_aux_rem.
    rewrite (plus_comm _ 1), Nat.pow_succ_r'.
    ring.
Qed.

(* nat -> numerals -> nat *)
Theorem nat_to_nstring_to_nat:
  forall (n: nat),
    nstring_to_nat (nat_to_nstring n) = n.
Proof.
  intros; unfold nstring_to_nat.
  rewrite nat_to_nstring_to_nat_aux; ring.
Qed.

(*  *)
Open Scope string_scope.

Fixpoint normalize_aux (s: string): string :=
  match s with
  | "0" :: (_ :: _) as s' => normalize_aux s'
  | _ => s
  end.

Lemma normalize_aux_ascii:
  forall c, normalize_aux (c :: "") = c :: "".
Proof.
  simpl; intros.
  now destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; simpl.
Qed.

Lemma nstring_not_empty:
  forall s: nstring, s.! <> ""%string.
Proof.
  intros [s Hs]; simpl; intros Heq.
  subst s; inversion Hs.
Qed.

Lemma normalize_aux_valid:
  forall (s: nstring),
    numerals (normalize_aux s).
Proof.
  induction s using nstring_ind.
  - induction c using nchar_ind; simpl;
      apply numerals_numeral; unfold numeral; simpl; tauto.
  - induction c using nchar_ind;
      try (apply numerals_String;
           try (now destruct s);
           unfold numeral; simpl; tauto).
    simpl.
    now destruct s as [[|] Hs]; simpl; auto; inversion Hs.
Qed.

Definition normalize (s: nstring): nstring :=
  exist numerals _ (normalize_aux_valid s).

Open Scope string_scope.
Lemma append_assoc:
  forall (s1 s2 s3: string),
    (s1 ++ s2) ++ s3 = s1 ++ (s2 ++ s3).
Proof.
  induction s1 as [| c1 s1 IH1]; auto.
  now intros; simpl; rewrite IH1.
Qed.

Lemma napp_cons_assoc:
  forall c s1 s2,
    napp (nstring_cons c s1) s2 = nstring_cons c (napp s1 s2).
Proof.
  intros.
  now unfold napp; simpl; apply subset_eq.
Qed.

Lemma napp_assoc:
  forall s1 s2 s3,
    napp (napp s1 s2) s3 = napp s1 (napp s2 s3).
Proof.
  induction s1 using nstring_ind; intros.
  - now rewrite <- !nstring_cons_napp, napp_cons_assoc.
  - now rewrite !napp_cons_assoc, IHs1.
Qed.

Lemma normalize_nchar:
  forall c, normalize (nstring_nchar c) = nstring_nchar c.
Proof.
  intros c; unfold normalize; simpl; apply subset_eq_compat.
  now induction c using nchar_ind; simpl.
Qed.

Lemma normalize_app:
  forall m s,
    0 < m ->
    normalize (napp (nat_to_nstring m) s)
    = napp (nat_to_nstring m) s.
Proof.
  induction m using decimals_ind.
  - intros s Hlt.
    rewrite nat_to_nstring_decomp_rem.
    rewrite <- nstring_cons_napp.
    unfold normalize.
    induction r using decimal_ind; try (now apply subset_eq).
    now elim (lt_n_0 _ Hlt).
  - intros s Hlt.
    rewrite (nat_to_nstring_decomp r H).
    rewrite napp_assoc.
    now rewrite IHm.
Qed.    

Lemma append_length:
  forall (s1 s2: string),
    length (s1 ++ s2) = length s1 + length s2.
Proof.
  induction s1 as [| c1 s1 IH1]; auto; intros; simpl.
  rewrite IH1; ring.
Qed.

Lemma numeral_0: numeral "0".
Proof.
  now left.
Qed.

Definition nat_to_nstring_0:
  nat_to_nstring 0 = nstring_nchar (make_nchar numeral_0).
Proof.
  now unfold nat_to_nstring; simpl; apply subset_eq.
Qed.

Lemma normalize_napp_0:
  forall (s: nstring),
    normalize (napp (nat_to_nstring 0) s) =
    normalize s.
Proof.
  intros s; rewrite nat_to_nstring_0.
  rewrite <- nstring_cons_napp.
  unfold normalize; apply subset_eq_compat.
  now induction s using nstring_ind; auto.
Qed.

Lemma nstring_to_nat_nchar:
  forall c,
    nstring_to_nat (nstring_nchar c) = nchar_to_decimal c.
Proof.
  now induction c using nchar_ind; auto.
Qed.

Lemma nstring_to_nat_aux_decomp_nchar':
  forall (m : nat) (c : nchar),
    nstring_to_nat_aux m (nstring_nchar c) = nchar_to_decimal c + 10 * m.
Proof.
  intros m c.
  rewrite nstring_to_nat_aux_decomp_nchar.
  fold (nstring_to_nat (nstring_nchar c)).
  now rewrite nstring_to_nat_nchar.
Qed.

Lemma nstring_to_nat_to_nstring_aux:
  forall m s,
    nat_to_nstring (nstring_to_nat_aux m s) =
    normalize (napp (nat_to_nstring m) s).
Proof.
  intros m s; revert m; induction s using nstring_ind; intros.
  - rewrite nstring_to_nat_aux_decomp_nchar'.
    destruct (le_lt_or_eq 0 m (le_0_n m)) as [Hltm | Heqm].
    + rewrite nat_to_nstring_decomp; auto.
      now rewrite normalize_app, nchar_to_decimal_to_nchar.
    + subst; rewrite plus_0_r.
      rewrite normalize_napp_0.
      rewrite nat_to_nstring_decomp_rem, nchar_to_decimal_to_nchar.
      now rewrite normalize_nchar.
  - rewrite nstring_cons_napp.
    rewrite nstring_to_nat_aux_app.
    rewrite IHs.
    rewrite nstring_to_nat_aux_decomp_nchar'.
    destruct (le_lt_or_eq 0 m (le_0_n m)) as [Hltm | Heqm].
    + rewrite (nat_to_nstring_decomp _ Hltm).
      now rewrite nchar_to_decimal_to_nchar, napp_assoc.
    + subst m; rewrite plus_0_r.
      rewrite normalize_napp_0.
      now rewrite nat_to_nstring_decomp_rem, nchar_to_decimal_to_nchar.
Qed.

Theorem nstring_to_nat_to_nstring:
  forall (s: nstring),
    nat_to_nstring (nstring_to_nat s) = normalize s.
Proof.
  unfold nstring_to_nat.
  intros s; rewrite nstring_to_nat_to_nstring_aux.
  now apply normalize_napp_0.
Qed.

Lemma normalize_aux_idempotent:
  forall s,
    normalize_aux (normalize_aux s) = normalize_aux s.
Proof.
  induction s as [| c s IHs]; auto.
  destruct (ascii_dec c "0").
  - subst c; simpl.
    destruct s; auto.
  - simpl.
    now destruct c as [[|] [|] [|] [|] [|] [|] [|] [|]]; simpl.
Qed.

Lemma normalize_idempotent:
  forall (s: nstring),
    normalize (normalize s) = normalize s.
Proof.
  now intros; apply subset_eq_compat, normalize_aux_idempotent.
Qed.

Definition normalized (s: nstring) := normalize s = s.

Definition nnstring := (sig normalized).

Lemma nstring_to_nat_to_nstring':
  forall (s: nnstring),
    nat_to_nstring (nstring_to_nat s.!) = s.!.
Proof.
  intros [s Hn]; simpl.
  rewrite <- Hn, nstring_to_nat_to_nstring.
  now apply normalize_idempotent.
Qed.


(*  *)
Definition numeral_dec (c: ascii): { numeral c } + { ~ numeral c }.
Proof.
  destruct (ascii_dec c "0") as [Heq | Hneq0];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "1") as [Heq | Hneq1];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "2") as [Heq | Hneq2];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "3") as [Heq | Hneq3];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "4") as [Heq | Hneq4];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "5") as [Heq | Hneq5];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "6") as [Heq | Hneq6];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "7") as [Heq | Hneq7];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "8") as [Heq | Hneq8];
    [now subst; left; unfold numeral; simpl; tauto |].
  destruct (ascii_dec c "9") as [Heq | Hneq9];
    [now subst; left; unfold numeral; simpl; tauto |].
  right; intros Hc.
  repeat destruct Hc as [Heq | Hc]; subst;  contradiction.
Defined.

Definition numerals_dec (s: string): { numerals s } + { ~ numerals s }.
Proof.
  induction s as [| c s IHs];
    [now right; intros Hs; inversion Hs |].
  destruct (numeral_dec c) as [Hc | Hnc], IHs as [Hs | Hns].
  - now left; apply numerals_String.
  - destruct s; [now left; apply numerals_numeral | right].
    intros H; inversion H; subst; contradiction.
  - right; intros H; inversion H; subst; contradiction.
  - right; intros H; inversion H; subst; contradiction.
Defined.

Definition string_to_nat (s: string): option nat :=
  match numerals_dec s with
  | left H => Some (nstring_to_nat (make_nstring H))
  | right _ => None
  end.

Definition nat_to_string (n: nat): string :=
  (nat_to_nstring n).!.

Eval compute in string_to_nat "000329".
Eval compute in nat_to_string 329.

Lemma numerals_dec_nstring:
  forall (s: nstring), numerals_dec s = left s.p.
Proof.
  induction s using nstring_ind.
  - now induction c using nchar_ind; simpl;
      apply f_equal, proof_irrelevance.
  - induction c using nchar_ind;
      simpl; simpl id_nstring_string in IHs; rewrite IHs;
        apply f_equal, proof_irrelevance.
Qed.

Theorem nat_to_string_to_nat:
  forall n, string_to_nat (nat_to_string n) = Some n.
Proof.
  intros n.
  unfold nat_to_string, string_to_nat.
  rewrite numerals_dec_nstring.
  replace (make_nstring (nat_to_nstring n).p) with (nat_to_nstring n); [| destruct (nat_to_nstring n); auto].
  now rewrite nat_to_nstring_to_nat.
Qed.

Definition onlySome (X: Type)(P: X -> Prop): option X -> Prop :=
  fun m => match m with Some x => P x | _ => True end.
Arguments onlySome X P m /.

Notation "'let_Some' x := m 'in' P" := (onlySome (fun x => P) m) (at level 90, P at next level, no associativity).

Theorem string_to_nat_to_string:
  forall s,
    let_Some n := string_to_nat s in
      nat_to_string n = normalize_aux s.
Proof.
  intros s; unfold nat_to_string, string_to_nat.
  destruct (numerals_dec s) as [Hs | Hns]; simpl; auto.
  rewrite nstring_to_nat_to_nstring.
  now unfold normalize; simpl.
Qed.