Library Coq.NArith.Ndist

Require Import Arith.
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:

Definition Npdist (a a´:N) := Nplength (N.lxor a a´).

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 :

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).

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´).