to_decimal

Require Import PeanoNat Lia List Wf_nat.
Import ListNotations.

Fixpoint to_decimal_helper (n : nat) (dummy : nat) :=
  match dummy with
    | 0 => []
    | S dummy' => if n =? 0
                  then []
                  else (to_decimal_helper (n / 10) dummy') ++ [ n mod 10 ]
  end.

Definition to_decimal (n: nat) :=
  if n =? 0 then [0] else to_decimal_helper n n.

Lemma to_decimal_helper_0:
  forall m, to_decimal_helper 0 m = [].
Proof.
  destruct m; trivial.
Qed.

Lemma to_decimal_helper_step:
  forall n m, n <> 0 -> m <> 0 -> to_decimal_helper n m = (to_decimal_helper (n / 10) (pred m)) ++ [ n mod 10 ].
Proof.
  destruct n, m; easy.
Qed.

Lemma arithmetic_helper:
 forall n, n >= S n / 10.
Proof.
  destruct n; unfold ge.
    easy.
  eapply Nat.le_trans.
  apply (Nat.div_le_mono _ ((S n)* 10)).
    1,2: lia.
  rewrite Nat.div_mul.
  all: lia.
Qed.

Lemma to_decimal_helper_large_stoping_limit:
  forall m n, m >= n -> to_decimal_helper n m = to_decimal_helper n n.
Proof.
  intros m n; revert m.
  induction n using (well_founded_induction lt_wf).
  rename H into IH.
  destruct n.
  { (* case n = 0 *)
    intros; rewrite !to_decimal_helper_0; reflexivity.
  }
  { intros m MN.
    rewrite (to_decimal_helper_step _ m).
      2,3: lia.
    rewrite (to_decimal_helper_step _ (S n)).
      2,3: lia.
    rewrite Nat.pred_succ.
    rewrite IH.
    erewrite (IH (S n / 10) _ n).
    reflexivity.
    all: clear IH.
    * apply arithmetic_helper.
    * apply Nat.lt_succ_r, arithmetic_helper.
    * unfold ge in *.
      eapply Nat.le_trans.
      apply arithmetic_helper.
      destruct m.
        lia.
      simpl.
      apply le_S_n.
      assumption.
   }
  Unshelve.
  apply Nat.lt_succ_r, arithmetic_helper.
Qed.

Lemma beq_0:
  forall n, n <> 0 -> (n =? 0) = false.
Proof.
  intro.
  rewrite Nat.eqb_neq.
  easy.
Qed.

Theorem to_decimal_recurrence:
  forall n, (n < 10 /\ to_decimal n = [n]) \/
            (n >= 10 /\ to_decimal n =  to_decimal (n / 10) ++ [ n mod 10 ]).
Proof.
  intros.
  destruct (Nat.lt_ge_cases n 10).
  { left; split; [assumption | ].
    destruct n; [trivial | ].
    unfold to_decimal.
    rewrite beq_0.
      2: lia.
    rewrite to_decimal_helper_step.
      2,3: lia.
    rewrite Nat.div_small.
      2: assumption.
    rewrite to_decimal_helper_0.
    rewrite Nat.mod_small.
      2: assumption.
    easy.
  }
  { right; split; [assumption | ].
    unfold to_decimal.
    rewrite beq_0.
      2: lia.
    rewrite beq_0.
      2:{ apply (Nat.div_le_mono _ _ 10) in H.
            2: lia.
          remember (n / 10) as n'.
          clear Heqn'.
          simpl in H; lia.
        }
    rewrite to_decimal_helper_step.
      2,3: lia.
    f_equal.
    apply to_decimal_helper_large_stoping_limit.
    destruct n.
      easy.
    rewrite Nat.pred_succ.
    apply arithmetic_helper.
  }
Qed.