michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(hott): port group_power and int/order from standard library. Update markdown files

Browse source
This commit is contained in:
Floris van Doorn 2017-05-19 13:36:43 -04:00
parent a588c0f205
commit 0cf04ed3f2
10 changed files with 721 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
hott/algebra/algebra.md
View file

@ -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):

264
hott/algebra/group_power.hlean Normal file
View file

@ -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

2
hott/algebra/group_theory.hlean
View file

@ -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

4
hott/init/path.hlean
View file

@ -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

2
hott/types/int/default.hlean
View file

@ -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

1
hott/types/int/int.md
View file

@ -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

438
hott/types/int/order.hlean Normal file
View file

@ -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

2
hott/types/nat/basic.hlean
View file

@ -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

1
hott/types/nat/nat.md
View file

@ -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

10
hott/types/prod.hlean
View file

@ -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