From HoTT.Basics Require Import Overture Numeral Tactics Decidable.From HoTT.Basics Require Import Overture Numeral Tactics Decidable.
From HoTT.Basics Require Import Equivalences PathGroupoids Trunc Iff.
Require Import Types.Paths Types.Universe.
Require Import Spaces.Nat.Core Spaces.SInt.
(** Users of this file likely want the instances in Equiv.BiInv, such as [isequiv_isbiinv], so we export this file. *)
Require Export Equiv.BiInv.

(** * The integers, defined as a HIT *)

(** Following "The integers as a higher inductive type" by Altenkirch and Scoccola, we define the integers as a higher inductive type.  Morally it is the free pointed type with a biinvertible self-map.  This representation leads to more convenient induction and recursion principles that avoid needing to split into many cases as happens with the signed integers [SInt].  Moreover, many results hold definitionally instead of requiring lengthy proofs.  Examples include results about addition, multiplication, iteration of equivalences and exponentiation of loops such as [int_add_succ_l], [int_mul_pred_l], [int_iter_succ_l], and [loopexp_pred_r] to name just a few.  We also have a convenient lemma [int_homotopic] for proving that two functions [Int -> P] are homotopic.  Part of what makes it easy to use is that the functions being compared often compute definitionally on [zero] and [int_succ].

One difference compared to the Altenkirch-Scoccola paper is that we prove additional induction principles, [int_ind_biinv] and [int_ind_equiv].  The key to these is a carefully chosen proof of [int_succ_pred] that satisfies the half-adjoint law.  Then, using [int_ind_equiv], we are able to trivially prove [int_homotopic] (their Theorem 2.4) without using univalence or needing to introduce "prBiInv" (squares preserving bi-invertible maps).  As a result, we don't need univalence for any fundamental results about the integers.

One thing to be aware of is that the representation of integers is no longer definitionally unique. For example, [2 - 3] is not definitionally equal to [-1].  [int_reduce] or [ltac:(decide)] can be used to show that these are equal, with [int_reduce] being faster, as illustrated in test/Spaces/Int.v. *)

Set Universe Minimization ToSet.

Declare Scope int_scope.
Delimit Scope int_scope with int.
Local Open Scope int_scope.

(** ** The definition of [Int] *)

