Library Coq.NArith.Ndist
An ultrametric distance over N numbers
Inductive natinf : Set :=
| infty : natinf
| ni : nat -> natinf.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Fixpoint Pplength (p:positive) : nat :=
match p with
| xH => 0
| xI _ => 0
| xO p' => S (Pplength p')
end.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Definition Nplength (a:N) :=
match a with
| N0 => infty
| Npos p => ni (Pplength p)
end.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Nplength_infty : forall a:N, Nplength a = infty -> a = N0.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Nplength_zeros :
forall (a:N) (n:nat),
Nplength a = ni n -> forall k:nat, k < n -> N.testbit_nat a k = false.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Nplength_one :
forall (a:N) (n:nat), Nplength a = ni n -> N.testbit_nat a n = true.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
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.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
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.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_idemp : forall d:natinf, ni_min d d = d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_comm : forall d d':natinf, ni_min d d' = ni_min d' d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_assoc :
forall d d' d'':natinf, ni_min (ni_min d d') d'' = ni_min d (ni_min d' d'').
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_O_l : forall d:natinf, ni_min (ni 0) d = ni 0.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_O_r : forall d:natinf, ni_min d (ni 0) = ni 0.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_inf_l : forall d:natinf, ni_min infty d = d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_inf_r : forall d:natinf, ni_min d infty = d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Definition ni_le (d d':natinf) := ni_min d d' = d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_refl : forall d:natinf, ni_le d d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_antisym : forall d d':natinf, ni_le d d' -> ni_le d' d -> d = d'.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_trans :
forall d d' d'':natinf, ni_le d d' -> ni_le d' d'' -> ni_le d d''.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_min_1 : forall d d':natinf, ni_le (ni_min d d') d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_min_2 : forall d d':natinf, ni_le (ni_min d d') d'.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_min_case : forall d d':natinf, ni_min d d' = d \/ ni_min d d' = d'.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_total : forall d d':natinf, ni_le d d' \/ ni_le d' d.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
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.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma le_ni_le : forall m n:nat, m <= n -> ni_le (ni m) (ni n).
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma ni_le_le : forall m n:nat, ni_le (ni m) (ni n) -> m <= n.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
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).
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
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:
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Definition Npdist (a a':N) := Nplength (N.lxor a a').
d is a distance, so iff ; this means that
iff :
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Npdist_eq_1 : forall a:N, Npdist a a = infty.
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Npdist_eq_2 : forall a a':N, Npdist a a' = infty -> a = a'.
is a distance, so :
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Npdist_comm : forall a a':N, Npdist a a' = Npdist a' a.
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).
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Nplength_ultra_1 :
forall a a':N,
ni_le (Nplength a) (Nplength a') ->
ni_le (Nplength a) (Nplength (N.lxor a a')).
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Nplength_ultra :
forall a a':N,
ni_le (ni_min (Nplength a) (Nplength a')) (Nplength (N.lxor a a')).
#[deprecated(since="8.19", note="Please step up to maintain Ndist.v if you need it.")]
Lemma Npdist_ultra :
forall a a' a'':N,
ni_le (ni_min (Npdist a a'') (Npdist a'' a')) (Npdist a a').