Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

DecimalFacts : some facts about Decimal numbers

Require Import Decimal.

Lemma uint_dec (d d' : uint) : { d = d' } + { d <> d' }.d, d':uint
{d = d'} + {d <> d'}
Proof.d, d':uint
{d = d'} + {d <> d'}
 decide equality.
Defined.

Lemma rev_revapp d d' :
 rev (revapp d d') = revapp d' d.d, d':uint
rev (revapp d d') = revapp d' d
Proof.d, d':uint
rev (revapp d d') = revapp d' d
 revert d'.d:uint
forall d' : uint, rev (revapp d d') = revapp d' d induction d; simpl; intros; now rewrite ?IHd.
Qed.

Lemma rev_rev d : rev (rev d) = d.d:uint
rev (rev d) = d
Proof.d:uint
rev (rev d) = d
 apply rev_revapp.
Qed.

Normalization on little-endian numbers

Fixpoint nztail d :=
 match d with
 | Nil => Nil
 | D0 d => match nztail d with Nil => Nil | d' => D0 d' end
 | D1 d => D1 (nztail d)
 | D2 d => D2 (nztail d)
 | D3 d => D3 (nztail d)
 | D4 d => D4 (nztail d)
 | D5 d => D5 (nztail d)
 | D6 d => D6 (nztail d)
 | D7 d => D7 (nztail d)
 | D8 d => D8 (nztail d)
 | D9 d => D9 (nztail d)
 end.

Definition lnorm d :=
 match nztail d with
 | Nil => zero
 | d => d
 end.

Lemma nzhead_revapp_0 d d' : nztail d = Nil ->
 nzhead (revapp d d') = nzhead d'.d, d':uint
nztail d = Nil -> nzhead (revapp d d') = nzhead d'
Proof.d, d':uint
nztail d = Nil -> nzhead (revapp d d') = nzhead d'
 revert d'.d:uint
forall d' : uint,
nztail d = Nil -> nzhead (revapp d d') = nzhead d' induction d; intros d' [=]; simpl; trivial.d:uint
IHd:forall d'0 : uint, nztail d = Nil -> nzhead (revapp d d'0) = nzhead d'0
d':uint
H0:match nztail d with
| Nil => Nil
| D0 u => D0 (D0 u)
| D1 u => D0 (D1 u)
| D2 u => D0 (D2 u)
| D3 u => D0 (D3 u)
| D4 u => D0 (D4 u)
| D5 u => D0 (D5 u)
| D6 u => D0 (D6 u)
| D7 u => D0 (D7 u)
| D8 u => D0 (D8 u)
| D9 u => D0 (D9 u)
end = Nil
nzhead (revapp d (D0 d')) = nzhead d'
 destruct (nztail d); now rewrite IHd.
Qed.

Lemma nzhead_revapp d d' : nztail d <> Nil ->
 nzhead (revapp d d') = revapp (nztail d) d'.d, d':uint
nztail d <> Nil ->
nzhead (revapp d d') = revapp (nztail d) d'
Proof.d, d':uint
nztail d <> Nil ->
nzhead (revapp d d') = revapp (nztail d) d'
 revert d'.d:uint
forall d' : uint,
nztail d <> Nil ->
nzhead (revapp d d') = revapp (nztail d) d'
 induction d; intros d' H; simpl in *;
 try destruct (nztail d) eqn:E;
  (now rewrite ?nzhead_revapp_0) || (now rewrite IHd).
Qed.

Lemma nzhead_rev d : nztail d <> Nil ->
 nzhead (rev d) = rev (nztail d).d:uint
nztail d <> Nil -> nzhead (rev d) = rev (nztail d)
Proof.d:uint
nztail d <> Nil -> nzhead (rev d) = rev (nztail d)
 apply nzhead_revapp.
Qed.

Lemma rev_nztail_rev d :
  rev (nztail (rev d)) = nzhead d.d:uint
rev (nztail (rev d)) = nzhead d
Proof.d:uint
rev (nztail (rev d)) = nzhead d
 destruct (uint_dec (nztail (rev d)) Nil) as [H|H].d:uint
H:nztail (rev d) = Nil
rev (nztail (rev d)) = nzhead d
d:uint
H:nztail (rev d) <> Nil
rev (nztail (rev d)) = nzhead d
 -d:uint
H:nztail (rev d) = Nil
rev (nztail (rev d)) = nzhead d rewrite H.d:uint
H:nztail (rev d) = Nil
rev Nil = nzhead d unfold rev; simpl.d:uint
H:nztail (rev d) = Nil
Nil = nzhead d
   rewrite <- (rev_rev d).d:uint
H:nztail (rev d) = Nil
Nil = nzhead (rev (rev d)) symmetry.d:uint
H:nztail (rev d) = Nil
nzhead (rev (rev d)) = Nil
   now apply nzhead_revapp_0.
 -d:uint
H:nztail (rev d) <> Nil
rev (nztail (rev d)) = nzhead d now rewrite <- nzhead_rev, rev_rev.
Qed.

Lemma revapp_nil_inv d d' : revapp d d' = Nil -> d = Nil /\ d' = Nil.d, d':uint
revapp d d' = Nil -> d = Nil /\ d' = Nil
Proof.d, d':uint
revapp d d' = Nil -> d = Nil /\ d' = Nil
 revert d'.d:uint
forall d' : uint,
revapp d d' = Nil -> d = Nil /\ d' = Nil
 induction d; simpl; intros d' H; auto; now apply IHd in H.
Qed.

Lemma rev_nil_inv d : rev d = Nil -> d = Nil.d:uint
rev d = Nil -> d = Nil
Proof.d:uint
rev d = Nil -> d = Nil
 apply revapp_nil_inv.
Qed.

Lemma rev_lnorm_rev d :
  rev (lnorm (rev d)) = unorm d.d:uint
rev (lnorm (rev d)) = unorm d
Proof.d:uint
rev (lnorm (rev d)) = unorm d
 unfold unorm, lnorm.d:uint
rev
  match nztail (rev d) with
  | Nil => 0
  | D0 u => D0 u
  | D1 u => D1 u
  | D2 u => D2 u
  | D3 u => D3 u
  | D4 u => D4 u
  | D5 u => D5 u
  | D6 u => D6 u
  | D7 u => D7 u
  | D8 u => D8 u
  | D9 u => D9 u
  end =
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end
 rewrite <- rev_nztail_rev.d:uint
rev
  match nztail (rev d) with
  | Nil => 0
  | D0 u => D0 u
  | D1 u => D1 u
  | D2 u => D2 u
  | D3 u => D3 u
  | D4 u => D4 u
  | D5 u => D5 u
  | D6 u => D6 u
  | D7 u => D7 u
  | D8 u => D8 u
  | D9 u => D9 u
  end =
match rev (nztail (rev d)) with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end
 destruct nztail; simpl; trivial;
  destruct rev eqn:E; trivial; now apply rev_nil_inv in E.
Qed.

Lemma nzhead_nonzero d d' : nzhead d <> D0 d'.d, d':uint
nzhead d <> D0 d'
Proof.d, d':uint
nzhead d <> D0 d'
 induction d; easy.
Qed.

Lemma unorm_0 d : unorm d = zero <-> nzhead d = Nil.d:uint
unorm d = 0%uint <-> nzhead d = Nil
Proof.d:uint
unorm d = 0%uint <-> nzhead d = Nil
 unfold unorm.d:uint
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint <-> nzhead d = Nil split.d:uint
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint -> nzhead d = Nil
d:uint
nzhead d = Nil ->
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint
 -d:uint
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint -> nzhead d = Nil generalize (nzhead_nonzero d).d:uint
(forall d' : uint, nzhead d <> D0 d') ->
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint -> nzhead d = Nil
   destruct nzhead; intros H [=]; trivial.d, u:uint
H:forall d' : uint, D0 u <> D0 d'
H1:u = Nil
D0 u = Nil now destruct (H u).
 -d:uint
nzhead d = Nil ->
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end = 0%uint now intros ->.
Qed.

Lemma unorm_nonnil d : unorm d <> Nil.d:uint
unorm d <> Nil
Proof.d:uint
unorm d <> Nil
 unfold unorm.d:uint
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end <> Nil now destruct nzhead.
Qed.

Lemma nzhead_invol d : nzhead (nzhead d) = nzhead d.d:uint
nzhead (nzhead d) = nzhead d
Proof.d:uint
nzhead (nzhead d) = nzhead d
 now induction d.
Qed.

Lemma unorm_invol d : unorm (unorm d) = unorm d.d:uint
unorm (unorm d) = unorm d
Proof.d:uint
unorm (unorm d) = unorm d
 unfold unorm.d:uint
match
  nzhead
    match nzhead d with
    | Nil => 0
    | D0 u => D0 u
    | D1 u => D1 u
    | D2 u => D2 u
    | D3 u => D3 u
    | D4 u => D4 u
    | D5 u => D5 u
    | D6 u => D6 u
    | D7 u => D7 u
    | D8 u => D8 u
    | D9 u => D9 u
    end
with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end =
match nzhead d with
| Nil => 0%uint
| D0 u => D0 u
| D1 u => D1 u
| D2 u => D2 u
| D3 u => D3 u
| D4 u => D4 u
| D5 u => D5 u
| D6 u => D6 u
| D7 u => D7 u
| D8 u => D8 u
| D9 u => D9 u
end
 destruct (nzhead d) eqn:E; trivial.d, u:uint
E:nzhead d = D0 u
match nzhead (D0 u) with
| Nil => 0%uint
| D0 u0 => D0 u0
| D1 u0 => D1 u0
| D2 u0 => D2 u0
| D3 u0 => D3 u0
| D4 u0 => D4 u0
| D5 u0 => D5 u0
| D6 u0 => D6 u0
| D7 u0 => D7 u0
| D8 u0 => D8 u0
| D9 u0 => D9 u0
end = D0 u
 destruct (nzhead_nonzero _ _ E).
Qed.

Lemma norm_invol d : norm (norm d) = norm d.d:int
norm (norm d) = norm d
Proof.d:int
norm (norm d) = norm d
 unfold norm.d:int
match
  match d with
  | Pos d0 => Pos (unorm d0)
  | Neg d0 =>
      match nzhead d0 with
      | Nil => 0%int
      | D0 u => Neg (D0 u)
      | D1 u => Neg (D1 u)
      | D2 u => Neg (D2 u)
      | D3 u => Neg (D3 u)
      | D4 u => Neg (D4 u)
      | D5 u => Neg (D5 u)
      | D6 u => Neg (D6 u)
      | D7 u => Neg (D7 u)
      | D8 u => Neg (D8 u)
      | D9 u => Neg (D9 u)
      end
  end
with
| Pos d0 => Pos (unorm d0)
| Neg d0 =>
    match nzhead d0 with
    | Nil => 0%int
    | D0 u => Neg (D0 u)
    | D1 u => Neg (D1 u)
    | D2 u => Neg (D2 u)
    | D3 u => Neg (D3 u)
    | D4 u => Neg (D4 u)
    | D5 u => Neg (D5 u)
    | D6 u => Neg (D6 u)
    | D7 u => Neg (D7 u)
    | D8 u => Neg (D8 u)
    | D9 u => Neg (D9 u)
    end
end =
match d with
| Pos d0 => Pos (unorm d0)
| Neg d0 =>
    match nzhead d0 with
    | Nil => 0%int
    | D0 u => Neg (D0 u)
    | D1 u => Neg (D1 u)
    | D2 u => Neg (D2 u)
    | D3 u => Neg (D3 u)
    | D4 u => Neg (D4 u)
    | D5 u => Neg (D5 u)
    | D6 u => Neg (D6 u)
    | D7 u => Neg (D7 u)
    | D8 u => Neg (D8 u)
    | D9 u => Neg (D9 u)
    end
end
 destruct d.d:uint
Pos (unorm (unorm d)) = Pos (unorm d)
d:uint
match
  match nzhead d with
  | Nil => 0%int
  | D0 u => Neg (D0 u)
  | D1 u => Neg (D1 u)
  | D2 u => Neg (D2 u)
  | D3 u => Neg (D3 u)
  | D4 u => Neg (D4 u)
  | D5 u => Neg (D5 u)
  | D6 u => Neg (D6 u)
  | D7 u => Neg (D7 u)
  | D8 u => Neg (D8 u)
  | D9 u => Neg (D9 u)
  end
with
| Pos d0 => Pos (unorm d0)
| Neg d0 =>
    match nzhead d0 with
    | Nil => 0%int
    | D0 u => Neg (D0 u)
    | D1 u => Neg (D1 u)
    | D2 u => Neg (D2 u)
    | D3 u => Neg (D3 u)
    | D4 u => Neg (D4 u)
    | D5 u => Neg (D5 u)
    | D6 u => Neg (D6 u)
    | D7 u => Neg (D7 u)
    | D8 u => Neg (D8 u)
    | D9 u => Neg (D9 u)
    end
end =
match nzhead d with
| Nil => 0%int
| D0 u => Neg (D0 u)
| D1 u => Neg (D1 u)
| D2 u => Neg (D2 u)
| D3 u => Neg (D3 u)
| D4 u => Neg (D4 u)
| D5 u => Neg (D5 u)
| D6 u => Neg (D6 u)
| D7 u => Neg (D7 u)
| D8 u => Neg (D8 u)
| D9 u => Neg (D9 u)
end
 -d:uint
Pos (unorm (unorm d)) = Pos (unorm d) f_equal.d:uint
unorm (unorm d) = unorm d apply unorm_invol.
 -d:uint
match
  match nzhead d with
  | Nil => 0%int
  | D0 u => Neg (D0 u)
  | D1 u => Neg (D1 u)
  | D2 u => Neg (D2 u)
  | D3 u => Neg (D3 u)
  | D4 u => Neg (D4 u)
  | D5 u => Neg (D5 u)
  | D6 u => Neg (D6 u)
  | D7 u => Neg (D7 u)
  | D8 u => Neg (D8 u)
  | D9 u => Neg (D9 u)
  end
with
| Pos d0 => Pos (unorm d0)
| Neg d0 =>
    match nzhead d0 with
    | Nil => 0%int
    | D0 u => Neg (D0 u)
    | D1 u => Neg (D1 u)
    | D2 u => Neg (D2 u)
    | D3 u => Neg (D3 u)
    | D4 u => Neg (D4 u)
    | D5 u => Neg (D5 u)
    | D6 u => Neg (D6 u)
    | D7 u => Neg (D7 u)
    | D8 u => Neg (D8 u)
    | D9 u => Neg (D9 u)
    end
end =
match nzhead d with
| Nil => 0%int
| D0 u => Neg (D0 u)
| D1 u => Neg (D1 u)
| D2 u => Neg (D2 u)
| D3 u => Neg (D3 u)
| D4 u => Neg (D4 u)
| D5 u => Neg (D5 u)
| D6 u => Neg (D6 u)
| D7 u => Neg (D7 u)
| D8 u => Neg (D8 u)
| D9 u => Neg (D9 u)
end destruct (nzhead d) eqn:E; auto.d, u:uint
E:nzhead d = D0 u
match nzhead (D0 u) with
| Nil => 0%int
| D0 u0 => Neg (D0 u0)
| D1 u0 => Neg (D1 u0)
| D2 u0 => Neg (D2 u0)
| D3 u0 => Neg (D3 u0)
| D4 u0 => Neg (D4 u0)
| D5 u0 => Neg (D5 u0)
| D6 u0 => Neg (D6 u0)
| D7 u0 => Neg (D7 u0)
| D8 u0 => Neg (D8 u0)
| D9 u0 => Neg (D9 u0)
end = Neg (D0 u)
   destruct (nzhead_nonzero _ _ E).
Qed.