theory.nat_distance

Require
  orders.naturals peano_naturals.
Require Import
  Morphisms Ring
  abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations.

Section contents.
Context `{Naturals N}.
Add Ring N : (rings.stdlib_semiring_theory N).

Program Lemma nat_distance_unique_respectful {a b: NatDistance N} : ((=) ==> (=) ==> (=))%signature a b.

Lemma nat_distance_unique {a b: NatDistance N} {x y : N} : a x y = b x y.

Context `{!NatDistance N}.

Global Instance nat_distance_proper : Proper ((=) ==> (=) ==> (=)) nat_distance.
End contents.

Program Instance natdistancecut_minus `{Naturals N} `{Apart N} `{!TrivialApart N} `{!FullPseudoSemiRingOrder Nle Nlt}
       `{!CutMinusSpec N cm} `{ x y, Decision (x y)} : NatDistance N
  := λ x y, if decide_rel (≤) x y then y x else x y.

Global Program Instance natdistance_default `{Naturals N} : NatDistance N | 10 := λ x y: N,
  naturals_to_semiring nat N (nat_distance (naturals_to_semiring N nat x) (naturals_to_semiring N nat y)).