Module Export Int.
  Section Int.

    (** Here we are modeling the HIT which has a point [zero] and a successor map [int_succ] which is a biinvertible equivalence.  [int_pred] and [int_pred2] are its left and right inverses. *)

    Private Inductive Int : Type0 :=
    | zero : Int
    | int_succ : Int -> Int
    | int_pred : Int -> Int
    | int_pred2 : Int -> Int.

    Axiom int_pred_succ : int_pred o int_succ == idmap.

    Axiom int_succ_pred2 : int_succ o int_pred2 == idmap.

    Context {P : Int -> Type} (t0 : P zero) (e : forall z : Int, P z -> P (int_succ z))
      (r : forall z : Int, P z -> P (int_pred z)) (s : forall z : Int, P z -> P (int_pred2 z))
      (re : forall (z : Int) (t : P z), int_pred_succ z # (r (int_succ z) (e z t)) = t)
      (es : forall (z : Int) (t : P z), int_succ_pred2 z # (e (int_pred2 z) (s z t)) = t).

    Fixpoint int_ind (z : Int) : P z
      := match z with
      | zero => fun _ _ => t0
      | int_succ z => fun _ _ => e z (int_ind z)
      | int_pred z => fun _ _ => r z (int_ind z)
      | int_pred2 z => fun _ _ => s z (int_ind z)
      end re es.
      (** We make sure that this depends on [re] and [es] as well. *)

    (** The beta principles for [int_ind] on [int_pred_succ] and [int_succ_pred2]. *)
    Axiom int_ind_beta_int_pred_succ
      : forall (z : Int), apD int_ind (int_pred_succ z) = re z (int_ind z).

    Axiom int_ind_beta_int_succ_pred2
      : forall (z : Int), apD int_ind (int_succ_pred2 z) = es z (int_ind z).

  End Int.
End Int.

(** We sometimes want to treat the integers as a pointed type with basepoint given by 0. *)
Instance ispointed_int : IsPointed Int := zero.

(** Successor is biinvertible.  It follows from typeclass inference that it is an equivalence. *)
Instance isbiinv_int_succ : IsBiInv int_succ
  := Build_IsBiInv _ _ _ int_pred2 int_pred int_succ_pred2 int_pred_succ.

Definition biinv_int_succ : BiInv Int Int
  := Build_BiInv _ _ int_succ _.

(** The predecessor is an equivalence on [Int]. *)
Instance isequiv_int_pred : IsEquiv int_pred
  := isequiv_retr_biinv int_succ.

Notation "z .+1" := (int_succ z) : int_scope.
Notation "z .-1" := (int_pred z) : int_scope.

(** [int_pred] is a section of [int_succ]. *)
Definition int_succ_pred : int_succ o int_pred == idmap
  := retr_is_sect_isbiinv int_succ.

(** [int_pred2] is a retraction of [int_succ]. *)
Definition int_pred2_succ : int_pred2 o int_succ == idmap
  := sect_is_retr_isbiinv int_succ.

(** Our proof of [retr_is_sect_isbiinv] was carefully chosen so that the data showing that [int_succ] and [int_pred] form an equivalence satisfies the adjoint law. *)
Definition int_succ_isadj (z : Int)
  : int_succ_pred (int_succ z) = ap int_succ (int_pred_succ z)
  := eisadj int_succ z.

(** ** Induction and recursion principles for Int *)

Definition int_ind_biinv {P : Int -> Type} (t0 : P zero)
  (e : forall z : Int, P z -> P z.+1) {iseq : forall z, IsBiInv (e z)}
  : forall z, P z.
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z
Proof.
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z
  snapply (int_ind t0 e).
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z -> P z.-1
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z -> P (int_pred2 z)
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall (z : Int) (t : P z),
transport P (int_pred_succ z) (?r z.+1 (e z t)) = t
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall (z : Int) (t : P z),
transport P (int_succ_pred2 z) (e (int_pred2 z) (?s z t)) = t
  -
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z -> P z.-1 intro z.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
P z -> P z.-1
    exact ((retr_biinv (e z.-1)) o transport P (int_succ_pred z)^).
  -
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall z : Int, P z -> P (int_pred2 z) intro z.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
P z -> P (int_pred2 z)
    exact ((e (int_pred2 z))^-1 o transport P (int_succ_pred2 z)^).
  -
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall (z : Int) (t : P z),
transport P (int_pred_succ z)
  ((fun z0 : Int => retr_biinv (e z0.-1) o transport P (int_succ_pred z0)^)
     z.+1 (e z t)) =
t intros z p; cbn beta.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport P (int_pred_succ z)
  (retr_biinv (e z.+1.-1) (transport P (int_succ_pred z.+1)^ (e z p))) =
p
    lhs_V napply (ap_transport _ (fun z => retr_biinv (e z))).
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
retr_biinv (e z)
  (transport (fun z0 : Int => P z0.+1) (int_pred_succ z)
     (transport P (int_succ_pred z.+1)^ (e z p))) =
p
    lhs napply (ap (retr_biinv (e z))).
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport (fun z0 : Int => P z0.+1) (int_pred_succ z)
  (transport P (int_succ_pred z.+1)^ (e z p)) =
?Goal
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
retr_biinv (e z) ?Goal = p
    {
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport (fun z0 : Int => P z0.+1) (int_pred_succ z)
  (transport P (int_succ_pred z.+1)^ (e z p)) =
?Goal lhs napply transport_compose.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport P (ap int_succ (int_pred_succ z))
  (transport P (int_succ_pred z.+1)^ (e z p)) =
?Goal
      lhs_V napply transport_pp.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport P ((int_succ_pred z.+1)^ @ ap int_succ (int_pred_succ z)) (e z p) =
?Goal
      apply transport2.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
(int_succ_pred z.+1)^ @ ap int_succ (int_pred_succ z) = ?q
      lhs napply (ap inverse (int_succ_isadj z) @@ 1).
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
(ap int_succ (int_pred_succ z))^ @ ap int_succ (int_pred_succ z) = ?q
      apply concat_Vp. }
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
retr_biinv (e z) (transport P 1 (e z p)) = p
    cbn.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
retr_biinv (e z) (e z p) = p apply eissect_biinv.
  -
P: Int -> Type
t0: P zero
e: forall z : Int, P z -> P z.+1
iseq: forall z : Int, IsBiInv (e z)
forall (z : Int) (t : P z),
transport P (int_succ_pred2 z)
  (e (int_pred2 z)
     ((fun z0 : Int =>
       (e (int_pred2 z0))^-1 o transport P (int_succ_pred2 z0)^) z t)) =
t intros z p; cbn beta.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport P (int_succ_pred2 z)
  (e (int_pred2 z) ((e (int_pred2 z))^-1 (transport P (int_succ_pred2 z)^ p))) =
p
    rewrite eisretr.
P: Int -> Type
t0: P zero
e: forall z0 : Int, P z0 -> P z0.+1
iseq: forall z0 : Int, IsBiInv (e z0)
z: Int
p: P z
transport P (int_succ_pred2 z) (transport P (int_succ_pred2 z)^ p) = p
    apply transport_pV.
Defined.

Definition int_ind_equiv {P : Int -> Type} (t0 : P zero)
  (e : forall z : Int, P z -> P z.+1) {iseq : forall z, IsEquiv (e z)}
  : forall z, P z
  := @int_ind_biinv P t0 e (fun z => isbiinv_isequiv _ (iseq z)).

Section RecursionPrinciple.

  Context {P : Type} (t0 : P) (f : P -> P) (g1 g2 : P -> P)
    (s : g1 o f == idmap) (r : f o g2 == idmap).

  (** The recursion principle. *)
  Definition int_rec : Int -> P.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
Int -> P
  Proof.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
Int -> P
    snapply (int_ind t0 (fun _ => f) (fun _ => g1) (fun _ => g2)).
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall (z : Int) (t : (fun _ : Int => P) z),
transport (fun _ : Int => P) (int_pred_succ z)
  ((fun _ : Int => g1) z.+1 ((fun _ : Int => f) z t)) =
t
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall (z : Int) (t : (fun _ : Int => P) z),
transport (fun _ : Int => P) (int_succ_pred2 z)
  ((fun _ : Int => f) (int_pred2 z) ((fun _ : Int => g2) z t)) =
t
    all: intros z t; cbn.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
transport (fun _ : Int => P) (int_pred_succ z) (g1 (f t)) = t
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
transport (fun _ : Int => P) (int_succ_pred2 z) (f (g2 t)) = t
    all: lhs napply transport_const.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
g1 (f t) = t
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
f (g2 t) = t
    -
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
g1 (f t) = t apply s.
    -
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
t: (fun _ : Int => P) z
f (g2 t) = t apply r.
  Defined.

  Definition int_rec_beta_int_pred_succ
    : forall z, ap int_rec (int_pred_succ z) = s (int_rec z).
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall z : Int, ap int_rec (int_pred_succ z) = s (int_rec z)
  Proof.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall z : Int, ap int_rec (int_pred_succ z) = s (int_rec z)
    intro z.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
ap int_rec (int_pred_succ z) = s (int_rec z)
    napply (cancelL (transport_const (int_pred_succ z) _)).
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
transport_const (int_pred_succ z) (int_rec z.+1.-1) @
ap int_rec (int_pred_succ z) =
transport_const (int_pred_succ z) (int_rec z.+1.-1) @ s (int_rec z)
    lhs_V napply apD_const.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
apD int_rec (int_pred_succ z) =
transport_const (int_pred_succ z) (int_rec z.+1.-1) @ s (int_rec z)
    napply int_ind_beta_int_pred_succ.
  Defined.

  Definition int_rec_beta_int_succ_pred2
    : forall z, ap int_rec (int_succ_pred2 z) = r (int_rec z).
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall z : Int, ap int_rec (int_succ_pred2 z) = r (int_rec z)
  Proof.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
forall z : Int, ap int_rec (int_succ_pred2 z) = r (int_rec z)
    intro z.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
ap int_rec (int_succ_pred2 z) = r (int_rec z)
    napply (cancelL (transport_const (int_succ_pred2 z) _)).
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
transport_const (int_succ_pred2 z) (int_rec (int_pred2 z).+1) @
ap int_rec (int_succ_pred2 z) =
transport_const (int_succ_pred2 z) (int_rec (int_pred2 z).+1) @ r (int_rec z)
    lhs_V napply apD_const.
P: Type
t0: P
f, g1, g2: P -> P
s: g1 o f == idmap
r: f o g2 == idmap
z: Int
apD int_rec (int_succ_pred2 z) =
transport_const (int_succ_pred2 z) (int_rec (int_pred2 z).+1) @ r (int_rec z)
    napply int_ind_beta_int_succ_pred2.
  Defined.

End RecursionPrinciple.

(** The recursion principle phrased using a biinvertible map. *)
Definition int_rec_biinv {P : Type} (t0 : P) (f : P -> P) `{IsBiInv P P f}
  : Int -> P
  := int_rec t0 f (retr_biinv f) (sect_biinv f) (eissect_biinv f) (eisretr_biinv f).

(** The recursion principle phrased using a half-adjoint equivalence. *)
Definition int_rec_equiv {P : Type} (t0 : P) (f : P -> P) `{IsEquiv P P f}
  : Int -> P
  := @int_rec_biinv P t0 f (isbiinv_isequiv _ _).

(** Equivalence iteration.  The properties of this are proved later in the file. *)
Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (z : Int) (a0 : A) : A
  := int_rec_equiv a0 f z.

Section Uniqueness.

  Context {P : Type} (e : BiInv P P).

  (** The following uniqueness principle states that if two maps out of [Int] agree on 0 and commute with the successor, then they are homotopic. *)
  Definition int_homotopic_biinv (k1 : Int -> P) (k2 : Int -> P)
    (p0 : k1 zero = k2 zero) (pf1 : k1 o int_succ == e o k1) (pf2 : k2 o int_succ == e o k2)
    : k1 == k2.
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
k1 == k2
  Proof.
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
k1 == k2
    snapply int_ind_equiv; cbn beta.
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
k1 zero = k2 zero
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
forall z : Int, k1 z = k2 z -> k1 z.+1 = k2 z.+1
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
forall z : Int, IsEquiv (?Goal0 z)
    -
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
k1 zero = k2 zero exact p0.
    -
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
forall z : Int, k1 z = k2 z -> k1 z.+1 = k2 z.+1 intro z.
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
z: Int
k1 z = k2 z -> k1 z.+1 = k2 z.+1
      exact (equiv_concat_l (pf1 z) _ oE equiv_concat_r (pf2 z)^ _ oE equiv_ap e _ _).
    -
P: Type
e: BiInv P P
k1, k2: Int -> P
p0: k1 zero = k2 zero
pf1: k1 o int_succ == e o k1
pf2: k2 o int_succ == e o k2
forall z : Int,
IsEquiv
  ((fun z0 : Int =>
    equiv_fun
      (equiv_concat_l (pf1 z0) (k2 z0.+1)
       oE equiv_concat_r (pf2 z0)^ (e (k1 z0)) oE 
       equiv_ap e (k1 z0) (k2 z0)))
     z) exact _.
  Defined.

  (** As a special case, we can characterize the recursor. *)
  Definition int_homotopic_rec (t0 : P) (k : Int -> P)
    (p0 : k zero = t0) (pf : k o int_succ == e o k)
    (rec := int_rec_biinv t0 e)
    : k == rec
    := int_homotopic_biinv k rec p0 pf (fun _ => idpath).

End Uniqueness.

(** The same uniqueness principle but for half-adjoint equivalences. *)
Definition int_homotopic {P : Type} (f : P -> P)
  {e' : IsEquiv f} (k1 : Int -> P) (k2 : Int -> P)
  (p0 : k1 zero = k2 zero) (pf1 : k1 o int_succ == f o k1)
  (pf2 : k2 o int_succ == f o k2)
  : forall (z : Int), k1 z = k2 z
  := int_homotopic_biinv (Build_BiInv P P _ (isbiinv_isequiv f e')) k1 k2 p0 pf1 pf2.

(** ** [Int] is equivalent to [SInt] *)

Definition int_to_sint : Int -> SInt
  := int_rec sint_zero sint_succ sint_pred sint_pred sint_pred_succ sint_succ_pred.

Definition sint_to_int : SInt -> Int.
SInt -> Int
Proof.
SInt -> Int
  intro s; induction s as [|n IHz|n IHz].
Int
n: nat
IHz: Int
Int
n: nat
IHz: Int
Int
  -
Int exact zero.
  -
n: nat
IHz: Int
Int exact (int_succ IHz).
  -
n: nat
IHz: Int
Int exact (int_pred IHz).
Defined.

Definition sint_to_int_issect : int_to_sint o sint_to_int == idmap.
int_to_sint o sint_to_int == idmap
Proof.
int_to_sint o sint_to_int == idmap
  intro s; induction s as [|[|n] IHz|[|n] IHz].
int_to_sint (sint_to_int sint_zero) = sint_zero
IHz: int_to_sint (sint_to_int (sint_of_nat 0)) = sint_of_nat 0
int_to_sint (sint_to_int (sint_PosS 0)) = sint_PosS 0
n: nat
IHz: int_to_sint (sint_to_int (sint_of_nat n.+1)) = sint_of_nat n.+1
int_to_sint (sint_to_int (sint_PosS n.+1)) = sint_PosS n.+1
IHz: int_to_sint (sint_to_int (sint_neg (sint_of_nat 0))) =
sint_neg (sint_of_nat 0)
int_to_sint (sint_to_int (sint_NegS 0)) = sint_NegS 0
n: nat
IHz: int_to_sint (sint_to_int (sint_neg (sint_of_nat n.+1))) =
sint_neg (sint_of_nat n.+1)
int_to_sint (sint_to_int (sint_NegS n.+1)) = sint_NegS n.+1
  1, 2, 4: reflexivity.
n: nat
IHz: int_to_sint (sint_to_int (sint_of_nat n.+1)) = sint_of_nat n.+1
int_to_sint (sint_to_int (sint_PosS n.+1)) = sint_PosS n.+1
n: nat
IHz: int_to_sint (sint_to_int (sint_neg (sint_of_nat n.+1))) =
sint_neg (sint_of_nat n.+1)
int_to_sint (sint_to_int (sint_NegS n.+1)) = sint_NegS n.+1
  -
n: nat
IHz: int_to_sint (sint_to_int (sint_of_nat n.+1)) = sint_of_nat n.+1
int_to_sint (sint_to_int (sint_PosS n.+1)) = sint_PosS n.+1 exact (ap sint_succ IHz).
  -
n: nat
IHz: int_to_sint (sint_to_int (sint_neg (sint_of_nat n.+1))) =
sint_neg (sint_of_nat n.+1)
int_to_sint (sint_to_int (sint_NegS n.+1)) = sint_NegS n.+1 exact (ap sint_pred IHz).
Defined.

Definition sint_to_int_succ : sint_to_int o sint_succ == int_succ o sint_to_int.
sint_to_int o sint_succ == int_succ o sint_to_int
Proof.
sint_to_int o sint_succ == int_succ o sint_to_int
  intro s; induction s as [|[|n] IHz|[|n] IHz].
sint_to_int (sint_succ sint_zero) = (sint_to_int sint_zero).+1
IHz: sint_to_int (sint_succ (sint_of_nat 0)) = (sint_to_int (sint_of_nat 0)).+1
sint_to_int (sint_succ (sint_PosS 0)) = (sint_to_int (sint_PosS 0)).+1
n: nat
IHz: sint_to_int (sint_succ (sint_of_nat n.+1)) =
(sint_to_int (sint_of_nat n.+1)).+1
sint_to_int (sint_succ (sint_PosS n.+1)) = (sint_to_int (sint_PosS n.+1)).+1
IHz: sint_to_int (sint_succ (sint_neg (sint_of_nat 0))) =
(sint_to_int (sint_neg (sint_of_nat 0))).+1
sint_to_int (sint_succ (sint_NegS 0)) = (sint_to_int (sint_NegS 0)).+1
n: nat
IHz: sint_to_int (sint_succ (sint_neg (sint_of_nat n.+1))) =
(sint_to_int (sint_neg (sint_of_nat n.+1))).+1
sint_to_int (sint_succ (sint_NegS n.+1)) = (sint_to_int (sint_NegS n.+1)).+1
  1-3: reflexivity.
IHz: sint_to_int (sint_succ (sint_neg (sint_of_nat 0))) =
(sint_to_int (sint_neg (sint_of_nat 0))).+1
sint_to_int (sint_succ (sint_NegS 0)) = (sint_to_int (sint_NegS 0)).+1
n: nat
IHz: sint_to_int (sint_succ (sint_neg (sint_of_nat n.+1))) =
(sint_to_int (sint_neg (sint_of_nat n.+1))).+1
sint_to_int (sint_succ (sint_NegS n.+1)) = (sint_to_int (sint_NegS n.+1)).+1
  all: symmetry; exact (int_succ_pred _).
Defined.

Definition sint_to_int_isretr : sint_to_int o int_to_sint == idmap.
sint_to_int o int_to_sint == idmap
Proof.
sint_to_int o int_to_sint == idmap
  napply (int_homotopic_biinv biinv_int_succ).
sint_to_int (int_to_sint zero) = zero
(fun x : Int => sint_to_int (int_to_sint x.+1)) ==
(fun x : Int => biinv_int_succ (sint_to_int (int_to_sint x)))
(fun x : Int => x.+1) == (fun x : Int => biinv_int_succ x)
  1,3: reflexivity.
(fun x : Int => sint_to_int (int_to_sint x.+1)) ==
(fun x : Int => biinv_int_succ (sint_to_int (int_to_sint x)))
  intro z; simpl.
z: Int
sint_to_int (sint_succ (int_to_sint z)) = (sint_to_int (int_to_sint z)).+1
  apply sint_to_int_succ.
Defined.

(** [sint_to_int] is biinvertible.  It follows from typeclass inference that it is an equivalence. *)
Instance isbiinv_sint_to_int : IsBiInv sint_to_int
  := Build_IsBiInv _ _ _ _ _ sint_to_int_isretr sint_to_int_issect.

(** Since [SInt] has decidable equality, so does [Int]. *)
Instance decidablepaths_int@{} : DecidablePaths Int
  := decidablepaths_equiv SInt _ _.

(** Since [SInt] is a set, therefore also [Int] is a set. *)
Instance ishset_int : IsHSet Int
  := istrunc_isequiv_istrunc SInt _.

(** The following function reduces an integer expression by cancelling successive successor and predecessor terms. It is homotopic to the identity by [sint_to_int_isretr]. *)
Definition int_reduce : Int -> Int := sint_to_int o int_to_sint.

(** From the equivalence to [SInt] we can deduce another induction principle for [Int].  This one has weak hypotheses, but since [HN 1 (HP 0 t)] doesn't necessarily transport to [t] along [int_pred_succ 0], it is impossible for it to compute well on general [int_pred] and [int_succ] operations.  Passing through [SInt] normalizes terms giving us a canonical choice. *)
Definition int_ind_sint (P : Int -> Type)
  (H0 : P zero)
  (HP : forall z, P z -> P z.+1)
  (HN : forall z, P z -> P z.-1)
  : forall z, P z.
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
forall z : Int, P z
Proof.
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
forall z : Int, P z
  equiv_intro sint_to_int s.
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
s: SInt
P (sint_to_int s)
  induction s as [|n IHz|n IHz].
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
P (sint_to_int sint_zero)
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_of_nat n))
P (sint_to_int (sint_PosS n))
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_neg (sint_of_nat n)))
P (sint_to_int (sint_NegS n))
  -
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
P (sint_to_int sint_zero) exact H0.
  -
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_of_nat n))
P (sint_to_int (sint_PosS n)) destruct n as [|n].
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
IHz: P (sint_to_int (sint_of_nat 0))
P (sint_to_int (sint_PosS 0))
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_of_nat n.+1))
P (sint_to_int (sint_PosS n.+1))
    all: apply HP, IHz.
  -
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_neg (sint_of_nat n)))
P (sint_to_int (sint_NegS n)) destruct n as [|n].
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
IHz: P (sint_to_int (sint_neg (sint_of_nat 0)))
P (sint_to_int (sint_NegS 0))
P: Int -> Type
H0: P zero
HP: forall z : Int, P z -> P z.+1
HN: forall z : Int, P z -> P z.-1
n: nat
IHz: P (sint_to_int (sint_neg (sint_of_nat n.+1)))
P (sint_to_int (sint_NegS n.+1))
    all: apply HN, IHz.
