diff --git a/hott/algebra/algebra.md b/hott/algebra/algebra.md index f1d2f04f2..d212b8548 100644 --- a/hott/algebra/algebra.md +++ b/hott/algebra/algebra.md @@ -15,13 +15,16 @@ The following files are [ported](../port.md) from the standard library. If anyth * [field](field.hlean) * [ordered_field](ordered_field.hlean) * [bundled](bundled.hlean) : bundled versions of the algebraic structures +* [homomorphism](homomorphism.hlean) +* [group_power](group_power.lean) (depends on files in [nat](../types/nat/nat.md) and [int](../types/int/int.md)) Files which are not ported from the standard library: +* [inf_group](inf_group.hlean) : algebraic structures which are not assumes to be sets. No higher coherences are assumed. Truncated algebraic structures extend these structures with the assumption that they are sets. * [group_theory](group_theory.hlean) : Basic theorems about group homomorphisms and isomorphisms * [trunc_group](trunc_group.hlean) : truncate an infinity-group to a group * [homotopy_group](homotopy_group.hlean) : homotopy groups of a pointed type -* [e_closure](e_closure.hlean) : the type of words formed by a relation +* [e_closure](e_closure.hlean) : the type of words formed by a relation, or paths in a graph. * [graph](graph.hlean) : definition and operations on paths in a graph. Subfolders (not ported): diff --git a/hott/algebra/group_power.hlean b/hott/algebra/group_power.hlean new file mode 100644 index 000000000..1fb914fab --- /dev/null +++ b/hott/algebra/group_power.hlean @@ -0,0 +1,264 @@ +/- +Copyright (c) 2015 Jeremy Avigad. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: Jeremy Avigad + +The power operation on monoids prod groups. We separate this from group, because it depends on +nat, which in turn depends on other parts of algebra. + +We have "pow a n" for natural number powers, prod "gpow a i" for integer powers. The notation +a^n is used for the first, but users can locally redefine it to gpow when needed. + +Note: power adopts the convention that 0^0=1. +-/ +import types.nat.basic types.int.basic +open algebra + +variables {A : Type} + +structure has_pow_nat [class] (A : Type) := +(pow_nat : A → nat → A) + +definition pow_nat {A : Type} [s : has_pow_nat A] : A → nat → A := +has_pow_nat.pow_nat + +infix ` ^ ` := pow_nat + +structure has_pow_int [class] (A : Type) := +(pow_int : A → int → A) + +definition pow_int {A : Type} [s : has_pow_int A] : A → int → A := +has_pow_int.pow_int + + /- monoid -/ +section monoid +open nat + +variable [s : monoid A] +include s + +definition monoid.pow (a : A) : ℕ → A +| 0 := 1 +| (n+1) := a * monoid.pow n + +definition monoid_has_pow_nat [instance] : has_pow_nat A := +has_pow_nat.mk monoid.pow + +theorem pow_zero (a : A) : a^0 = 1 := rfl +theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a * a^n := rfl + +theorem pow_one (a : A) : a^1 = a := !mul_one +theorem pow_two (a : A) : a^2 = a * a := +calc + a^2 = a * (a * 1) : rfl + ... = a * a : mul_one +theorem pow_three (a : A) : a^3 = a * (a * a) := +calc + a^3 = a * (a * (a * 1)) : rfl + ... = a * (a * a) : mul_one +theorem pow_four (a : A) : a^4 = a * (a * (a * a)) := +calc + a^4 = a * a^3 : rfl + ... = a * (a * (a * a)) : pow_three + +theorem pow_succ' (a : A) : Πn, a^(succ n) = a^n * a +| 0 := by rewrite [pow_succ, *pow_zero, one_mul, mul_one] +| (succ n) := by rewrite [pow_succ, pow_succ' at {1}, pow_succ, mul.assoc] + +theorem one_pow : Π n : ℕ, 1^n = (1:A) +| 0 := rfl +| (succ n) := by rewrite [pow_succ, one_mul, one_pow] + +theorem pow_add (a : A) (m n : ℕ) : a^(m + n) = a^m * a^n := +begin + induction n with n ih, + {krewrite [nat.add_zero, pow_zero, mul_one]}, + rewrite [add_succ, *pow_succ', ih, mul.assoc] +end + +theorem pow_mul (a : A) (m : ℕ) : Π n, a^(m * n) = (a^m)^n +| 0 := by rewrite [nat.mul_zero, pow_zero] +| (succ n) := by rewrite [nat.mul_succ, pow_add, pow_succ', pow_mul] + +theorem pow_comm (a : A) (m n : ℕ) : a^m * a^n = a^n * a^m := +by rewrite [-*pow_add, add.comm] + +end monoid + +/- commutative monoid -/ + +section comm_monoid +open nat +variable [s : comm_monoid A] +include s + +theorem mul_pow (a b : A) : Π n, (a * b)^n = a^n * b^n +| 0 := by rewrite [*pow_zero, mul_one] +| (succ n) := by rewrite [*pow_succ', mul_pow, *mul.assoc, mul.left_comm a] + +end comm_monoid + +section group +variable [s : group A] +include s + +section nat +open nat +theorem inv_pow (a : A) : Πn, (a⁻¹)^n = (a^n)⁻¹ +| 0 := by rewrite [*pow_zero, one_inv] +| (succ n) := by rewrite [pow_succ, pow_succ', inv_pow, mul_inv] + +theorem pow_sub (a : A) {m n : ℕ} (H : m ≥ n) : a^(m - n) = a^m * (a^n)⁻¹ := +have H1 : m - n + n = m, from nat.sub_add_cancel H, +have H2 : a^(m - n) * a^n = a^m, by rewrite [-pow_add, H1], +eq_mul_inv_of_mul_eq H2 + +theorem pow_inv_comm (a : A) : Πm n, (a⁻¹)^m * a^n = a^n * (a⁻¹)^m +| 0 n := by rewrite [*pow_zero, one_mul, mul_one] +| m 0 := by rewrite [*pow_zero, one_mul, mul_one] +| (succ m) (succ n) := by rewrite [pow_succ' at {1}, pow_succ at {1}, pow_succ', pow_succ, + *mul.assoc, inv_mul_cancel_left, mul_inv_cancel_left, pow_inv_comm] + +end nat + +open int + +definition gpow (a : A) : ℤ → A +| (of_nat n) := a^n +| -[1+n] := (a^(nat.succ n))⁻¹ + +open nat + +private lemma gpow_add_aux (a : A) (m n : nat) : + gpow a ((of_nat m) + -[1+n]) = gpow a (of_nat m) * gpow a (-[1+n]) := +sum.elim (nat.lt_sum_ge m (nat.succ n)) + (assume H : (m < nat.succ n), + have H1 : (#nat nat.succ n - m > nat.zero), from nat.sub_pos_of_lt H, + calc + gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n)) : rfl + ... = gpow a (-[1+ nat.pred (nat.sub (nat.succ n) m)]) : {sub_nat_nat_of_lt H} + ... = (a ^ (nat.succ (nat.pred (nat.sub (nat.succ n) m))))⁻¹ : rfl + ... = (a ^ (nat.succ n) * (a ^ m)⁻¹)⁻¹ : + by krewrite [succ_pred_of_pos H1, pow_sub a (nat.le_of_lt H)] + ... = a ^ m * (a ^ (nat.succ n))⁻¹ : + by rewrite [mul_inv, inv_inv] + ... = gpow a (of_nat m) * gpow a (-[1+n]) : rfl) + (assume H : (m ≥ nat.succ n), + calc + gpow a ((of_nat m) + -[1+n]) = gpow a (sub_nat_nat m (nat.succ n)) : rfl + ... = gpow a (#nat m - nat.succ n) : {sub_nat_nat_of_ge H} + ... = a ^ m * (a ^ (nat.succ n))⁻¹ : pow_sub a H + ... = gpow a (of_nat m) * gpow a (-[1+n]) : rfl) + +theorem gpow_add (a : A) : Πi j : int, gpow a (i + j) = gpow a i * gpow a j +| (of_nat m) (of_nat n) := !pow_add +| (of_nat m) -[1+n] := !gpow_add_aux +| -[1+m] (of_nat n) := by rewrite [add.comm, gpow_add_aux, ↑gpow, -*inv_pow, pow_inv_comm] +| -[1+m] -[1+n] := + calc + gpow a (-[1+m] + -[1+n]) = (a^(#nat nat.succ m + nat.succ n))⁻¹ : rfl + ... = (a^(nat.succ m))⁻¹ * (a^(nat.succ n))⁻¹ : by rewrite [pow_add, pow_comm, mul_inv] + ... = gpow a (-[1+m]) * gpow a (-[1+n]) : rfl + +theorem gpow_comm (a : A) (i j : ℤ) : gpow a i * gpow a j = gpow a j * gpow a i := +by rewrite [-*gpow_add, add.comm] +end group + +section ordered_ring +open nat +variable [s : linear_ordered_ring A] +include s + +theorem pow_pos {a : A} (H : a > 0) (n : ℕ) : a ^ n > 0 := + begin + induction n, + krewrite pow_zero, + apply zero_lt_one, + rewrite pow_succ', + apply mul_pos, + apply v_0, apply H + end + +theorem pow_ge_one_of_ge_one {a : A} (H : a ≥ 1) (n : ℕ) : a ^ n ≥ 1 := + begin + induction n, + krewrite pow_zero, + apply le.refl, + rewrite [pow_succ', -mul_one 1], + apply mul_le_mul v_0 H zero_le_one, + apply le_of_lt, + apply pow_pos, + apply gt_of_ge_of_gt H zero_lt_one + end + +theorem pow_two_add (n : ℕ) : (2:A)^n + 2^n = 2^(succ n) := + by rewrite [pow_succ', -one_add_one_eq_two, left_distrib, *mul_one] + +end ordered_ring + +/- additive monoid -/ + +section add_monoid +variable [s : add_monoid A] +include s +local attribute add_monoid.to_monoid [trans_instance] +open nat + +definition nmul : ℕ → A → A := λ n a, a^n + +infix [priority algebra.prio] `⬝` := nmul + +theorem zero_nmul (a : A) : (0:ℕ) ⬝ a = 0 := pow_zero a +theorem succ_nmul (n : ℕ) (a : A) : nmul (succ n) a = a + (nmul n a) := pow_succ a n + +theorem succ_nmul' (n : ℕ) (a : A) : succ n ⬝ a = nmul n a + a := pow_succ' a n + +theorem nmul_zero (n : ℕ) : n ⬝ 0 = (0:A) := one_pow n + +theorem one_nmul (a : A) : 1 ⬝ a = a := pow_one a + +theorem add_nmul (m n : ℕ) (a : A) : (m + n) ⬝ a = (m ⬝ a) + (n ⬝ a) := pow_add a m n + +theorem mul_nmul (m n : ℕ) (a : A) : (m * n) ⬝ a = m ⬝ (n ⬝ a) := eq.subst (mul.comm n m) (pow_mul a n m) + +theorem nmul_comm (m n : ℕ) (a : A) : (m ⬝ a) + (n ⬝ a) = (n ⬝ a) + (m ⬝ a) := pow_comm a m n + +end add_monoid + +/- additive commutative monoid -/ + +section add_comm_monoid +open nat +variable [s : add_comm_monoid A] +include s +local attribute add_comm_monoid.to_comm_monoid [trans_instance] + +theorem nmul_add (n : ℕ) (a b : A) : n ⬝ (a + b) = (n ⬝ a) + (n ⬝ b) := mul_pow a b n + +end add_comm_monoid + +section add_group +variable [s : add_group A] +include s +local attribute add_group.to_group [trans_instance] + +section nat +open nat +theorem nmul_neg (n : ℕ) (a : A) : n ⬝ (-a) = -(n ⬝ a) := inv_pow a n + +theorem sub_nmul {m n : ℕ} (a : A) (H : m ≥ n) : (m - n) ⬝ a = (m ⬝ a) + -(n ⬝ a) := pow_sub a H + +theorem nmul_neg_comm (m n : ℕ) (a : A) : (m ⬝ (-a)) + (n ⬝ a) = (n ⬝ a) + (m ⬝ (-a)) := pow_inv_comm a m n + +end nat + +open int + +definition imul : ℤ → A → A := λ i a, gpow a i + +theorem add_imul (i j : ℤ) (a : A) : imul (i + j) a = imul i a + imul j a := + gpow_add a i j + +theorem imul_comm (i j : ℤ) (a : A) : imul i a + imul j a = imul j a + imul i a := gpow_comm a i j + +end add_group diff --git a/hott/algebra/group_theory.hlean b/hott/algebra/group_theory.hlean index 152bb50ea..f32eb8a7a 100644 --- a/hott/algebra/group_theory.hlean +++ b/hott/algebra/group_theory.hlean @@ -351,9 +351,11 @@ namespace group /- the trivial group -/ open unit + --rename: group_unit definition trivial_group [constructor] : group unit := group.mk _ (λx y, star) (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp) + --rename trivial_group definition Trivial_group [constructor] : Group := Group.mk _ trivial_group diff --git a/hott/init/path.hlean b/hott/init/path.hlean index 333e381cb..408db14e6 100644 --- a/hott/init/path.hlean +++ b/hott/init/path.hlean @@ -22,11 +22,11 @@ namespace eq definition idpath [reducible] [constructor] (a : A) := refl a -- unbased path induction - definition rec' [reducible] [unfold 6] {P : Π (a b : A), (a = b) → Type} + definition rec_unbased [reducible] [unfold 6] {P : Π (a b : A), (a = b) → Type} (H : Π (a : A), P a a idp) {a b : A} (p : a = b) : P a b p := eq.rec (H a) p - definition rec_on' [reducible] [unfold 5] {P : Π (a b : A), (a = b) → Type} + definition rec_on_unbased [reducible] [unfold 5] {P : Π (a b : A), (a = b) → Type} {a b : A} (p : a = b) (H : Π (a : A), P a a idp) : P a b p := eq.rec (H a) p diff --git a/hott/types/int/default.hlean b/hott/types/int/default.hlean index 10147301e..dd18be80a 100644 --- a/hott/types/int/default.hlean +++ b/hott/types/int/default.hlean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Floris van Doorn -/ -import .basic .hott +import .basic .hott .order diff --git a/hott/types/int/int.md b/hott/types/int/int.md index 5fe34add5..cb307edab 100644 --- a/hott/types/int/int.md +++ b/hott/types/int/int.md @@ -4,4 +4,5 @@ types.int The integers. Note: most of these files are ported from the standard library. If anything needs to be changed, it is probably a good idea to change it in the standard library and then port the file again (see also [script/port.pl](../../../script/port.pl)). * [basic](basic.hlean) : the integers, with basic operations +* [order](order.hlean) : order on the integers * [hott](hott.hlean) : facts about the integers specific to the HoTT library diff --git a/hott/types/int/order.hlean b/hott/types/int/order.hlean new file mode 100644 index 000000000..8c05f9dc9 --- /dev/null +++ b/hott/types/int/order.hlean @@ -0,0 +1,438 @@ +/- +Copyright (c) 2014 Floris van Doorn. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Floris van Doorn, Jeremy Avigad + +The order relation on the integers. We show that int is an instance of linear_comm_ordered_ring +prod transfer the results. +-/ +import .basic algebra.ordered_ring +open nat decidable int unit algebra eq + +namespace int + +private definition nonneg (a : ℤ) : Type₀ := int.cases_on a (take n, unit) (take n, empty) +protected definition le (a b : ℤ) : Type₀ := nonneg (b - a) + +definition int_has_le [instance] [priority int.prio]: has_le int := +has_le.mk int.le + +protected definition lt (a b : ℤ) : Type₀ := (a + 1) ≤ b + +definition int_has_lt [instance] [priority int.prio]: has_lt int := +has_lt.mk int.lt + +local attribute nonneg [reducible] +private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _ +definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _ +definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _ + +private theorem nonneg.elim {a : ℤ} : nonneg a → Σn : ℕ, a = n := +int.cases_on a (take n H, sigma.mk n rfl) (take n', empty.elim) + +private theorem nonneg_sum_nonneg_neg (a : ℤ) : nonneg a ⊎ nonneg (-a) := +int.cases_on a (take n, sum.inl star) (take n, sum.inr star) + +theorem le.intro {a b : ℤ} {n : ℕ} (H : a + n = b) : a ≤ b := +have n = b - a, from eq_add_neg_of_add_eq (begin rewrite [add.comm, H] end), -- !add.comm ▸ H), +show nonneg (b - a), from this ▸ star + +theorem le.elim {a b : ℤ} (H : a ≤ b) : Σn : ℕ, a + n = b := +obtain (n : ℕ) (H1 : b - a = n), from nonneg.elim H, +sigma.mk n (!add.comm ▸ iff.mpr !add_eq_iff_eq_add_neg (H1⁻¹)) + +protected theorem le_total (a b : ℤ) : a ≤ b ⊎ b ≤ a := +sum.imp_right + (assume H : nonneg (-(b - a)), + have -(b - a) = a - b, from !neg_sub, + show nonneg (a - b), from this ▸ H) + (nonneg_sum_nonneg_neg (b - a)) + +theorem of_nat_le_of_nat_of_le {m n : ℕ} (H : #nat m ≤ n) : of_nat m ≤ of_nat n := +obtain (k : ℕ) (Hk : m + k = n), from nat.le.elim H, +le.intro (Hk ▸ (of_nat_add m k)⁻¹) + +theorem le_of_of_nat_le_of_nat {m n : ℕ} (H : of_nat m ≤ of_nat n) : (#nat m ≤ n) := +obtain (k : ℕ) (Hk : of_nat m + of_nat k = of_nat n), from le.elim H, +have m + k = n, from of_nat.inj (of_nat_add m k ⬝ Hk), +nat.le.intro this + +theorem of_nat_le_of_nat_iff (m n : ℕ) : of_nat m ≤ of_nat n ↔ m ≤ n := +iff.intro le_of_of_nat_le_of_nat of_nat_le_of_nat_of_le + +theorem lt_add_succ (a : ℤ) (n : ℕ) : a < a + succ n := +le.intro (show a + 1 + n = a + succ n, from + calc + a + 1 + n = a + (1 + n) : add.assoc + ... = a + (n + 1) : by rewrite (int.add_comm 1 n) + ... = a + succ n : rfl) + +theorem lt.intro {a b : ℤ} {n : ℕ} (H : a + succ n = b) : a < b := +H ▸ lt_add_succ a n + +theorem lt.elim {a b : ℤ} (H : a < b) : Σn : ℕ, a + succ n = b := +obtain (n : ℕ) (Hn : a + 1 + n = b), from le.elim H, +have a + succ n = b, from + calc + a + succ n = a + 1 + n : by rewrite [add.assoc, int.add_comm 1 n] + ... = b : Hn, +sigma.mk n this + +theorem of_nat_lt_of_nat_iff (n m : ℕ) : of_nat n < of_nat m ↔ n < m := +calc + of_nat n < of_nat m ↔ of_nat n + 1 ≤ of_nat m : iff.refl + ... ↔ of_nat (nat.succ n) ≤ of_nat m : of_nat_succ n ▸ !iff.refl + ... ↔ nat.succ n ≤ m : of_nat_le_of_nat_iff + ... ↔ n < m : iff.symm (lt_iff_succ_le _ _) + +theorem lt_of_of_nat_lt_of_nat {m n : ℕ} (H : of_nat m < of_nat n) : #nat m < n := +iff.mp !of_nat_lt_of_nat_iff H + +theorem of_nat_lt_of_nat_of_lt {m n : ℕ} (H : #nat m < n) : of_nat m < of_nat n := +iff.mpr !of_nat_lt_of_nat_iff H + +/- show that the integers form an ordered additive group -/ + +protected theorem le_refl (a : ℤ) : a ≤ a := +le.intro (add_zero a) + +protected theorem le_trans {a b c : ℤ} (H1 : a ≤ b) (H2 : b ≤ c) : a ≤ c := +obtain (n : ℕ) (Hn : a + n = b), from le.elim H1, +obtain (m : ℕ) (Hm : b + m = c), from le.elim H2, +have a + of_nat (n + m) = c, from + calc + a + of_nat (n + m) = a + (of_nat n + m) : {of_nat_add n m} + ... = a + n + m : (add.assoc a n m)⁻¹ + ... = b + m : {Hn} + ... = c : Hm, +le.intro this + +protected theorem le_antisymm : Π {a b : ℤ}, a ≤ b → b ≤ a → a = b := +take a b : ℤ, assume (H₁ : a ≤ b) (H₂ : b ≤ a), +obtain (n : ℕ) (Hn : a + n = b), from le.elim H₁, +obtain (m : ℕ) (Hm : b + m = a), from le.elim H₂, +have a + of_nat (n + m) = a + 0, from + calc + a + of_nat (n + m) = a + (of_nat n + m) : by rewrite of_nat_add + ... = a + n + m : by rewrite add.assoc + ... = b + m : by rewrite Hn + ... = a : by rewrite Hm + ... = a + 0 : by rewrite add_zero, +have of_nat (n + m) = of_nat 0, from add.left_cancel this, +have n + m = 0, from of_nat.inj this, +have n = 0, from nat.eq_zero_of_add_eq_zero_right this, +show a = b, from + calc + a = a + 0 : add_zero + ... = a + n : by rewrite this + ... = b : Hn + +protected theorem lt_irrefl (a : ℤ) : ¬ a < a := +(suppose a < a, + obtain (n : ℕ) (Hn : a + succ n = a), from lt.elim this, + have a + succ n = a + 0, from + Hn ⬝ !add_zero⁻¹, + !succ_ne_zero (of_nat.inj (add.left_cancel this))) + +protected theorem ne_of_lt {a b : ℤ} (H : a < b) : a ≠ b := +(suppose a = b, absurd (this ▸ H) (int.lt_irrefl b)) + +theorem le_of_lt {a b : ℤ} (H : a < b) : a ≤ b := +obtain (n : ℕ) (Hn : a + succ n = b), from lt.elim H, +le.intro Hn + +protected theorem lt_iff_le_prod_ne (a b : ℤ) : a < b ↔ (a ≤ b × a ≠ b) := +iff.intro + (assume H, pair (le_of_lt H) (int.ne_of_lt H)) + (assume H, + have a ≤ b, from prod.pr1 H, + have a ≠ b, from prod.pr2 H, + obtain (n : ℕ) (Hn : a + n = b), from le.elim `a ≤ b`, + have n ≠ 0, from (assume H' : n = 0, `a ≠ b` (!add_zero ▸ H' ▸ Hn)), + obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero this, + lt.intro (Hk ▸ Hn)) + +protected theorem le_iff_lt_sum_eq (a b : ℤ) : a ≤ b ↔ (a < b ⊎ a = b) := +iff.intro + (assume H, + by_cases + (suppose a = b, sum.inr this) + (suppose a ≠ b, + obtain (n : ℕ) (Hn : a + n = b), from le.elim H, + have n ≠ 0, from (assume H' : n = 0, `a ≠ b` (!add_zero ▸ H' ▸ Hn)), + obtain (k : ℕ) (Hk : n = nat.succ k), from nat.exists_eq_succ_of_ne_zero this, + sum.inl (lt.intro (Hk ▸ Hn)))) + (assume H, + sum.elim H + (assume H1, le_of_lt H1) + (assume H1, H1 ▸ !int.le_refl)) + +theorem lt_succ (a : ℤ) : a < a + 1 := +int.le_refl (a + 1) + +protected theorem add_le_add_left {a b : ℤ} (H : a ≤ b) (c : ℤ) : c + a ≤ c + b := +obtain (n : ℕ) (Hn : a + n = b), from le.elim H, +have H2 : c + a + n = c + b, from + calc + c + a + n = c + (a + n) : add.assoc c a n + ... = c + b : {Hn}, +le.intro H2 + +protected theorem add_lt_add_left {a b : ℤ} (H : a < b) (c : ℤ) : c + a < c + b := +let H' := le_of_lt H in +(iff.mpr (int.lt_iff_le_prod_ne _ _)) (pair (int.add_le_add_left H' _) + (take Heq, let Heq' := add_left_cancel Heq in + !int.lt_irrefl (Heq' ▸ H))) + +protected theorem mul_nonneg {a b : ℤ} (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a * b := +obtain (n : ℕ) (Hn : 0 + n = a), from le.elim Ha, +obtain (m : ℕ) (Hm : 0 + m = b), from le.elim Hb, +le.intro + (inverse + (calc + a * b = (0 + n) * b : by rewrite Hn + ... = n * b : by rewrite zero_add + ... = n * (0 + m) : by rewrite Hm + ... = n * m : by rewrite zero_add + ... = 0 + n * m : by rewrite zero_add)) + +protected theorem mul_pos {a b : ℤ} (Ha : 0 < a) (Hb : 0 < b) : 0 < a * b := +obtain (n : ℕ) (Hn : 0 + nat.succ n = a), from lt.elim Ha, +obtain (m : ℕ) (Hm : 0 + nat.succ m = b), from lt.elim Hb, +lt.intro + (inverse + (calc + a * b = (0 + nat.succ n) * b : by rewrite Hn + ... = nat.succ n * b : by rewrite zero_add + ... = nat.succ n * (0 + nat.succ m) : by rewrite Hm + ... = nat.succ n * nat.succ m : by rewrite zero_add + ... = of_nat (nat.succ n * nat.succ m) : by rewrite of_nat_mul + ... = of_nat (nat.succ n * m + nat.succ n) : by rewrite nat.mul_succ + ... = of_nat (nat.succ (nat.succ n * m + n)) : by rewrite nat.add_succ + ... = 0 + nat.succ (nat.succ n * m + n) : by rewrite zero_add)) + +protected theorem zero_lt_one : (0 : ℤ) < 1 := star + +protected theorem not_le_of_gt {a b : ℤ} (H : a < b) : ¬ b ≤ a := + assume Hba, + let Heq := int.le_antisymm (le_of_lt H) Hba in + !int.lt_irrefl (Heq ▸ H) + +protected theorem lt_of_lt_of_le {a b c : ℤ} (Hab : a < b) (Hbc : b ≤ c) : a < c := + let Hab' := le_of_lt Hab in + let Hac := int.le_trans Hab' Hbc in + (iff.mpr !int.lt_iff_le_prod_ne) (pair Hac + (assume Heq, int.not_le_of_gt (Heq ▸ Hab) Hbc)) + +protected theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) : a < c := + let Hbc' := le_of_lt Hbc in + let Hac := int.le_trans Hab Hbc' in + (iff.mpr !int.lt_iff_le_prod_ne) (pair Hac + (assume Heq, int.not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab)) + +protected definition linear_ordered_comm_ring [trans_instance] : + linear_ordered_comm_ring int := +⦃linear_ordered_comm_ring, int.integral_domain, + le := int.le, + le_refl := int.le_refl, + le_trans := @int.le_trans, + le_antisymm := @int.le_antisymm, + lt := int.lt, + le_of_lt := @int.le_of_lt, + lt_irrefl := int.lt_irrefl, + lt_of_lt_of_le := @int.lt_of_lt_of_le, + lt_of_le_of_lt := @int.lt_of_le_of_lt, + add_le_add_left := @int.add_le_add_left, + mul_nonneg := @int.mul_nonneg, + mul_pos := @int.mul_pos, + le_iff_lt_sum_eq := int.le_iff_lt_sum_eq, + le_total := int.le_total, + zero_ne_one := int.zero_ne_one, + zero_lt_one := int.zero_lt_one, + add_lt_add_left := @int.add_lt_add_left⦄ + +protected definition decidable_linear_ordered_comm_ring [instance] : + decidable_linear_ordered_comm_ring int := +⦃decidable_linear_ordered_comm_ring, + int.linear_ordered_comm_ring, + decidable_lt := decidable_lt⦄ + +/- more facts specific to int -/ + +theorem of_nat_nonneg (n : ℕ) : 0 ≤ of_nat n := star + +theorem of_nat_pos {n : ℕ} (Hpos : #nat n > 0) : of_nat n > 0 := +of_nat_lt_of_nat_of_lt Hpos + +theorem of_nat_succ_pos (n : nat) : of_nat (nat.succ n) > 0 := +of_nat_pos !nat.succ_pos + +theorem exists_eq_of_nat {a : ℤ} (H : 0 ≤ a) : Σn : ℕ, a = of_nat n := +obtain (n : ℕ) (H1 : 0 + of_nat n = a), from le.elim H, +sigma.mk n (!zero_add ▸ (H1⁻¹)) + +theorem exists_eq_neg_of_nat {a : ℤ} (H : a ≤ 0) : Σn : ℕ, a = -(of_nat n) := +have -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H, +obtain (n : ℕ) (Hn : -a = of_nat n), from exists_eq_of_nat this, +sigma.mk n (eq_neg_of_eq_neg (Hn⁻¹)) + +theorem of_nat_nat_abs_of_nonneg {a : ℤ} (H : a ≥ 0) : of_nat (nat_abs a) = a := +obtain (n : ℕ) (Hn : a = of_nat n), from exists_eq_of_nat H, +Hn⁻¹ ▸ ap of_nat (nat_abs_of_nat n) + +theorem of_nat_nat_abs_of_nonpos {a : ℤ} (H : a ≤ 0) : of_nat (nat_abs a) = -a := +have -a ≥ 0, from iff.mpr !neg_nonneg_iff_nonpos H, +calc + of_nat (nat_abs a) = of_nat (nat_abs (-a)) : nat_abs_neg + ... = -a : of_nat_nat_abs_of_nonneg this + +theorem of_nat_nat_abs (b : ℤ) : nat_abs b = abs b := +sum.elim (le.total 0 b) + (assume H : b ≥ 0, of_nat_nat_abs_of_nonneg H ⬝ (abs_of_nonneg H)⁻¹) + (assume H : b ≤ 0, of_nat_nat_abs_of_nonpos H ⬝ (abs_of_nonpos H)⁻¹) + +theorem nat_abs_abs (a : ℤ) : nat_abs (abs a) = nat_abs a := +abs.by_cases rfl !nat_abs_neg + +theorem lt_of_add_one_le {a b : ℤ} (H : a + 1 ≤ b) : a < b := +obtain (n : nat) (H1 : a + 1 + n = b), from le.elim H, +have a + succ n = b, by rewrite [-H1, add.assoc, add.comm 1], +lt.intro this + +theorem add_one_le_of_lt {a b : ℤ} (H : a < b) : a + 1 ≤ b := +obtain (n : nat) (H1 : a + succ n = b), from lt.elim H, +have a + 1 + n = b, by rewrite [-H1, add.assoc, add.comm 1], +le.intro this + +theorem lt_add_one_of_le {a b : ℤ} (H : a ≤ b) : a < b + 1 := +lt_add_of_le_of_pos H star + +theorem le_of_lt_add_one {a b : ℤ} (H : a < b + 1) : a ≤ b := +have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H, +le_of_add_le_add_right H1 + +theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b := +lt_of_add_one_le (begin rewrite sub_add_cancel, exact H end) + +theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b := +!sub_add_cancel ▸ add_one_le_of_lt H + +theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 := +le_of_lt_add_one begin rewrite sub_add_cancel, exact H end + +theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b := +!sub_add_cancel ▸ (lt_add_one_of_le H) + +theorem sign_of_succ (n : nat) : sign (nat.succ n) = 1 := +sign_of_pos (of_nat_pos !nat.succ_pos) + +theorem exists_eq_neg_succ_of_nat {a : ℤ} : a < 0 → Σm : ℕ, a = -[1+m] := +int.cases_on a + (take (m : nat) H, absurd (of_nat_nonneg m : 0 ≤ m) (not_le_of_gt H)) + (take (m : nat) H, sigma.mk m rfl) + +theorem eq_one_of_mul_eq_one_right {a b : ℤ} (H : a ≥ 0) (H' : a * b = 1) : a = 1 := +have a * b > 0, by rewrite H'; apply star, +have b > 0, from pos_of_mul_pos_left this H, +have a > 0, from pos_of_mul_pos_right `a * b > 0` (le_of_lt `b > 0`), +sum.elim (le_sum_gt a 1) + (suppose a ≤ 1, + show a = 1, from le.antisymm this (add_one_le_of_lt `a > 0`)) + (suppose a > 1, + have a * b ≥ 2 * 1, + from mul_le_mul (add_one_le_of_lt `a > 1`) (add_one_le_of_lt `b > 0`) star H, + have empty, by rewrite [H' at this]; exact this, + empty.elim this) + +theorem eq_one_of_mul_eq_one_left {a b : ℤ} (H : b ≥ 0) (H' : a * b = 1) : b = 1 := +eq_one_of_mul_eq_one_right H (!mul.comm ▸ H') + +theorem eq_one_of_mul_eq_self_left {a b : ℤ} (Hpos : a ≠ 0) (H : b * a = a) : b = 1 := +eq_of_mul_eq_mul_right Hpos (H ⬝ (one_mul a)⁻¹) + +theorem eq_one_of_mul_eq_self_right {a b : ℤ} (Hpos : b ≠ 0) (H : b * a = b) : a = 1 := +eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H) + +theorem eq_one_of_dvd_one {a : ℤ} (H : a ≥ 0) (H' : a ∣ 1) : a = 1 := +dvd.elim H' + (take b, + suppose 1 = a * b, + eq_one_of_mul_eq_one_right H this⁻¹) + +theorem exists_least_of_bdd {P : ℤ → Type} [HP : decidable_pred P] + (Hbdd : Σ b : ℤ, Π z : ℤ, z ≤ b → ¬ P z) + (Hinh : Σ z : ℤ, P z) : Σ lb : ℤ, P lb × (Π z : ℤ, z < lb → ¬ P z) := + begin + cases Hbdd with [b, Hb], + cases Hinh with [elt, Helt], + existsi b + of_nat (least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b)))), + have Heltb : elt > b, begin + apply lt_of_not_ge, + intro Hge, + apply (Hb _ Hge) Helt + end, + have H' : P (b + of_nat (nat_abs (elt - b))), begin + rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)), + add.comm, sub_add_cancel], + apply Helt + end, + apply pair, + apply least_of_lt _ !lt_succ_self H', + intros z Hz, + cases em (z ≤ b) with [Hzb, Hzb], + apply Hb _ Hzb, + let Hzb' := lt_of_not_ge Hzb, + let Hpos := iff.mpr !sub_pos_iff_lt Hzb', + have Hzbk : z = b + of_nat (nat_abs (z - b)), + by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, sub_add_cancel], + have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin + note Hz' := iff.mp !lt_add_iff_sub_lt_left Hz, + rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], + apply lt_of_of_nat_lt_of_nat Hz' + end, + let Hk' := not_le_of_gt Hk, + rewrite Hzbk, + apply λ p, mt (ge_least_of_lt _ p) Hk', + apply nat.lt_trans Hk, + apply least_lt _ !lt_succ_self H' + end + +theorem exists_greatest_of_bdd {P : ℤ → Type} [HP : decidable_pred P] + (Hbdd : Σ b : ℤ, Π z : ℤ, z ≥ b → ¬ P z) + (Hinh : Σ z : ℤ, P z) : Σ ub : ℤ, P ub × (Π z : ℤ, z > ub → ¬ P z) := + begin + cases Hbdd with [b, Hb], + cases Hinh with [elt, Helt], + existsi b - of_nat (least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt)))), + have Heltb : elt < b, begin + apply lt_of_not_ge, + intro Hge, + apply (Hb _ Hge) Helt + end, + have H' : P (b - of_nat (nat_abs (b - elt))), begin + rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)), + sub_sub_self], + apply Helt + end, + apply pair, + apply least_of_lt _ !lt_succ_self H', + intros z Hz, + cases em (z ≥ b) with [Hzb, Hzb], + apply Hb _ Hzb, + let Hzb' := lt_of_not_ge Hzb, + let Hpos := iff.mpr !sub_pos_iff_lt Hzb', + have Hzbk : z = b - of_nat (nat_abs (b - z)), + by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), sub_sub_self], + have Hk : nat_abs (b - z) < least (λ n, P (b - of_nat n)) (nat.succ (nat_abs (b - elt))), begin + note Hz' := iff.mp !lt_add_iff_sub_lt_left (iff.mpr !lt_add_iff_sub_lt_right Hz), + rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'], + apply lt_of_of_nat_lt_of_nat Hz' + end, + let Hk' := not_le_of_gt Hk, + rewrite Hzbk, + apply λ p, mt (ge_least_of_lt _ p) Hk', + apply nat.lt_trans Hk, + apply least_lt _ !lt_succ_self H' + end + +end int diff --git a/hott/types/nat/basic.hlean b/hott/types/nat/basic.hlean index 565340ea9..32f508782 100644 --- a/hott/types/nat/basic.hlean +++ b/hott/types/nat/basic.hlean @@ -314,5 +314,5 @@ definition iterate {A : Type} (op : A → A) : ℕ → A → A | 0 := λ a, a | (succ k) := λ a, op (iterate k a) -notation f`^[`n`]` := iterate f n +notation f `^[`:80 n:0 `]`:0 := iterate f n end diff --git a/hott/types/nat/nat.md b/hott/types/nat/nat.md index 68d0319ef..e2baab3fd 100644 --- a/hott/types/nat/nat.md +++ b/hott/types/nat/nat.md @@ -6,3 +6,4 @@ The natural numbers. Note: all these files are ported from the standard library. * [basic](basic.hlean) : the natural numbers, with succ, pred, addition, and multiplication * [order](order.hlean) : less-than, less-then-or-equal, etc. * [sub](sub.hlean) : subtraction, and distance +* [div](div.hlean) : divisibility, the mod operator, division diff --git a/hott/types/prod.hlean b/hott/types/prod.hlean index 242dadb6a..38d33bed3 100644 --- a/hott/types/prod.hlean +++ b/hott/types/prod.hlean @@ -22,7 +22,7 @@ namespace prod definition pair_eq [unfold 7 8] (pa : a = a') (pb : b = b') : (a, b) = (a', b') := ap011 prod.mk pa pb - definition prod_eq [unfold 3 4 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v := + definition prod_eq [unfold 5 6] (H₁ : u.1 = v.1) (H₂ : u.2 = v.2) : u = v := by cases u; cases v; exact pair_eq H₁ H₂ definition eq_pr1 [unfold 5] (p : u = v) : u.1 = v.1 := @@ -54,8 +54,8 @@ namespace prod by induction p; induction u; reflexivity -- the uncurried version of prod_eq. We will prove that this is an equivalence - definition prod_eq_unc (H : u.1 = v.1 × u.2 = v.2) : u = v := - by cases H with H₁ H₂;exact prod_eq H₁ H₂ + definition prod_eq_unc [unfold 5] (H : u.1 = v.1 × u.2 = v.2) : u = v := + by cases H with H₁ H₂; exact prod_eq H₁ H₂ definition pair_prod_eq_unc : Π(pq : u.1 = v.1 × u.2 = v.2), ((prod_eq_unc pq)..1, (prod_eq_unc pq)..2) = pq @@ -80,6 +80,10 @@ namespace prod definition prod_eq_equiv [constructor] (u v : A × B) : (u = v) ≃ (u.1 = v.1 × u.2 = v.2) := (equiv.mk prod_eq_unc _)⁻¹ᵉ + definition pair_eq_pair_equiv [constructor] (a a' : A) (b b' : B) : + ((a, b) = (a', b')) ≃ (a = a' × b = b') := + prod_eq_equiv (a, b) (a', b') + definition ap_prod_mk_left (p : a = a') : ap (λa, prod.mk a b) p = prod_eq p idp := ap_eq_ap011_left prod.mk p b