Library Coq.NArith.Ndist
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 :
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).