Defined.

Definition int_ind_iff (P : Int -> Type)
  (t0 : P zero) (f : forall z : Int, P z <-> P z.+1)
  : forall z, P z.
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z
Proof.
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z
  srapply (int_ind_sint P t0).
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z -> P z.+1
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z -> P z.-1
  -
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z -> P z.+1 intro z.
P: Int -> Type
t0: P zero
f: forall z0 : Int, P z0 <-> P z0.+1
z: Int
P z -> P z.+1  exact (fst (f z)).
  -
P: Int -> Type
t0: P zero
f: forall z : Int, P z <-> P z.+1
forall z : Int, P z -> P z.-1 equiv_intro int_succ z.
P: Int -> Type
t0: P zero
f: forall z0 : Int, P z0 <-> P z0.+1
z: Int
P z.+1 -> P z.+1.-1
    refine (_ o snd (f z)).
P: Int -> Type
t0: P zero
f: forall z0 : Int, P z0 <-> P z0.+1
z: Int
P z -> P z.+1.-1
    exact (transport P (int_pred_succ z)^).
Defined.

(** ** Printing and parsing *)

(** We pass through [SInt] for printing and parsing. *)
Definition int_to_number_int : Int -> Numeral.int := sint_to_number_int o int_to_sint.

Definition int_of_number_int : Numeral.int -> Int := sint_to_int o sint_of_number_int.

