Library Coq.NArith.Ndist
Require Import Arith.
Require Import Min.
Require Import BinPos.
Require Import BinNat.
Require Import Ndigits.
Require Import Min.
Require Import BinPos.
Require Import BinNat.
Require Import Ndigits.
An ultrametric distance over N numbers
Inductive natinf : Set :=
| infty : natinf
| ni : nat -> natinf.
Fixpoint Pplength (p:positive) : nat :=
match p with
| xH => 0
| xI _ => 0
| xO p' => S (Pplength p')
end.
Definition Nplength (a:N) :=
match a with
| N0 => infty
| Npos p => ni (Pplength p)
end.
Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.
Lemma Nplength_zeros :
forall (a:N) (n:nat),
Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false.
Lemma Nplength_one :
forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true.
Lemma Nplength_first_one :
forall (a:N) (n:nat),
(forall k:nat, k < n -> N.testbit_nat a k = false) ->
N.testbit_nat a n = true -> Nplength a = ni n.
Definition ni_min (d d':natinf) :=
match d with
| infty => d'
| ni n => match d' with
| infty => d
| ni n' => ni (min n n')
end
end.
Lemma ni_min_idemp : forall d:natinf, ni_min d d = d.
Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d.
Lemma ni_min_assoc :
forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'').
Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0.
Lemma ni_min_O_r : forall d:natinf, ni_min d (ni 0) = ni 0.
Lemma ni_min_inf_l : forall d:natinf, ni_min infty d = d.
Lemma ni_min_inf_r : forall d:natinf, ni_min d infty = d.
Definition ni_le (d d':natinf) := ni_min d d' = d.
Lemma ni_le_refl : forall d:natinf, ni_le d d.
Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'.
Lemma ni_le_trans :
forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''.
Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d.
Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'.
Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'.
Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d.
Lemma ni_le_min_induc :
forall d d' dm:natinf,
ni_le dm d ->
ni_le dm d' ->
(forall d'':natinf, ni_le d'' d -> ni_le d'' d' -> ni_le d'' dm) ->
ni_min d d' = dm.
Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n).
Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n.
Lemma Nplength_lb :
forall (a:N) (n:nat),
(forall k:nat, k < n -> N.testbit_nat a k = false) -> ni_le (ni n) (Nplength a).
Lemma Nplength_ub :
forall (a:N) (n:nat), N.testbit_nat a n = true -> ni_le (Nplength a) (ni n).
We define an ultrametric distance between N numbers:
,
where is the number of identical bits at the beginning
of and (infinity if ).
Instead of working with , we work with , namely
Npdist:
d is a distance, so iff ; this means that
iff :
Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.
Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.
is a distance, so :
is an ultrametric distance, that is, not only ,
but in fact .
This means that (lemma Npdist_ultra below).
This follows from the fact that
is an ultrametric norm, i.e. that ,
or equivalently that , i.e. that
min
(lemma Nplength_ultra).
Lemma Nplength_ultra_1 :
forall a a':N,
ni_le (Nplength a) (Nplength a') ->
ni_le (Nplength a) (Nplength (N.lxor a a')).
Lemma Nplength_ultra :
forall a a':N,
ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')).
Lemma Npdist_ultra :
forall a a' a'':N,
ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').