Timings for Int.v
Require Import Basics.Overture Basics.Nat Basics.Tactics Basics.Decidable Basics.Equivalences Basics.PathGroupoids Types.Paths Types.Universe.
Require Basics.Numerals.Decimal.
Require Import Spaces.Nat.Core.
Unset Elimination Schemes.
Set Universe Minimization ToSet.
Delimit Scope int_scope with int.
Local Open Scope int_scope.
(** * The Integers *)
(** ** Definition *)
(** We define the integers as two copies of [nat] stuck together around a [zero]. *)
Inductive Int : Type0 :=
| negS : nat -> Int
| zero : Int
| posS : nat -> Int.
(** We can convert a [nat] to an [Int] by mapping [0] to [zero] and [S n] to [posS n]. Various operations on [nat] are preserved by this function. See the section on conversion functions starting with [int_nat_succ]. *)
Definition int_of_nat (n : nat) :=
match n with
| O => zero
| S n => posS n
end.
(** We declare this conversion as a coercion so we can freely use [nat]s in statements about integers. *)
Coercion int_of_nat : nat >-> Int.
(** ** Number Notations *)
(** Here we define some printing and parsing functions that convert the integers between numeral representations so that we can use notations such as [123] for [posS 122] and [-123] for [negS 122]. *)
(** Printing *)
Definition int_to_number_int (n : Int) : Numeral.int :=
match n with
| posS n => Numeral.IntDec (Decimal.Pos (Nat.to_uint (S n)))
| zero => Numeral.IntDec (Decimal.Pos (Nat.to_uint 0))
| negS n => Numeral.IntDec (Decimal.Neg (Nat.to_uint (S n)))
end.
Definition int_of_number_int (d : Numeral.int) :=
match d with
| Numeral.IntDec (Decimal.Pos d) => int_of_nat (Nat.of_uint d)
| Numeral.IntDec (Decimal.Neg d) => negS (nat_pred (Nat.of_uint d))
| Numeral.IntHex (Hexadecimal.Pos u) => int_of_nat (Nat.of_hex_uint u)
| Numeral.IntHex (Hexadecimal.Neg u) => negS (nat_pred (Nat.of_hex_uint u))
end.
Number Notation Int int_of_number_int int_to_number_int : int_scope.
(** ** Successor, Predecessor and Negation *)
(** These operations will be used in the induction principle we derive for [Int] so we need to define them early on. *)
(** *** Successor and Predecessor *)
Definition int_succ (n : Int) : Int :=
match n with
| posS n => posS (S n)
| 0 => 1
| -1 => 0
| negS (S n) => negS n
end.
Notation "n .+1" := (int_succ n) : int_scope.
Definition int_pred (n : Int) : Int :=
match n with
| posS (S n) => posS n
| 1 => 0
| 0 => -1
| negS n => negS (S n)
end.
Notation "n .-1" := (int_pred n) : int_scope.
Definition int_neg@{} (x : Int) : Int :=
match x with
| posS x => negS x
| zero => zero
| negS x => posS x
end.
Notation "- x" := (int_neg x) : int_scope.
(** ** Basic Properties *)
(** *** Integer induction *)
(** The induction principle for integers is similar to the induction principle for natural numbers. However we have two induction hypotheses going in either direction starting from 0. *)
Definition Int_ind@{i} (P : Int -> Type@{i})
(H0 : P 0)
(HP : forall n : nat, P n -> P (int_succ n))
(HN : forall n : nat, P (- n) -> P (int_pred (-n)))
: forall x, P x.
apply (HN x.+1%nat), IHx.
apply (HP x.+1%nat), IHx.
(** We record these so that they can be used with the [induction] tactic. *)
Definition Int_rect := Int_ind.
Definition Int_rec := Int_ind.
(** *** Decidable Equality *)
(** The integers have decidable equality. *)
Instance decidable_paths_int@{} : DecidablePaths Int.
destruct x as [x | | x], y as [y | | y].
2-4,6-8: right; intros; discriminate.
1,2: napply decidable_iff.
1,2: intros H; by injection H.
(** By Hedberg's theorem, we have that the integers are a set. *)
Instance ishset_int@{} : IsHSet Int := _.
(** *** Pointedness *)
(** We sometimes want to treat the integers as a pointed type with basepoint given by 0. *)
Instance ispointed_int : IsPointed Int := 0.
(** ** Operations *)
(** *** Addition *)
(** Addition for integers is defined by integer induction on the first argument. *)
Definition int_add@{} (x y : Int) : Int.
induction x as [|x IHx|x IHx] in y |- *.
(** [x.+1 + y = (x + y).+1] *)
exact (int_succ (IHx y)).
(** [x.-1 + y = (x + y).-1] *)
exact (int_pred (IHx y)).
Infix "+" := int_add : int_scope.
Infix "-" := (fun x y => x + -y) : int_scope.
(** *** Multiplication *)
(** Multiplication for integers is defined by integer induction on the first argument. *)
Definition int_mul@{} (x y : Int) : Int.
induction x as [|x IHx|x IHx] in y |- *.
(** [x.+1 * y = y + x * y] *)
(** [x.-1 * y = -y + x * y] *)
Infix "*" := int_mul : int_scope.
(** ** Properties of Operations *)
(** *** Negation *)
(** Negation is involutive. *)
Definition int_neg_neg@{} (x : Int) : - - x = x.
(** Negation is an equivalence. *)
Instance isequiv_int_neg@{} : IsEquiv int_neg.
snapply (isequiv_adjointify int_neg int_neg).
(** 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 (x : Int) : - x.+1 = (- x).-1.
by destruct x as [[] | | ].
(** The negation of a predecessor is the successor of the negation. *)
Definition int_neg_pred (x : Int) : - x.-1 = (- x).+1.
by destruct x as [ | | []].
(** The successor of a predecessor is the identity. *)
Definition int_pred_succ@{} (x : Int) : x.-1.+1 = x.
by destruct x as [ | | []].
(** The predecessor of a successor is the identity. *)
Definition int_succ_pred@{} (x : Int) : x.+1.-1 = x.
by destruct x as [[] | | ].
(** The successor is an equivalence on [Int] *)
Instance isequiv_int_succ@{} : IsEquiv int_succ
:= isequiv_adjointify int_succ int_pred int_pred_succ int_succ_pred.
(** The predecessor is an equivalence on [Int] *)
Instance isequiv_int_pred@{} : IsEquiv int_pred
:= isequiv_inverse int_succ.
(** *** Addition *)
(** Integer addition with zero on the left is the identity by definition. *)
Definition int_add_0_l@{} (x : Int) : 0 + x = x := 1.
(** Integer addition with zero on the right is the identity. *)
Definition int_add_0_r@{} (x : Int) : x + 0 = x.
induction x as [|[|x] IHx|[|x] IHx].
change (?z.+1 + 0) with (z + 0).+1.
change (?z.-1 + 0) with (z + 0).-1.
(** 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.
induction x as [|[|x] IHx|[|x] IHx] in y |- *.
all: symmetry; apply int_pred_succ.
(** 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.
induction x as [|[|x] IHx|[|x] IHx] in y |- *.
all: symmetry; apply int_succ_pred.
(** 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.
induction x as [|x IHx|[] IHx] in y |- *.
by rewrite 2 int_add_succ_l, IHx.
cbn; by rewrite int_succ_pred, int_pred_succ.
change ((- (n.+1%nat)).-1 + y.+1 = ((- (n.+1%nat)).-1 + y).+1).
rewrite <- 2 int_add_succ_l.
rewrite <- int_add_pred_l.
by rewrite int_pred_succ, int_succ_pred.
(** 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.
induction x as [|x IHx|[] IHx] in y |- *.
rewrite 2 int_add_succ_l.
by rewrite int_pred_succ, int_succ_pred.
rewrite 2 int_add_pred_l.
(** Integer addition is commutative. *)
Definition int_add_comm@{} (x y : Int) : x + y = y + x.
induction y as [|y IHy|y IHy] in x |- *.
by rewrite int_add_succ_r.
(** Integer addition is associative. *)
Definition int_add_assoc@{} (x y z : Int) : x + (y + z) = x + y + z.
induction x as [|x IHx|x IHx] in y, z |- *.
by rewrite !int_add_succ_l, IHx.
by rewrite !int_add_pred_l, IHx.
(** Negation is a left inverse with respect to integer addition. *)
Definition int_add_neg_l@{} (x : Int) : - x + x = 0.
induction x as [|x IHx|x IHx].
by rewrite int_neg_succ, int_add_pred_l, int_add_succ_r, IHx.
by rewrite int_neg_pred, int_add_succ_l, int_add_pred_r, IHx.
(** Negation is a right inverse with respect to integer addition. *)
Definition int_add_neg_r@{} (x : Int) : x - x = 0.
unfold "-"; by rewrite int_add_comm, int_add_neg_l.
(** Negation distributes over addition. *)
Definition int_neg_add@{} (x y : Int) : - (x + y) = - x - y.
induction x as [|x IHx|x IHx] in y |- *.
(** *** Multiplication *)
(** Multiplication with a successor on the left is the sum of the multiplication without the successor and the multiplicand which was not a successor. *)
Definition int_mul_succ_l@{} (x y : Int) : x.+1 * y = y + x * y.
induction x as [|[|x] IHx|[] IHx] in y |- *.
by rewrite int_add_neg_r.
(** Similarly, multiplication with a predecessor on the left is the sum of the multiplication without the predecessor and the negation of the multiplicand which was not a predecessor. *)
Definition int_mul_pred_l@{} (x y : Int) : x.-1 * y = -y + x * y.
induction x as [|x IHx|[] IHx] in y |- *.
by rewrite int_add_neg_l.
(** Integer multiplication with zero on the left is zero by definition. *)
Definition int_mul_0_l@{} (x : Int) : 0 * x = 0 := 1.
(** Integer multiplication with zero on the right is zero. *)
Definition int_mul_0_r@{} (x : Int) : x * 0 = 0.
induction x as [|x IHx|x IHx].
by rewrite int_mul_succ_l, int_add_0_l.
by rewrite int_mul_pred_l, int_add_0_l.
(** Integer multiplication with one on the left is the identity. *)
Definition int_mul_1_l@{} (x : Int) : 1 * x = x.
(** Integer multiplication with one on the right is the identity. *)
Definition int_mul_1_r@{} (x : Int) : x * 1 = x.
induction x as [|x IHx|x IHx].
by rewrite int_mul_succ_l, IHx.
by rewrite int_mul_pred_l, IHx.
(** 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).
induction x as [|x IHx|x IHx] in y |- *.
(** Multiplying with a successor on the right is the sum of the multiplication without the successor and the product of the multiplicand which was not a successor and the multiplicand. *)
Definition int_mul_succ_r@{} (x y : Int) : x * y.+1 = x + x * y.
induction x as [|x IHx|x IHx] in y |- *.
rewrite 2 int_mul_succ_l.
rewrite 2 int_add_succ_l.
rewrite !int_add_assoc; f_ap.
rewrite 2 int_mul_pred_l.
rewrite 2 int_add_pred_l.
rewrite <- int_mul_neg_l.
rewrite !int_add_assoc; f_ap.
(** Multiplying with a predecessor on the right is the sum of the multiplication without the predecessor and the product of the multiplicand which was not a predecessor and the negation of the multiplicand which was not a predecessor. *)
Definition int_mul_pred_r@{} (x y : Int) : x * y.-1 = -x + x * y.
induction x as [|x IHx|x IHx] in y |- *.
rewrite 2 int_mul_succ_l.
rewrite !int_add_assoc; f_ap.
rewrite <- (int_neg_neg y.-1).
rewrite <- int_add_succ_l.
rewrite 2 int_mul_pred_l.
rewrite !int_add_assoc; f_ap.
rewrite 2 int_add_succ_l; f_ap.
(** Integer multiplication is commutative. *)
Definition int_mul_comm@{} (x y : Int) : x * y = y * x.
induction y as [|y IHy|y IHy] in x |- *.
(** 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).
rewrite !(int_mul_comm x).
(** Multiplication distributes over addition on the left. *)
Definition int_dist_l@{} (x y z : Int) : x * (y + z) = x * y + x * z.
induction x as [|x IHx|x IHx] in y, z |- *.
rewrite 3 int_mul_succ_l.
rewrite !int_add_assoc; f_ap.
rewrite <- !int_add_assoc; f_ap.
rewrite 3 int_mul_pred_l.
rewrite !int_add_assoc; f_ap.
rewrite <- !int_add_assoc; f_ap.
(** Multiplication distributes over addition on the right. *)
Definition int_dist_r@{} (x y z : Int) : (x + y) * z = x * z + y * z.
by rewrite int_mul_comm, int_dist_l, !(int_mul_comm z).
(** Multiplication is associative. *)
Definition int_mul_assoc@{} (x y z : Int) : x * (y * z) = x * y * z.
induction x as [|x IHx|x IHx] in y, z |- *.
rewrite 2 int_mul_succ_l.
rewrite 2 int_mul_pred_l.
rewrite <- int_mul_neg_l.
(** ** Iteration of equivalences *)
(** *** Iteration by arbitrary integers *)
(** Iteration by arbitrary integers requires the endofunction to be an equivalence, so that we can define a negative iteration by using its inverse. *)
Definition int_iter {A} (f : A -> A) `{!IsEquiv f} (n : Int) : A -> A
:= match n with
| negS n => fun x => nat_iter n.+1%nat f^-1 x
| zero => idmap
| posS n => fun x => nat_iter n.+1%nat f x
end.
Definition int_iter_neg {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
: int_iter f (- n) a = int_iter f^-1 n a.
Definition int_iter_succ_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
: int_iter f (int_succ n) a = f (int_iter f n a).
all: symmetry; apply eisretr.
Definition int_iter_succ_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
: int_iter f (int_succ n) a = int_iter f n (f a).
1: symmetry; apply eissect.
Definition int_iter_pred_l {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
: int_iter f (int_pred n) a = f^-1 (int_iter f n a).
(* Convert the problem to be a problem about [f^-1] and [-n]. *)
lhs_V exact (int_iter_neg f^-1 (n.-1) a).
rhs_V exact (ap f^-1 (int_iter_neg f^-1 n a)).
(* Then [int_iter_succ_l] applies, after changing [- n.-1] to [(-n).+1]. *)
Definition int_iter_pred_r {A} (f : A -> A) `{IsEquiv _ _ f} (n : Int) (a : A)
: int_iter f (int_pred n) a = int_iter f n (f^-1 a).
(* Convert the problem to be a problem about [f^-1] and [-n]. *)
lhs_V exact (int_iter_neg f^-1 (n.-1) a).
rhs_V exact (int_iter_neg f^-1 n (f^-1 a)).
(* Then [int_iter_succ_r] applies, after changing [- n.-1] to [(-n).+1]. *)
Definition int_iter_add {A} (f : A -> A) `{IsEquiv _ _ f} (m n : Int)
: int_iter f (m + n) == int_iter f m o int_iter f n.
rewrite 2 int_iter_succ_l.
rewrite 2 int_iter_pred_l.
(** 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) (n : Int) (a : A)
: g (int_iter f n a) = int_iter f' n (g a).
induction n as [|n IHn|n IHn] in a |- *.
rewrite 2 int_iter_succ_r.
rewrite 2 int_iter_pred_r.
(** In particular, homotopic maps have homotopic iterations. *)
Definition int_iter_homotopic (n : Int) {A} (f f' : A -> A) `{!IsEquiv f} `{!IsEquiv f'}
(h : f == f')
: int_iter f n == int_iter f' n
:= int_iter_commute_map f f' idmap h n.
(** [int_iter f n x] doesn't depend on the proof that [f] is an equivalence. *)
Definition int_iter_agree (n : Int) {A} (f : A -> A) {ief ief' : IsEquiv f}
: forall x, @int_iter A f ief n x = @int_iter A f ief' n x
:= int_iter_homotopic n f f (fun _ => idpath).
Definition int_iter_invariant (n : Int) {A} (f : A -> A) `{!IsEquiv f}
(P : A -> Type)
(Psucc : forall x, P x -> P (f x))
(Ppred : forall x, P x -> P (f^-1 x))
: forall x, P x -> P (int_iter f n x).
induction n as [|n IHn|n IHn]; intro x.
(** ** Exponentiation of loops *)
Definition loopexp {A : Type} {x : A} (p : x = x) (z : Int) : (x = x)
:= int_iter (equiv_concat_r p x) z idpath.
Definition loopexp_succ_r {A : Type} {x : A} (p : x = x) (z : Int)
: loopexp p z.+1 = loopexp p z @ p
:= int_iter_succ_l _ _ _.
Definition loopexp_pred_r {A : Type} {x : A} (p : x = x) (z : Int)
: loopexp p z.-1 = loopexp p z @ p^
:= int_iter_pred_l _ _ _.
Definition loopexp_succ_l {A : Type} {x : A} (p : x = x) (z : Int)
: loopexp p z.+1 = p @ loopexp p z.
lhs napply loopexp_succ_r.
Definition loopexp_pred_l {A : Type} {x : A} (p : x = x) (z : Int)
: loopexp p z.-1 = p^ @ loopexp p z.
exact (concat_1p _ @ (concat_p1 _)^).
Definition ap_loopexp {A B} (f : A -> B) {x : A} (p : x = x) (z : Int)
: ap f (loopexp p z) = loopexp (ap f p) z.
napply int_iter_commute_map.
Definition loopexp_add {A : Type} {x : A} (p : x = x) m n
: loopexp p (m + n) = loopexp p m @ loopexp p n.
symmetry; apply concat_1p.
rewrite 2 loopexp_succ_l.
by rewrite IHm, concat_p_pp.
rewrite 2 loopexp_pred_l.
by rewrite IHm, concat_p_pp.
(** 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.
refine (int_iter_commute_map _ _ (fun p => equiv_path A A p a) _ _ _).
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.
equiv_intro (equiv_path A A) p.
refine (_ @ equiv_path_loopexp p z a).
refine (ap (fun q => equiv_path A A (loopexp q z) a) _).
(** ** Converting between integers and naturals *)
(** [int_of_nat] preserves successors. *)
Definition int_nat_succ (n : nat)
: (n.+1)%int = (n.+1)%nat :> Int.
(** [int_of_nat] preserves addition. Hence is a monoid homomorphism. *)
Definition int_nat_add (n m : nat)
: (n + m)%int = (n + m)%nat :> Int.
rewrite <- 2 int_nat_succ.
(** [int_of_nat] preserves subtraction when not truncated. *)
Definition int_nat_sub (n m : nat)
: (m <= n)%nat -> (n - m)%int = (n - m)%nat :> Int.
induction H as [|n H IHn].
lhs napply int_add_neg_r.
by rewrite nat_sub_cancel.
rewrite nat_sub_succ_l; only 2: exact _.
rewrite <- 2 int_nat_succ.
(** [int_of_nat] preserves multiplication. This makes [int_of_nat] a semiring homomorphism. *)
Definition int_nat_mul (n m : nat)
: (n * m)%int = (n * m)%nat :> Int.
rhs_V napply int_nat_add.