Number Notation Int int_of_number_int int_to_number_int : int_scope.

(** ** Integer arithmetic *)

(** *** Negation *)

Definition int_neg (z : Int) : Int
  := int_rec_equiv zero int_pred z.

Notation "- z" := (int_neg z) : int_scope.

(** Negation is involutive. *)
Definition int_neg_neg (z : Int) : --z = z.
z: Int
- - z = z
Proof.
z: Int
- - z = z
  revert z.
forall z : Int, - - z = z
  by srapply (int_homotopic int_succ).
Defined.

(** Negation is an equivalence. *)
Instance isequiv_int_neg : IsEquiv int_neg.
IsEquiv int_neg
Proof.
IsEquiv int_neg
  snapply (isequiv_adjointify int_neg int_neg).
int_neg o int_neg == idmap
int_neg o int_neg == idmap
  1,2: napply int_neg_neg.
Defined.

(** Negation is injective. *)
Definition isinj_int_neg (x y : Int) : -x = -y -> x = y
  := equiv_inj int_neg.

(** The negation of a successor is the predecessor of the negation. *)
Definition int_neg_succ (z : Int) : -(z.+1) = (-z).-1
  := idpath.

(** The negation of a predecessor is the successor of the negation. *)
Definition int_neg_pred (z : Int) : -(z.-1) = (-z).+1
  := idpath.

(** *** Addition *)

(** We define addition by recursion on the first argument. *)
Definition int_add (x y : Int) : Int
  := int_iter int_succ x y.

Infix "+" := int_add : int_scope.
Infix "-" := (fun x y => x + -y) : int_scope.

(** Integer addition with zero on the left is the identity by definition. *)
Definition int_add_0_l (z : Int) : 0 + z = z
  := idpath.

(** Adding a successor on the left is the successor of the sum. *)
Definition int_add_succ_l (x y : Int) : x.+1 + y = (x + y).+1
  := idpath.

(** Adding a predecessor on the left is the predecessor of the sum. *)
Definition int_add_pred_l (x y : Int) : x.-1 + y = (x + y).-1
  := idpath.

(** Integer addition with 1 on the left is the successor. *)
Definition int_add_1_l (z : Int) : 1 + z = z.+1
  := idpath.

(** Integer addition with zero on the right is the identity. *)
Definition int_add_0_r (z : Int) : z + 0 = z.
z: Int
z + 0 = z
Proof.
z: Int
z + 0 = z
  revert z.
forall z : Int, z + 0 = z
  by srapply (int_homotopic int_succ).
Defined.

(** Adding a successor on the right is the successor of the sum. *)
Definition int_add_succ_r (x y : Int) : x + y.+1 = (x + y).+1.
x, y: Int
x + y.+1 = (x + y).+1
Proof.
x, y: Int
x + y.+1 = (x + y).+1
  revert x.
y: Int
forall x : Int, x + y.+1 = (x + y).+1
  by srapply (int_homotopic int_succ).
Defined.

(** Integer addition is commutative. *)
Definition int_add_comm (x y : Int) : x + y = y + x.
x, y: Int
x + y = y + x
Proof.
x, y: Int
x + y = y + x
  revert x.
y: Int
forall x : Int, x + y = y + x
  srapply (int_homotopic int_succ); cbn beta.
y: Int
0 + y = y + 0
y: Int
(fun x : Int => x.+1 + y) == (fun x : Int => (x + y).+1)
y: Int
(fun x : Int => y + x.+1) == (fun x : Int => (y + x).+1)
  -
y: Int
0 + y = y + 0 by rewrite int_add_0_r.
  -
y: Int
(fun x : Int => x.+1 + y) == (fun x : Int => (x + y).+1) reflexivity.
  -
y: Int
(fun x : Int => y + x.+1) == (fun x : Int => (y + x).+1) intro z.
y, z: Int
y + z.+1 = (y + z).+1
    by rewrite int_add_succ_r.
Defined.

(** Adding a predecessor on the right is the predecessor of the sum. *)
Definition int_add_pred_r (x y : Int) : x + y.-1 = (x + y).-1
  := int_add_comm x y.-1 @ ap int_pred (int_add_comm y x).

(** Integer addition with 1 on the right is the successor. *)
Definition int_add_1_r (z : Int) : z + 1 = z.+1.
z: Int
z + 1 = z.+1
Proof.
z: Int
z + 1 = z.+1
  revert z.
forall z : Int, z + 1 = z.+1
  by srapply (int_homotopic int_succ).
Defined.

(** Integer addition is associative. *)
Definition int_add_assoc (x y z : Int) : x + (y + z) = x + y + z.
x, y, z: Int
x + (y + z) = x + y + z
Proof.
x, y, z: Int
x + (y + z) = x + y + z
  revert x.
y, z: Int
forall x : Int, x + (y + z) = x + y + z
  by srapply (int_homotopic int_succ).
Defined.

(** Negation is a left inverse with respect to integer addition. *)
Definition int_add_neg_l (z : Int) : -z + z = 0.
z: Int
- z + z = 0
Proof.
z: Int
- z + z = 0
  revert z.
forall z : Int, - z + z = 0
  srapply (int_homotopic idmap); cbn beta.
- 0 + 0 = 0
(fun x : Int => - x.+1 + x.+1) == (fun x : Int => - x + x)
(fun _ : Int => 0) == (fun _ : Int => 0)
  1,3: reflexivity.
(fun x : Int => - x.+1 + x.+1) == (fun x : Int => - x + x)
  simpl; intro s.
s: Int
(- s + s.+1).-1 = - s + s
  rewrite int_add_succ_r.
s: Int
(- s + s).+1.-1 = - s + s
  apply int_pred_succ.
Defined.

(** Negation is a right inverse with respect to integer addition. *)
Definition int_add_neg_r (z : Int) : z - z = 0
  := int_add_comm _ _ @ int_add_neg_l _.

