Require ImportRequire Import
  HoTT.Classes.orders.naturals
  HoTT.Classes.implementations.peano_naturals.
Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.naturals.


Generalizable Variables N.

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

(* NatDistance instances are all equivalent, because their behavior is fully
 determined by the specification. *)
Lemma nat_distance_unique {a b : NatDistance N}
  : forall x y, @nat_distance _ _ a x y = @nat_distance _ _ b x y.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
forall x y : N, nat_distance x y = nat_distance x y
Proof.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
forall x y : N, nat_distance x y = nat_distance x y
intros.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y: N
nat_distance x y = nat_distance x y unfold nat_distance.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y: N
match nat_distance_sig x y with
| inl s => s.1
| inr s => s.1
end = match nat_distance_sig x y with
      | inl s => s.1
      | inr s => s.1
      end
destruct (@nat_distance_sig _ _ a x y) as [[z1 E1]|[z1 E1]],
(@nat_distance_sig _ _ b x y) as [[z2 E2]|[z2 E2]];simpl.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: x + z1 = y
z2: N
E2: x + z2 = y
z1 = z2
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: x + z1 = y
z2: N
E2: y + z2 = x
z1 = z2
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: y + z1 = x
z2: N
E2: x + z2 = y
z1 = z2
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: y + z1 = x
z2: N
E2: y + z2 = x
z1 = z2
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: x + z1 = y
z2: N
E2: x + z2 = y
z1 = z2 apply (left_cancellation plus x).
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: x + z1 = y
z2: N
E2: x + z2 = y
x + z1 = x + z2 path_via y.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: x + z1 = y
z2: N
E2: y + z2 = x
z1 = z2 rewrite <-(rings.plus_0_r y),<-E2,<-rings.plus_assoc in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: y + (z2 + z1) = y + 0
E2: y + z2 = x
z1 = z2
  apply (left_cancellation plus y) in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: z2 + z1 = 0
E2: y + z2 = x
z1 = z2 apply naturals.zero_sum in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: (z2 = 0) * (z1 = 0)
E2: y + z2 = x
z1 = z2
  destruct E1;path_via 0.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: y + z1 = x
z2: N
E2: x + z2 = y
z1 = z2 rewrite <-(rings.plus_0_r x),<-E2,<-rings.plus_assoc in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: x + (z2 + z1) = x + 0
E2: x + z2 = y
z1 = z2
  apply (left_cancellation plus x) in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: z2 + z1 = 0
E2: x + z2 = y
z1 = z2 apply naturals.zero_sum in E1.
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1, z2: N
E1: (z2 = 0) * (z1 = 0)
E2: x + z2 = y
z1 = z2
  destruct E1;path_via 0.
-
H: Funext
H0: Univalence
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H1: Naturals N
a, b: NatDistance N
x, y, z1: N
E1: y + z1 = x
z2: N
E2: y + z2 = x
z1 = z2 apply (left_cancellation plus y);path_via x.
Qed.

End contents.

(* An existing instance of [CutMinus]
   allows to create an instance of [NatDistance] *)
Instance natdistance_cut_minus `{Naturals N} `{!TrivialApart N}
   {cm} `{!CutMinusSpec N cm} `{forall x y, Decidable (x ≤ y)} : NatDistance N.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x y : N, Decidable (x ≤ y)
NatDistance N
Proof.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x y : N, Decidable (x ≤ y)
NatDistance N
red.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x y : N, Decidable (x ≤ y)
forall x y : N, {z : N & x + z = y} + {z : N & y + z = x} intros.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
{z : N & x + z = y} + {z : N & y + z = x} destruct (decide_rel (<=) x y) as [E|E].
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: x ≤ y
{z : N & x + z = y} + {z : N & y + z = x}
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: ~ (x ≤ y)
{z : N & x + z = y} + {z : N & y + z = x}
-
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: x ≤ y
{z : N & x + z = y} + {z : N & y + z = x} left.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: x ≤ y
{z : N & x + z = y} exists (y ∸ x).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: x ≤ y
x + (y ∸ x) = y
  rewrite rings.plus_comm;apply cut_minus_le;trivial.
-
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: ~ (x ≤ y)
{z : N & x + z = y} + {z : N & y + z = x} right.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: ~ (x ≤ y)
{z : N & y + z = x} exists (x ∸ y).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
TrivialApart0: TrivialApart N
cm: CutMinus N
CutMinusSpec0: CutMinusSpec N cm
H0: forall x0 y0 : N, Decidable (x0 ≤ y0)
x, y: N
E: ~ (x ≤ y)
y + (x ∸ y) = x
  rewrite rings.plus_comm;apply cut_minus_le, orders.le_flip;trivial.
Defined.

(* Using the preceding instance we can make an instance
   for arbitrary models of the naturals
   by translation into [nat] on which we already have a [CutMinus] instance. *)
Instance natdistance_default `{Naturals N} : NatDistance N | 10.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
NatDistance N
Proof.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
NatDistance N
intros x y.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
{z : N & x + z = y} + {z : N & y + z = x}
destruct (nat_distance_sig (naturals_to_semiring N nat x)
  (naturals_to_semiring N nat y)) as [[n E]|[n E]].
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
{z : N & x + z = y} + {z : N & y + z = x}
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
{z : N & x + z = y} + {z : N & y + z = x}
-
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
{z : N & x + z = y} + {z : N & y + z = x} left.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
{z : N & x + z = y} exists (naturals_to_semiring nat N n).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
x + naturals_to_semiring nat N n = y
  rewrite <-(naturals.to_semiring_involutive N nat y), <-E.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
x + naturals_to_semiring nat N n =
naturals_to_semiring nat N (naturals_to_semiring N nat x + n)
  rewrite (rings.preserves_plus (A:=nat)), (naturals.to_semiring_involutive _ _).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat x + n = naturals_to_semiring N nat y
x + naturals_to_semiring nat N n = x + naturals_to_semiring nat N n
  split.
-
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
{z : N & x + z = y} + {z : N & y + z = x} right.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
{z : N & y + z = x} exists (naturals_to_semiring nat N n).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
y + naturals_to_semiring nat N n = x
  rewrite <-(naturals.to_semiring_involutive N nat x), <-E.
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
y + naturals_to_semiring nat N n =
naturals_to_semiring nat N (naturals_to_semiring N nat y + n)
  rewrite (rings.preserves_plus (A:=nat)), (naturals.to_semiring_involutive _ _).
N: Type
Aap: Apart N
Aplus: Plus N
Amult: Mult N
Azero: Zero N
Aone: One N
Ale: Le N
Alt: Lt N
U: NaturalsToSemiRing N
H: Naturals N
x, y: N
n: nat
E: naturals_to_semiring N nat y + n = naturals_to_semiring N nat x
y + naturals_to_semiring nat N n = y + naturals_to_semiring nat N n
  split.
Defined.