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