(** Negation distributes over addition. *)
Definition int_neg_add (x y : Int) : -(x + y) = -x - y.
x, y: Int
- (x + y) = - x - y
Proof.
x, y: Int
- (x + y) = - x - y
  revert x.
y: Int
forall x : Int, - (x + y) = - x - y
  by srapply (int_homotopic int_pred).
Defined.

(** Addition is an equivalence with first argument fixed. *)
Instance isequiv_int_add_l (x : Int) : IsEquiv (int_add x).
x: Int
IsEquiv (int_add x)
Proof.
x: Int
IsEquiv (int_add x)
  srapply (isequiv_adjointify _ (int_add (-x))).
x: Int
int_add x o int_add (- x) == idmap
x: Int
int_add (- x) o int_add x == idmap
  all: simpl; intro y.
x, y: Int
x + (- x + y) = y
x, y: Int
- x + (x + y) = y
  all: lhs napply int_add_assoc.
x, y: Int
x + - x + y = y
x, y: Int
- x + x + y = y
  -
x, y: Int
x + - x + y = y by rewrite int_add_neg_r.
  -
x, y: Int
- x + x + y = y by rewrite int_add_neg_l.
Defined.

(** Addition is an equivalence with second argument fixed.  This also follows from the previous result and [int_add_comm], but this proof computes better. *)
Instance isequiv_int_add_r (y : Int) : IsEquiv (fun x => x + y).
y: Int
IsEquiv (fun x : Int => x + y)
Proof.
y: Int
IsEquiv (fun x : Int => x + y)
  snapply (isequiv_adjointify _ (fun x => x - y)).
y: Int
(fun x : Int => x + y) o (fun x : Int => x - y) == idmap
y: Int
(fun x : Int => x - y) o (fun x : Int => x + y) == idmap
  all: simpl; intro x.
y, x: Int
x + - y + y = x
y, x: Int
x + y + - y = x
  all: lhs_V napply int_add_assoc.
y, x: Int
x + (- y + y) = x
y, x: Int
x + (y + - y) = x
  -
y, x: Int
x + (- y + y) = x rewrite int_add_neg_l.
y, x: Int
x + 0 = x
    apply int_add_0_r.
  -
y, x: Int
x + (y + - y) = x rewrite int_add_neg_r.
y, x: Int
x + 0 = x
    apply int_add_0_r.
Defined.

(** *** Multiplication *)

(** We define multiplication by recursion on the first argument.  This depends on the proof that addition is an equivalence. *)
Definition int_mul (x y : Int) : Int
  := int_iter (fun z => z + y) x 0.

Infix "*" := int_mul : int_scope.

(** Integer multiplication with zero on the left is zero by definition. *)
Definition int_mul_0_l (z : Int) : 0 * z = 0
  := idpath.

(** Multiplication with a successor on the left adds the other argument. *)
Definition int_mul_succ_l (x y : Int) : x.+1 * y = x * y + y
  := idpath.

(** Multiplication with a predecessor on the left subtracts the other argument. *)
Definition int_mul_pred_l (x y : Int) : x.-1 * y = x * y - y
  := idpath.

(** Integer multiplication with one on the left is the identity. *)
Definition int_mul_1_l (z : Int) : 1 * z = z
  := idpath.

(** Integer multiplication with [-1] on the left is negation. *)
Definition int_mul_neg1_l (z : Int) : -1 * z = -z
  := idpath.

(** Multiplying with a negation on the left is the same as negating the product. *)
Definition int_mul_neg_l (x y : Int) : -x * y = -(x * y).
x, y: Int
- x * y = - (x * y)
Proof.
x, y: Int
- x * y = - (x * y)
  revert x.
y: Int
forall x : Int, - x * y = - (x * y)
  rapply (int_homotopic (fun x => x - y)); cbn beta.
y: Int
- 0 * y = - (0 * y)
y: Int
(fun x : Int => - x.+1 * y) == (fun x : Int => - x * y + - y)
y: Int
(fun x : Int => - (x.+1 * y)) == (fun x : Int => - (x * y) + - y)
  1,2: reflexivity.
y: Int
(fun x : Int => - (x.+1 * y)) == (fun x : Int => - (x * y) + - y)
  simpl; intro x.
y, x: Int
- (x * y + y) = - (x * y) + - y
  apply int_neg_add.
Defined.

(** Multiplication distributes over addition on the left. *)
Definition int_dist_l (x y z : Int) : x * (y + z) = x * y + x * z.
x, y, z: Int
x * (y + z) = x * y + x * z
Proof.
x, y, z: Int
x * (y + z) = x * y + x * z
  revert x.
y, z: Int
forall x : Int, x * (y + z) = x * y + x * z
  srapply (int_homotopic (fun x => x + (y + z))); cbn beta.
y, z: Int
0 * (y + z) = 0 * y + 0 * z
y, z: Int
(fun x : Int => x.+1 * (y + z)) == (fun x : Int => x * (y + z) + (y + z))
y, z: Int
(fun x : Int => x.+1 * y + x.+1 * z) ==
(fun x : Int => x * y + x * z + (y + z))
  1,2: reflexivity.
y, z: Int
(fun x : Int => x.+1 * y + x.+1 * z) ==
(fun x : Int => x * y + x * z + (y + z))
  simpl; intro x.
y, z, x: Int
x * y + y + (x * z + z) = x * y + x * z + (y + z)
  lhs_V napply int_add_assoc.
y, z, x: Int
x * y + (y + (x * z + z)) = x * y + x * z + (y + z)
  rewrite (int_add_comm y (x * z + z)).
y, z, x: Int
x * y + (x * z + z + y) = x * y + x * z + (y + z)
  rewrite (int_add_comm y z).
y, z, x: Int
x * y + (x * z + z + y) = x * y + x * z + (z + y)
  by rewrite <- 2 int_add_assoc.
Defined.

(** Integer multiplication with zero on the right is zero. *)
Definition int_mul_0_r (z : Int) : z * 0 = 0.
z: Int
z * 0 = 0
Proof.
z: Int
z * 0 = 0
  revert z.
forall z : Int, z * 0 = 0
  rapply (int_homotopic idmap); cbn beta.
0 * 0 = 0
(fun x : Int => x.+1 * 0) == (fun x : Int => x * 0)
(fun _ : Int => 0) == (fun _ : Int => 0)
  1,3: reflexivity.
(fun x : Int => x.+1 * 0) == (fun x : Int => x * 0)
  simpl; intro z.
z: Int
z * 0 + 0 = z * 0
  apply int_add_0_r.
Defined.

(** Multiplying with a successor on the right adds the other argument. *)
Definition int_mul_succ_r (x y : Int) : x * y.+1 = x + x * y.
x, y: Int
x * y.+1 = x + x * y
Proof.
x, y: Int
x * y.+1 = x + x * y
  revert x.
y: Int
forall x : Int, x * y.+1 = x + x * y
  rapply (int_homotopic (fun x => x + y.+1)); cbn beta.
y: Int
0 * y.+1 = 0 + 0 * y
y: Int
(fun x : Int => x.+1 * y.+1) == (fun x : Int => x * y.+1 + y.+1)
y: Int
(fun x : Int => x.+1 + x.+1 * y) == (fun x : Int => x + x * y + y.+1)
  1,2: reflexivity.
y: Int
(fun x : Int => x.+1 + x.+1 * y) == (fun x : Int => x + x * y + y.+1)
  simpl; intro z.
y, z: Int
(z + (z * y + y)).+1 = z + z * y + y.+1
  rewrite int_add_succ_r.
y, z: Int
(z + (z * y + y)).+1 = (z + z * y + y).+1
  by rewrite int_add_assoc.
Defined.

(** Multiplication is commutative. *)
Definition int_mul_comm (x y : Int) : x * y = y * x.
x, y: Int
x * y = y * x
Proof.
x, y: Int
x * y = y * x
  revert x.
y: Int
forall x : Int, x * y = y * x
  srapply (int_homotopic (fun x => x + y)); cbn beta.
y: Int
0 * y = y * 0
y: Int
(fun x : Int => x.+1 * y) == (fun x : Int => x * y + y)
y: Int
(fun x : Int => y * x.+1) == (fun x : Int => y * x + y)
  -
