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 ->
Nbit a k =
false.
Lemma Nplength_one :
forall (
a:N) (
n:nat),
Nplength a =
ni n ->
Nbit a n =
true.
Lemma Nplength_first_one :
forall (
a:N) (
n:nat),
(
forall k:nat,
k <
n ->
Nbit a k =
false) ->
Nbit 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 ->
Nbit a k =
false) ->
ni_le (
ni n) (
Nplength a).
Lemma Nplength_ub :
forall (
a:N) (
n:nat),
Nbit 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).