y: Int
0 * y = y * 0 symmetry; apply int_mul_0_r.
  -
y: Int
(fun x : Int => x.+1 * y) == (fun x : Int => x * y + y) reflexivity.
  -
y: Int
(fun x : Int => y * x.+1) == (fun x : Int => y * x + y) intro z.
y, z: Int
y * z.+1 = y * z + y
    rewrite int_add_comm.
y, z: Int
y * z.+1 = y + y * z
    apply int_mul_succ_r.
Defined.

(** Multiplying with a predecessor on the right subtracts the other argument. *)
Definition int_mul_pred_r (x y : Int) : x * y.-1 = x * y - x
  := int_mul_comm x y.-1 @ ap _ (int_mul_comm y x).

(** Integer multiplication with one on the right is the identity. *)
Definition int_mul_1_r (z : Int) : z * 1 = z
  := int_mul_comm _ _.

(** Multiplying with a negation on the right is the same as negating the product. *)
Definition int_mul_neg_r (x y : Int) : x * -y = -(x * y)
  := int_mul_comm _ _ @ int_mul_neg_l _ _ @ ap _ (int_mul_comm _ _).

(** Multiplication distributes over addition on the right. *)
Definition int_dist_r (x y z : Int) : (x + y) * z = x * z + y * z.
x, y, z: Int
(x + y) * z = x * z + y * z
Proof.
x, y, z: Int
(x + y) * z = x * z + y * z
  by rewrite int_mul_comm, int_dist_l, !(int_mul_comm z).
Defined.

(** Multiplication is associative. *)
Definition int_mul_assoc (x y z : Int) : x * (y * z) = x * y * z.
x, y, z: Int
x * (y * z) = x * y * z
Proof.
x, y, z: Int
x * (y * z) = x * y * z
  revert x.
y, z: Int
forall x : Int, x * (y * z) = x * y * z
  srapply (int_homotopic (fun x => x + (y * z))); cbn beta.
y, z: Int
0 * (y * z) = 0 * y * z
y, z: Int
(fun x : Int => x.+1 * (y * z)) == (fun x : Int => x * (y * z) + y * z)
y, z: Int
(fun x : Int => x.+1 * y * z) == (fun x : Int => x * y * z + y * z)
  1,2: reflexivity.
y, z: Int
(fun x : Int => x.+1 * y * z) == (fun x : Int => x * y * z + y * z)
  simpl; intro x.
y, z, x: Int
(x * y + y) * z = x * y * z + y * z
  by rewrite int_dist_r.
Defined.

(** ** Results about iteration of equivalences *)

Definition int_iter_neg {A} (f : A -> A) `{IsEquiv _ _ f} (z : Int) (a : A)
  : int_iter f (int_neg z) a = int_iter f^-1 z a.
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f (- z) a = int_iter f^-1 z a
Proof.
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f (- z) a = int_iter f^-1 z a
  revert z.
A: Type
f: A -> A
H: IsEquiv f
a: A
forall z : Int, int_iter f (- z) a = int_iter f^-1 z a
  by srapply (int_homotopic f^-1).
Defined.

Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f} (z : Int) (a : A)
  : int_iter f z.+1 a = f (int_iter f z a)
  := idpath.

Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f} (z : Int) (a : A)
  : int_iter f z.+1 a = int_iter f z (f a).
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f z.+1 a = int_iter f z (f a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f z.+1 a = int_iter f z (f a)
  revert z.
A: Type
f: A -> A
H: IsEquiv f
a: A
forall z : Int, int_iter f z.+1 a = int_iter f z (f a)
  by srapply (int_homotopic f).
Defined.

Definition int_iter_pred_l {A} (f : A -> A) `{IsEquiv _ _ f} (z : Int) (a : A)
  : int_iter f z.-1 a = f^-1 (int_iter f z a)
  := idpath.

Definition int_iter_pred_r {A} (f : A -> A) `{IsEquiv _ _ f} (z : Int) (a : A)
  : int_iter f z.-1 a = int_iter f z (f^-1 a).
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f z.-1 a = int_iter f z (f^-1 a)
Proof.
A: Type
f: A -> A
H: IsEquiv f
z: Int
a: A
int_iter f z.-1 a = int_iter f z (f^-1 a)
  revert z.
A: Type
f: A -> A
H: IsEquiv f
a: A
forall z : Int, int_iter f z.-1 a = int_iter f z (f^-1 a)
  srapply (int_homotopic f); cbn beta.
A: Type
f: A -> A
H: IsEquiv f
a: A
int_iter f (-1) a = int_iter f 0 (f^-1 a)
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun x : Int => int_iter f x.+1.-1 a) ==
(fun x : Int => f (int_iter f x.-1 a))
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun x : Int => int_iter f x.+1 (f^-1 a)) ==
(fun x : Int => f (int_iter f x (f^-1 a)))
  1,3: reflexivity.
A: Type
f: A -> A
H: IsEquiv f
a: A
(fun x : Int => int_iter f x.+1.-1 a) ==
(fun x : Int => f (int_iter f x.-1 a))
  intro z; simpl.
A: Type
f: A -> A
H: IsEquiv f
a: A
z: Int
f^-1 (f (int_iter f z a)) = f (f^-1 (int_iter f z a))
  exact (eissect f (int_iter f z a) @ (eisretr f (int_iter f z a))^).
Defined.

Definition int_iter_add {A} (f : A -> A) `{IsEquiv _ _ f} (x y : Int)
  : int_iter f (x + y) == int_iter f x o int_iter f y.
A: Type
f: A -> A
H: IsEquiv f
x, y: Int
int_iter f (x + y) == int_iter f x o int_iter f y
Proof.
A: Type
f: A -> A
H: IsEquiv f
x, y: Int
int_iter f (x + y) == int_iter f x o int_iter f y
  intro a; revert x.
A: Type
f: A -> A
H: IsEquiv f
y: Int
a: A
forall x : Int, int_iter f (x + y) a = int_iter f x (int_iter f y a)
  by srapply (int_homotopic f).
Defined.

(** If [g : A -> A'] commutes with automorphisms of [A] and [A'], then it commutes with iteration. *)
Definition int_iter_commute_map {A A'} (f : A -> A) `{!IsEquiv f}
  (f' : A' -> A') `{!IsEquiv f'}
  (g : A -> A') (p : g o f == f' o g) (z : Int) (a : A)
  : g (int_iter f z a) = int_iter f' z (g a).
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
z: Int
a: A
g (int_iter f z a) = int_iter f' z (g a)
Proof.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
z: Int
a: A
g (int_iter f z a) = int_iter f' z (g a)
  revert z.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
forall z : Int, g (int_iter f z a) = int_iter f' z (g a)
  srapply (int_homotopic f'); cbn beta.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
g (int_iter f 0 a) = int_iter f' 0 (g a)
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
(fun x : Int => g (int_iter f x.+1 a)) ==
(fun x : Int => f' (g (int_iter f x a)))
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
(fun x : Int => int_iter f' x.+1 (g a)) ==
(fun x : Int => f' (int_iter f' x (g a)))
  1,3: reflexivity.
A, A': Type
f: A -> A
IsEquiv0: IsEquiv f
f': A' -> A'
IsEquiv1: IsEquiv f'
g: A -> A'
p: g o f == f' o g
a: A
(fun x : Int => g (int_iter f x.+1 a)) ==
(fun x : Int => f' (g (int_iter f x a)))
  intro x; apply p.
Defined.

(** In particular, homotopic maps have homotopic iterations. *)
Definition int_iter_homotopic (z : Int) {A} (f f' : A -> A) `{!IsEquiv f} `{!IsEquiv f'}
  (h : f == f')
  : int_iter f z == int_iter f' z
  := int_iter_commute_map f f' idmap h z.

(** [int_iter f n x] doesn't depend on the proof that [f] is an equivalence. *)
Definition int_iter_agree (z : Int) {A} (f : A -> A) {ief ief' : IsEquiv f}
  : forall x, @int_iter A f ief z x = @int_iter A f ief' z x
  := int_iter_homotopic z f f (fun _ => idpath).

(** An important invariance property of iteration.  The most obvious proof attempts fail, for the reasons described in the comment for [int_ind_sint]. *)
Definition int_iter_invariant {A} (f : A -> A) `{!IsEquiv f}
  (P : A -> Type)
  (Psucc : forall a, P a -> P (f a))
  (Ppred : forall a, P a -> P (f^-1 a))
  (a0 : A) (Pa0 : P a0)
  : forall z, P (int_iter f z a0).
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0)
Proof.
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0)
  snapply int_ind_sint; cbn.
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
P a0
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0) -> P (f (int_rec_equiv a0 f z))
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0) -> P (f^-1 (int_rec_equiv a0 f z))
  -
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
P a0 exact Pa0.
  -
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0) -> P (f (int_rec_equiv a0 f z)) intros z IH.
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
z: Int
IH: P (int_iter f z a0)
P (f (int_rec_equiv a0 f z)) apply Psucc, IH.
  -
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
forall z : Int, P (int_iter f z a0) -> P (f^-1 (int_rec_equiv a0 f z)) intros z IH.
A: Type
f: A -> A
IsEquiv0: IsEquiv f
P: A -> Type
Psucc: forall a : A, P a -> P (f a)
Ppred: forall a : A, P a -> P (f^-1 a)
a0: A
Pa0: P a0
z: Int
IH: P (int_iter f z a0)
P (f^-1 (int_rec_equiv a0 f z)) apply Ppred, IH.
Defined.

(** ** Exponentiation of loops *)

Definition loopexp {A : Type} {a : A} (p : a = a) (z : Int) : (a = a)
  := int_iter (equiv_concat_r p a) z idpath.

Definition loopexp_succ_r {A : Type} {a : A} (p : a = a) (z : Int)
  : loopexp p z.+1 = loopexp p z @ p
  := idpath.

Definition loopexp_pred_r {A : Type} {a : A} (p : a = a) (z : Int)
  : loopexp p z.-1 = loopexp p z @ p^
  := idpath.

Definition loopexp_succ_l {A : Type} {a : A} (p : a = a) (z : Int)
  : loopexp p z.+1 = p @ loopexp p z.
A: Type
a: A
p: a = a
z: Int
loopexp p z.+1 = p @ loopexp p z
Proof.
A: Type
a: A
p: a = a
z: Int
loopexp p z.+1 = p @ loopexp p z
  simpl; revert z.
A: Type
a: A
p: a = a
forall z : Int, loopexp p z @ p = p @ loopexp p z
  rapply (int_homotopic (equiv_concat_r p a)); cbn beta.
A: Type
a: A
p: a = a
loopexp p 0 @ p = p @ loopexp p 0
A: Type
a: A
p: a = a
(fun x : Int => loopexp p x.+1 @ p) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ p))
A: Type
a: A
p: a = a
(fun x : Int => p @ loopexp p x.+1) ==
(fun x : Int => equiv_concat_r p a (p @ loopexp p x))
  -
A: Type
a: A
p: a = a
loopexp p 0 @ p = p @ loopexp p 0 napply concat_1p_p1.
  -
A: Type
a: A
p: a = a
(fun x : Int => loopexp p x.+1 @ p) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ p)) reflexivity.
  -
A: Type
a: A
p: a = a
(fun x : Int => p @ loopexp p x.+1) ==
(fun x : Int => equiv_concat_r p a (p @ loopexp p x)) intro z; simpl.
A: Type
a: A
p: a = a
z: Int
p @ (loopexp p z @ p) = (p @ loopexp p z) @ p
    apply concat_p_pp.
Defined.

Definition loopexp_pred_l {A : Type} {a : A} (p : a = a) (z : Int)
  : loopexp p z.-1 = p^ @ loopexp p z.
A: Type
a: A
p: a = a
z: Int
loopexp p z.-1 = p^ @ loopexp p z
Proof.
A: Type
a: A
p: a = a
z: Int
loopexp p z.-1 = p^ @ loopexp p z
  simpl; revert z.
A: Type
a: A
p: a = a
forall z : Int, loopexp p z @ p^ = p^ @ loopexp p z
  rapply (int_homotopic (equiv_concat_r p a)); cbn beta.
A: Type
a: A
p: a = a
loopexp p 0 @ p^ = p^ @ loopexp p 0
A: Type
a: A
p: a = a
(fun x : Int => loopexp p x.+1 @ p^) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ p^))
A: Type
a: A
p: a = a
(fun x : Int => p^ @ loopexp p x.+1) ==
(fun x : Int => equiv_concat_r p a (p^ @ loopexp p x))
  -
A: Type
a: A
p: a = a
loopexp p 0 @ p^ = p^ @ loopexp p 0 napply concat_1p_p1.
  -
A: Type
a: A
p: a = a
(fun x : Int => loopexp p x.+1 @ p^) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ p^)) intro z; simpl.
A: Type
a: A
p: a = a
z: Int
(loopexp p z @ p) @ p^ = (loopexp p z @ p^) @ p
    exact (concat_pp_V _ _ @ (concat_pV_p _ _)^).
  -
A: Type
a: A
p: a = a
(fun x : Int => p^ @ loopexp p x.+1) ==
(fun x : Int => equiv_concat_r p a (p^ @ loopexp p x)) intro z; simpl.
A: Type
a: A
p: a = a
z: Int
p^ @ (loopexp p z @ p) = (p^ @ loopexp p z) @ p
    apply concat_p_pp.
Defined.

Definition ap_loopexp {A B} (f : A -> B) {a : A} (p : a = a) (z : Int)
  : ap f (loopexp p z) = loopexp (ap f p) z.
A, B: Type
f: A -> B
a: A
p: a = a
z: Int
ap f (loopexp p z) = loopexp (ap f p) z
Proof.
A, B: Type
f: A -> B
a: A
p: a = a
z: Int
ap f (loopexp p z) = loopexp (ap f p) z
  napply int_iter_commute_map.
A, B: Type
f: A -> B
a: A
p: a = a
z: Int
(fun x : a = a => ap f (equiv_concat_r p a x)) ==
(fun x : a = a => equiv_concat_r (ap f p) (f a) (ap f x))
  intro q; apply ap_pp.
Defined.

Definition loopexp_add {A : Type} {a : A} (p : a = a) x y
  : loopexp p (x + y) = loopexp p x @ loopexp p y.
A: Type
a: A
p: a = a
x, y: Int
loopexp p (x + y) = loopexp p x @ loopexp p y
Proof.
A: Type
a: A
p: a = a
x, y: Int
loopexp p (x + y) = loopexp p x @ loopexp p y
  revert x.
A: Type
a: A
p: a = a
y: Int
forall x : Int, loopexp p (x + y) = loopexp p x @ loopexp p y
  rapply (int_homotopic (equiv_concat_r p a)); cbn beta.
A: Type
a: A
p: a = a
y: Int
loopexp p (0 + y) = loopexp p 0 @ loopexp p y
A: Type
a: A
p: a = a
y: Int
(fun x : Int => loopexp p (x.+1 + y)) ==
(fun x : Int => equiv_concat_r p a (loopexp p (x + y)))
A: Type
a: A
p: a = a
y: Int
(fun x : Int => loopexp p x.+1 @ loopexp p y) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ loopexp p y))
  -
A: Type
a: A
p: a = a
y: Int
loopexp p (0 + y) = loopexp p 0 @ loopexp p y symmetry; apply concat_1p.
  -
A: Type
a: A
p: a = a
y: Int
(fun x : Int => loopexp p (x.+1 + y)) ==
(fun x : Int => equiv_concat_r p a (loopexp p (x + y))) reflexivity.
  -
A: Type
a: A
p: a = a
y: Int
(fun x : Int => loopexp p x.+1 @ loopexp p y) ==
(fun x : Int => equiv_concat_r p a (loopexp p x @ loopexp p y)) intro z; simpl.
A: Type
a: A
p: a = a
y, z: Int
(loopexp p z @ p) @ loopexp p y = (loopexp p z @ loopexp p y) @ p
    rewrite 2 concat_pp_p.
A: Type
a: A
p: a = a
y, z: Int
loopexp p z @ (p @ loopexp p y) = loopexp p z @ (loopexp p y @ p)
    by rewrite <- loopexp_succ_l.
Defined.

(** Under univalence, exponentiation of loops corresponds to iteration of auto-equivalences. *)

Definition equiv_path_loopexp {A : Type} (p : A = A) (z : Int) (a : A)
  : equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a.
A: Type
p: A = A
z: Int
a: A
equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a
Proof.
A: Type
p: A = A
z: Int
a: A
equiv_path A A (loopexp p z) a = int_iter (equiv_path A A p) z a
  apply int_iter_commute_map with (g:=fun p => equiv_path A A p a).
A: Type
p: A = A
z: Int
a: A
(fun x : A = A => equiv_path A A (equiv_concat_r p A x) a) ==
(fun x : A = A => equiv_path A A p (equiv_path A A x a))
  intro q; cbn.
A: Type
p: A = A
z: Int
a: A
q: A = A
transport idmap (q @ p) a = transport idmap p (transport idmap q a)
  napply transport_pp.
Defined.

Definition loopexp_path_universe `{Univalence} {A : Type} (f : A <~> A)
  (z : Int) (a : A)
  : transport idmap (loopexp (path_universe f) z) a = int_iter f z a.
H: Univalence
A: Type
f: A <~> A
z: Int
a: A
transport idmap (loopexp (path_universe f) z) a = int_iter f z a
Proof.
H: Univalence
A: Type
f: A <~> A
z: Int
a: A
transport idmap (loopexp (path_universe f) z) a = int_iter f z a
  revert f; equiv_intro (equiv_path A A) p.
H: Univalence
A: Type
z: Int
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
int_iter (equiv_path A A p) z a
  rhs_V napply equiv_path_loopexp.
H: Univalence
A: Type
z: Int
a: A
p: A = A
transport idmap (loopexp (path_universe (equiv_path A A p)) z) a =
equiv_path A A (loopexp p z) a
  nrefine (ap (fun q => equiv_path A A (loopexp q z) a) _).
H: Univalence
A: Type
z: Int
a: A
p: A = A
path_universe (equiv_path A A p) = p
  apply eissect.
Defined.

(** ** Converting between integers and naturals *)

(** We can convert a [nat] to an [Int] by mapping [0] to [zero] and [S n] to [int_succ n].  Various operations on [nat] are preserved by this function.  We will make this into a coercion later; we delay doing so to ensure that the lemmas about [int_of_nat] are interpreted as we want them to be. *)
Definition int_of_nat (n : nat) : Int
  := nat_iter n int_succ zero.

(** [int_of_nat] preserves zero. *)
Definition int_of_nat_zero : int_of_nat 0 = 0
  := idpath.

(** [int_of_nat] preserves successors. *)
Definition int_of_nat_succ (n : nat)
  : int_of_nat (n.+1) = (int_of_nat n).+1
  := idpath.

(** [int_of_nat] preserves predecessors of positive naturals. *)
Definition int_of_nat_pred (n : nat) (npos : (0 < n)%nat)
  : int_of_nat (nat_pred n) = (int_of_nat n).-1.
n: nat
npos: (0 < n)%nat
int_of_nat (nat_pred n) = (int_of_nat n).-1
Proof.
n: nat
npos: (0 < n)%nat
int_of_nat (nat_pred n) = (int_of_nat n).-1
  rhs_V napply (ap (fun _ => _.-1) (nat_succ_pred n npos)).
n: nat
npos: (0 < n)%nat
int_of_nat (nat_pred n) = (int_of_nat (nat_pred n).+1).-1
  simpl; symmetry.
n: nat
npos: (0 < n)%nat
(int_of_nat (nat_pred n)).+1.-1 = int_of_nat (nat_pred n)
  apply int_pred_succ.
Defined.

(** [int_of_nat] preserves addition. *)
Definition int_of_nat_add (n m : nat)
  : int_of_nat (n + m) = int_of_nat n + int_of_nat m.
n, m: nat
int_of_nat (n + m) = int_of_nat n + int_of_nat m
Proof.
n, m: nat
int_of_nat (n + m) = int_of_nat n + int_of_nat m
  induction n as [|n IHn].
m: nat
int_of_nat (0 + m) = int_of_nat 0 + int_of_nat m
n, m: nat
IHn: int_of_nat (n + m) = int_of_nat n + int_of_nat m
int_of_nat (n.+1 + m) = int_of_nat n.+1 + int_of_nat m
  -
m: nat
int_of_nat (0 + m) = int_of_nat 0 + int_of_nat m reflexivity.
  -
n, m: nat
IHn: int_of_nat (n + m) = int_of_nat n + int_of_nat m
int_of_nat (n.+1 + m) = int_of_nat n.+1 + int_of_nat m exact (ap _ IHn).
Defined.

(** [int_of_nat] preserves subtraction when not truncated. *)
Definition int_of_nat_sub (n m : nat) (ngeq : (m <= n)%nat)
  : int_of_nat (n - m) = int_of_nat n - int_of_nat m.
n, m: nat
ngeq: (m <= n)%nat
int_of_nat (n - m) = int_of_nat n - int_of_nat m
Proof.
n, m: nat
ngeq: (m <= n)%nat
int_of_nat (n - m) = int_of_nat n - int_of_nat m
  induction ngeq as [|n H IHn].
m: nat
int_of_nat (m - m) = int_of_nat m + - int_of_nat m
m, n: nat
H: (m <= n)%nat
IHn: int_of_nat (n - m) = int_of_nat n + - int_of_nat m
int_of_nat (n.+1 - m) = int_of_nat n.+1 + - int_of_nat m
  -
m: nat
int_of_nat (m - m) = int_of_nat m + - int_of_nat m rhs napply int_add_neg_r.
m: nat
int_of_nat (m - m) = 0
    by rewrite nat_sub_cancel.
  -
m, n: nat
H: (m <= n)%nat
IHn: int_of_nat (n - m) = int_of_nat n + - int_of_nat m
int_of_nat (n.+1 - m) = int_of_nat n.+1 + - int_of_nat m rewrite nat_sub_succ_l; only 2: exact _; simpl.
m, n: nat
H: (m <= n)%nat
IHn: int_of_nat (n - m) = int_of_nat n + - int_of_nat m
(int_of_nat (n - m)).+1 = (int_of_nat n + - int_of_nat m).+1
    exact (ap _ IHn).
Defined.

(** [int_of_nat] preserves multiplication. This makes [int_of_nat] a semiring homomorphism. *)
Definition int_of_nat_mul (n m : nat)
  : int_of_nat (n * m) = int_of_nat n * int_of_nat m.
n, m: nat
int_of_nat (n * m) = int_of_nat n * int_of_nat m
Proof.
n, m: nat
int_of_nat (n * m) = int_of_nat n * int_of_nat m
  induction n as [|n IHn].
m: nat
int_of_nat (0 * m) = int_of_nat 0 * int_of_nat m
n, m: nat
IHn: int_of_nat (n * m) = int_of_nat n * int_of_nat m
int_of_nat (n.+1 * m) = int_of_nat n.+1 * int_of_nat m
  -
m: nat
int_of_nat (0 * m) = int_of_nat 0 * int_of_nat m reflexivity.
  -
n, m: nat
IHn: int_of_nat (n * m) = int_of_nat n * int_of_nat m
int_of_nat (n.+1 * m) = int_of_nat n.+1 * int_of_nat m simpl; rewrite <- IHn.
n, m: nat
IHn: int_of_nat (n * m) = int_of_nat n * int_of_nat m
int_of_nat (m + n * m) = int_of_nat (n * m) + int_of_nat m
    rhs_V napply int_of_nat_add.
n, m: nat
IHn: int_of_nat (n * m) = int_of_nat n * int_of_nat m
int_of_nat (m + n * m) = int_of_nat (n * m + m)
    by rewrite nat_add_comm.
Defined.

Coercion int_of_nat : nat >-> Int.