feat(hott): port parts of natural numbers and integers from standard library to HoTT

This also involves:
- adding definitions about logic and natural numbers existing in the standard library to init
- porting the current algebraic hierarchy
This commit is contained in:
Floris van Doorn 2015-05-05 17:25:35 -04:00 committed by Leonardo de Moura
parent e9ff925e2f
commit 7cfac38eda
25 changed files with 4485 additions and 374 deletions

View file

@ -1,9 +1,15 @@
algebra
=======
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)).
* [binary](binary.hlean) : properties of binary operations
* [relation](relation.hlean) : properties of relations
* [group](group.hlean)
* [ring](ring.hlean)
* [ordered_group](ordered_group.hlean)
* [ordered_ring](ordered_ring.hlean)
* [field](field.hlean)
Subfolders:

View file

@ -10,7 +10,7 @@ Ported from Coq HoTT
import .iso ..group
open eq is_trunc iso category path_algebra nat unit
open eq is_trunc iso category algebra nat unit
namespace category
@ -72,15 +72,15 @@ namespace category
begin
fapply groupoid.mk, fapply precategory.mk,
intros, exact A,
intros, apply (@group.carrier_hset A G),
intros, apply (@group.is_hset_carrier A G),
intros [a, b, c, g, h], exact (@group.mul A G g h),
intro a, exact (@group.one A G),
intros, exact (@group.mul_assoc A G h g f)⁻¹,
intros, exact (@group.one_mul A G f),
intros, exact (@group.mul_one A G f),
intros, esimp [precategory.mk], apply is_iso.mk,
apply mul_left_inv,
apply mul_right_inv,
apply mul.left_inv,
apply mul.right_inv,
end
protected definition hom_group {A : Type} [G : groupoid A] (a : A) :

466
hott/algebra/field.hlean Normal file
View file

@ -0,0 +1,466 @@
/-
Copyright (c) 2014 Robert Lewis. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.field
Authors: Robert Lewis
Structures with multiplicative and additive components, including division rings and fields.
The development is modeled after Isabelle's library.
Ported from the standard library
-/
----------------------------------------------------------------------------------------------------
import algebra.ring
open core
namespace algebra
variable {A : Type}
-- in division rings, 1 / 0 = 0
structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A :=
(mul_inv_cancel : Π{a}, a ≠ zero → mul a (inv a) = one)
(inv_mul_cancel : Π{a}, a ≠ zero → mul (inv a) a = one)
--(inv_zero : inv zero = zero)
section division_ring
variables [s : division_ring A] {a b c : A}
include s
definition divide (a b : A) : A := a * b⁻¹
infix `/` := divide
-- only in this file
local attribute divide [reducible]
definition mul_inv_cancel (H : a ≠ 0) : a * a⁻¹ = 1 :=
division_ring.mul_inv_cancel H
definition inv_mul_cancel (H : a ≠ 0) : a⁻¹ * a = 1 :=
division_ring.inv_mul_cancel H
definition inv_eq_one_div : a⁻¹ = 1 / a := !one_mul⁻¹
-- the following are only theorems if we assume inv_zero here
/- definition inv_zero : 0⁻¹ = 0 := !division_ring.inv_zero
definition one_div_zero : 1 / 0 = 0 :=
calc
1 / 0 = 1 * 0⁻¹ : refl
... = 1 * 0 : division_ring.inv_zero A
... = 0 : mul_zero
-/
definition div_eq_mul_one_div : a / b = a * (1 / b) :=
by rewrite [↑divide, one_mul]
-- definition div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
definition mul_one_div_cancel (H : a ≠ 0) : a * (1 / a) = 1 :=
by rewrite [-inv_eq_one_div, (mul_inv_cancel H)]
definition one_div_mul_cancel (H : a ≠ 0) : (1 / a) * a = 1 :=
by rewrite [-inv_eq_one_div, (inv_mul_cancel H)]
definition div_self (H : a ≠ 0) : a / a = 1 := mul_inv_cancel H
definition one_div_one : 1 / 1 = 1 := div_self (ne.symm zero_ne_one)
definition mul_div_assoc : (a * b) / c = a * (b / c) := !mul.assoc
definition one_div_ne_zero (H : a ≠ 0) : 1 / a ≠ 0 :=
assume H2 : 1 / a = 0,
have C1 : 0 = 1, from inverse (by rewrite [-(mul_one_div_cancel H), H2, mul_zero]),
absurd C1 zero_ne_one
-- definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
-- assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
-- the analogue in group is called inv_one
definition inv_one_is_one : 1⁻¹ = 1 :=
by rewrite [-mul_one, (inv_mul_cancel (ne.symm zero_ne_one))]
definition div_one : a / 1 = a :=
by rewrite [↑divide, inv_one_is_one, mul_one]
definition zero_div : 0 / a = 0 := !zero_mul
-- note: integral domain has a "mul_ne_zero". Discrete fields are int domains.
definition mul_ne_zero' (Ha : a ≠ 0) (Hb : b ≠ 0) : a * b ≠ 0 :=
assume H : a * b = 0,
have C1 : a = 0, by rewrite [-mul_one, -(mul_one_div_cancel Hb), -mul.assoc, H, zero_mul],
absurd C1 Ha
definition mul_ne_zero_comm (H : a * b ≠ 0) : b * a ≠ 0 :=
have H2 : a ≠ 0 × b ≠ 0, from mul_ne_zero_imp_ne_zero H,
mul_ne_zero' (prod.pr2 H2) (prod.pr1 H2)
-- make "left" and "right" versions?
definition eq_one_div_of_mul_eq_one (H : a * b = 1) : b = 1 / a :=
have H2 : a ≠ 0, from
(assume A : a = 0,
have B : 0 = 1, by rewrite [-(zero_mul b), -A, H],
absurd B zero_ne_one),
show b = 1 / a, from inverse (calc
1 / a = (1 / a) * 1 : mul_one
... = (1 / a) * (a * b) : H
... = (1 / a) * a * b : mul.assoc
... = 1 * b : one_div_mul_cancel H2
... = b : one_mul)
-- which one is left and which is right?
definition eq_one_div_of_mul_eq_one_left (H : b * a = 1) : b = 1 / a :=
have H2 : a ≠ 0, from
(assume A : a = 0,
have B : 0 = 1, from inverse (calc
1 = b * a : inverse H
... = b * 0 : A
... = 0 : mul_zero),
absurd B zero_ne_one),
show b = 1 / a, from inverse (calc
1 / a = 1 * (1 / a) : one_mul
... = b * a * (1 / a) : H
... = b * (a * (1 / a)) : mul.assoc
... = b * 1 : mul_one_div_cancel H2
... = b : mul_one)
definition one_div_mul_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (b * a) :=
have H : (b * a) * ((1 / a) * (1 / b)) = 1, by
rewrite [mul.assoc, -(mul.assoc a), (mul_one_div_cancel Ha), one_mul, (mul_one_div_cancel Hb)],
eq_one_div_of_mul_eq_one H
definition one_div_neg_one_eq_neg_one : 1 / (-1) = -1 :=
have H : (-1) * (-1) = 1, by rewrite [-neg_eq_neg_one_mul, neg_neg],
inverse (eq_one_div_of_mul_eq_one H)
definition one_div_neg_eq_neg_one_div (H : a ≠ 0) : 1 / (- a) = - (1 / a) :=
have H1 : -1 ≠ 0, from
(assume H2 : -1 = 0, absurd (inverse (calc
1 = -(-1) : neg_neg
... = -0 : H2
... = 0 : neg_zero)) zero_ne_one),
calc
1 / (- a) = 1 / ((-1) * a) : neg_eq_neg_one_mul
... = (1 / a) * (1 / (- 1)) : one_div_mul_one_div H H1
... = (1 / a) * (-1) : one_div_neg_one_eq_neg_one
... = - (1 / a) : mul_neg_one_eq_neg
definition div_neg_eq_neg_div (Ha : a ≠ 0) : b / (- a) = - (b / a) :=
calc
b / (- a) = b * (1 / (- a)) : inv_eq_one_div
... = b * -(1 / a) : one_div_neg_eq_neg_one_div Ha
... = -(b * (1 / a)) : neg_mul_eq_mul_neg
... = - (b * a⁻¹) : inv_eq_one_div
definition neg_div (Ha : a ≠ 0) : (-b) / a = - (b / a) :=
by rewrite [neg_eq_neg_one_mul, mul_div_assoc, -neg_eq_neg_one_mul]
definition neg_div_neg_eq_div (Hb : b ≠ 0) : (-a) / (-b) = a / b :=
by rewrite [(div_neg_eq_neg_div Hb), (neg_div Hb), neg_neg]
definition div_div (H : a ≠ 0) : 1 / (1 / a) = a :=
inverse (eq_one_div_of_mul_eq_one_left (mul_one_div_cancel H))
definition eq_of_invs_eq (Ha : a ≠ 0) (Hb : b ≠ 0) (H : 1 / a = 1 / b) : a = b :=
by rewrite [-(div_div Ha), H, (div_div Hb)]
-- oops, the analogous definition in group is called inv_mul, but it *should* be called
-- mul_inv, in which case, we will have to rename this one
definition mul_inv (Ha : a ≠ 0) (Hb : b ≠ 0) : (b * a)⁻¹ = a⁻¹ * b⁻¹ :=
have H1 : b * a ≠ 0, from mul_ne_zero' Hb Ha,
inverse (calc
a⁻¹ * b⁻¹ = (1 / a) * b⁻¹ : inv_eq_one_div
... = (1 / a) * (1 / b) : inv_eq_one_div
... = (1 / (b * a)) : one_div_mul_one_div Ha Hb
... = (b * a)⁻¹ : inv_eq_one_div)
definition mul_div_cancel (Hb : b ≠ 0) : a * b / b = a :=
by rewrite [↑divide, mul.assoc, (mul_inv_cancel Hb), mul_one]
definition div_mul_cancel (Hb : b ≠ 0) : a / b * b = a :=
by rewrite [↑divide, mul.assoc, (inv_mul_cancel Hb), mul_one]
definition div_add_div_same : a / c + b / c = (a + b) / c := !right_distrib⁻¹
definition inv_mul_add_mul_inv_eq_inv_add_inv (Ha : a ≠ 0) (Hb : b ≠ 0) :
(1 / a) * (a + b) * (1 / b) = 1 / a + 1 / b :=
by rewrite [(left_distrib (1 / a)), (one_div_mul_cancel Ha), right_distrib, one_mul,
mul.assoc, (mul_one_div_cancel Hb), mul_one, add.comm]
definition inv_mul_sub_mul_inv_eq_inv_add_inv (Ha : a ≠ 0) (Hb : b ≠ 0) :
(1 / a) * (b - a) * (1 / b) = 1 / a - 1 / b :=
by rewrite [(mul_sub_left_distrib (1 / a)), (one_div_mul_cancel Ha), mul_sub_right_distrib,
one_mul, mul.assoc, (mul_one_div_cancel Hb), mul_one, one_mul]
definition div_eq_one_iff_eq (Hb : b ≠ 0) : a / b = 1 ↔ a = b :=
iff.intro
(assume H1 : a / b = 1, inverse (calc
b = 1 * b : one_mul
... = a / b * b : H1
... = a : div_mul_cancel Hb))
(assume H2 : a = b, calc
a / b = b / b : H2
... = 1 : div_self Hb)
definition eq_div_iff_mul_eq (Hc : c ≠ 0) : a = b / c ↔ a * c = b :=
iff.intro
(assume H : a = b / c, by rewrite [H, (div_mul_cancel Hc)])
(assume H : a * c = b, by rewrite [-(mul_div_cancel Hc), H])
definition add_div_eq_mul_add_div (Hc : c ≠ 0) : a + b / c = (a * c + b) / c :=
have H : (a + b / c) * c = a * c + b, by rewrite [right_distrib, (div_mul_cancel Hc)],
(iff.elim_right (eq_div_iff_mul_eq Hc)) H
definition mul_mul_div (Hc : c ≠ 0) : a = a * c * (1 / c) :=
calc
a = a * 1 : mul_one
... = a * (c * (1 / c)) : mul_one_div_cancel Hc
... = a * c * (1 / c) : mul.assoc
-- There are many similar rules to these last two in the Isabelle library
-- that haven't been ported yet. Do as necessary.
end division_ring
structure field [class] (A : Type) extends division_ring A, comm_ring A
section field
variables [s : field A] {a b c d: A}
include s
local attribute divide [reducible]
definition one_div_mul_one_div' (Ha : a ≠ 0) (Hb : b ≠ 0) : (1 / a) * (1 / b) = 1 / (a * b) :=
by rewrite [(one_div_mul_one_div Ha Hb), mul.comm b]
definition div_mul_right (Hb : b ≠ 0) (H : a * b ≠ 0) : a / (a * b) = 1 / b :=
let Ha : a ≠ 0 := prod.pr1 (mul_ne_zero_imp_ne_zero H) in
inverse (calc
1 / b = 1 * (1 / b) : one_mul
... = (a * a⁻¹) * (1 / b) : mul_inv_cancel Ha
... = a * (a⁻¹ * (1 / b)) : mul.assoc
... = a * ((1 / a) * (1 / b)) :inv_eq_one_div
... = a * (1 / (b * a)) : one_div_mul_one_div Ha Hb
... = a * (1 / (a * b)) : mul.comm
... = a * (a * b)⁻¹ : inv_eq_one_div)
definition div_mul_left (Ha : a ≠ 0) (H : a * b ≠ 0) : b / (a * b) = 1 / a :=
let H1 : b * a ≠ 0 := mul_ne_zero_comm H in
by rewrite [mul.comm a, (div_mul_right Ha H1)]
definition mul_div_cancel_left (Ha : a ≠ 0) : a * b / a = b :=
by rewrite [mul.comm a, (mul_div_cancel Ha)]
definition mul_div_cancel' (Hb : b ≠ 0) : b * (a / b) = a :=
by rewrite [mul.comm, (div_mul_cancel Hb)]
definition one_div_add_one_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / a + 1 / b = (a + b) / (a * b) :=
have H [visible] : a * b ≠ 0, from (mul_ne_zero' Ha Hb),
by rewrite [add.comm, -(div_mul_left Ha H), -(div_mul_right Hb H), ↑divide, -right_distrib]
definition div_mul_div (Hb : b ≠ 0) (Hd : d ≠ 0) : (a / b) * (c / d) = (a * c) / (b * d) :=
by rewrite [↑divide, 2 mul.assoc, (mul.comm b⁻¹), mul.assoc, (mul_inv Hd Hb)]
definition mul_div_mul_left (Hb : b ≠ 0) (Hc : c ≠ 0) : (c * a) / (c * b) = a / b :=
have H [visible] : c * b ≠ 0, from mul_ne_zero' Hc Hb,
by rewrite [-(div_mul_div Hc Hb), (div_self Hc), one_mul]
definition mul_div_mul_right (Hb : b ≠ 0) (Hc : c ≠ 0) : (a * c) / (b * c) = a / b :=
by rewrite [(mul.comm a), (mul.comm b), (mul_div_mul_left Hb Hc)]
definition div_mul_eq_mul_div : (b / c) * a = (b * a) / c :=
by rewrite [↑divide, mul.assoc, (mul.comm c⁻¹), -mul.assoc]
-- this one is odd -- I am not sure what to call it, but again, the prefix is right
definition div_mul_eq_mul_div_comm (Hc : c ≠ 0) : (b / c) * a = b * (a / c) :=
by rewrite [(div_mul_eq_mul_div), -(one_mul c), -(div_mul_div (ne.symm zero_ne_one) Hc), div_one, one_mul]
definition div_add_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
(a / b) + (c / d) = ((a * d) + (b * c)) / (b * d) :=
have H [visible] : b * d ≠ 0, from mul_ne_zero' Hb Hd,
by rewrite [-(mul_div_mul_right Hb Hd), -(mul_div_mul_left Hd Hb), div_add_div_same]
definition div_sub_div (Hb : b ≠ 0) (Hd : d ≠ 0) :
(a / b) - (c / d) = ((a * d) - (b * c)) / (b * d) :=
by rewrite [↑sub, neg_eq_neg_one_mul, -mul_div_assoc, (div_add_div Hb Hd),
-mul.assoc, (mul.comm b), mul.assoc, -neg_eq_neg_one_mul]
definition mul_eq_mul_of_div_eq_div (Hb : b ≠ 0) (Hd : d ≠ 0) (H : a / b = c / d) : a * d = c * b :=
by rewrite [-mul_one, mul.assoc, (mul.comm d), -mul.assoc, -(div_self Hb),
-(div_mul_eq_mul_div_comm Hb), H, (div_mul_eq_mul_div), (div_mul_cancel Hd)]
definition one_div_div (Ha : a ≠ 0) (Hb : b ≠ 0) : 1 / (a / b) = b / a :=
have H : (a / b) * (b / a) = 1, from calc
(a / b) * (b / a) = (a * b) / (b * a) : div_mul_div Hb Ha
... = (a * b) / (a * b) : mul.comm
... = 1 : div_self (mul_ne_zero' Ha Hb),
inverse (eq_one_div_of_mul_eq_one H)
definition div_div_eq_mul_div (Hb : b ≠ 0) (Hc : c ≠ 0) : a / (b / c) = (a * c) / b :=
by rewrite [div_eq_mul_one_div, (one_div_div Hb Hc), -mul_div_assoc]
definition div_div_eq_div_mul (Hb : b ≠ 0) (Hc : c ≠ 0) : (a / b) / c = a / (b * c) :=
by rewrite [div_eq_mul_one_div, (div_mul_div Hb Hc), mul_one]
definition div_div_div_div (Hb : b ≠ 0) (Hc : c ≠ 0) (Hd : d ≠ 0) : (a / b) / (c / d) = (a * d) / (b * c) :=
by rewrite [(div_div_eq_mul_div Hc Hd), (div_mul_eq_mul_div), (div_div_eq_div_mul Hb Hc)]
-- remaining to transfer from Isabelle fields: ordered fields
end field
structure discrete_field [class] (A : Type) extends field A :=
(has_decidable_eq : decidable_eq A)
(inv_zero : inv zero = zero)
attribute discrete_field.has_decidable_eq [instance]
section discrete_field
variable [s : discrete_field A]
include s
variables {a b c d : A}
-- many of the theorems in discrete_field are the same as theorems in field or division ring,
-- but with fewer hypotheses since 0⁻¹ = 0 and equality is decidable.
-- they are named with '. Is there a better convention?
definition discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero
(x y : A) (H : x * y = 0) : x = 0 ⊎ y = 0 :=
decidable.by_cases
(assume H : x = 0, sum.inl H)
(assume H1 : x ≠ 0,
sum.inr (by rewrite [-one_mul, -(inv_mul_cancel H1), mul.assoc, H, mul_zero]))
definition discrete_field.to_integral_domain [instance] [reducible] [coercion] :
integral_domain A :=
⦃ integral_domain, s,
eq_zero_or_eq_zero_of_mul_eq_zero := discrete_field.eq_zero_or_eq_zero_of_mul_eq_zero⦄
definition inv_zero : 0⁻¹ = (0 : A) := !discrete_field.inv_zero
definition one_div_zero : 1 / 0 = 0 :=
calc
1 / 0 = 1 * 0⁻¹ : refl
... = 1 * 0 : discrete_field.inv_zero A
... = 0 : mul_zero
definition div_zero : a / 0 = 0 := by rewrite [div_eq_mul_one_div, one_div_zero, mul_zero]
definition ne_zero_of_one_div_ne_zero (H : 1 / a ≠ 0) : a ≠ 0 :=
assume Ha : a = 0, absurd (Ha⁻¹ ▸ one_div_zero) H
definition inv_zero_imp_zero (H : 1 / a = 0) : a = 0 :=
decidable.by_cases
(assume Ha, Ha)
(assume Ha, empty.elim ((one_div_ne_zero Ha) H))
-- the following could all go in "discrete_division_ring"
definition one_div_mul_one_div'' : (1 / a) * (1 / b) = 1 / (b * a) :=
decidable.by_cases
(assume Ha : a = 0,
by rewrite [Ha, div_zero, zero_mul, -(@div_zero A s 1), mul_zero b])
(assume Ha : a ≠ 0,
decidable.by_cases
(assume Hb : b = 0,
by rewrite [Hb, div_zero, mul_zero, -(@div_zero A s 1), zero_mul a])
(assume Hb : b ≠ 0, one_div_mul_one_div Ha Hb))
definition one_div_neg_eq_neg_one_div' : 1 / (- a) = - (1 / a) :=
decidable.by_cases
(assume Ha : a = 0, by rewrite [Ha, neg_zero, 2 div_zero, neg_zero])
(assume Ha : a ≠ 0, one_div_neg_eq_neg_one_div Ha)
definition neg_div' : (-b) / a = - (b / a) :=
decidable.by_cases
(assume Ha : a = 0, by rewrite [Ha, 2 div_zero, neg_zero])
(assume Ha : a ≠ 0, neg_div Ha)
definition neg_div_neg_eq_div' : (-a) / (-b) = a / b :=
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, neg_zero, 2 div_zero])
(assume Hb : b ≠ 0, neg_div_neg_eq_div Hb)
definition div_div' : 1 / (1 / a) = a :=
decidable.by_cases
(assume Ha : a = 0, by rewrite [Ha, 2 div_zero])
(assume Ha : a ≠ 0, div_div Ha)
definition eq_of_invs_eq' (H : 1 / a = 1 / b) : a = b :=
decidable.by_cases
(assume Ha : a = 0,
have Hb : b = 0, from inv_zero_imp_zero (by rewrite [-H, Ha, div_zero]),
Hb⁻¹ ▸ Ha)
(assume Ha : a ≠ 0,
have Hb : b ≠ 0, from ne_zero_of_one_div_ne_zero (H ▸ (one_div_ne_zero Ha)),
eq_of_invs_eq Ha Hb H)
definition mul_inv' : (b * a)⁻¹ = a⁻¹ * b⁻¹ :=
decidable.by_cases
(assume Ha : a = 0, by rewrite [Ha, mul_zero, 2 inv_zero, zero_mul])
(assume Ha : a ≠ 0,
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, zero_mul, 2 inv_zero, mul_zero])
(assume Hb : b ≠ 0, mul_inv Ha Hb))
-- the following are specifically for fields
definition one_div_mul_one_div''' : (1 / a) * (1 / b) = 1 / (a * b) :=
by rewrite [(one_div_mul_one_div''), mul.comm b]
definition div_mul_right' (Ha : a ≠ 0) : a / (a * b) = 1 / b :=
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, mul_zero, 2 div_zero])
(assume Hb : b ≠ 0, div_mul_right Hb (mul_ne_zero Ha Hb))
definition div_mul_left' (Hb : b ≠ 0) : b / (a * b) = 1 / a :=
by rewrite [mul.comm a, div_mul_right' Hb]
definition div_mul_div' : (a / b) * (c / d) = (a * c) / (b * d) :=
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, div_zero, zero_mul, -(@div_zero A s (a * c)), zero_mul])
(assume Hb : b ≠ 0,
decidable.by_cases
(assume Hd : d = 0, by rewrite [Hd, div_zero, mul_zero, -(@div_zero A s (a * c)), mul_zero])
(assume Hd : d ≠ 0, div_mul_div Hb Hd))
definition mul_div_mul_left' (Hc : c ≠ 0) : (c * a) / (c * b) = a / b :=
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, mul_zero, 2 div_zero])
(assume Hb : b ≠ 0, mul_div_mul_left Hb Hc)
definition mul_div_mul_right' (Hc : c ≠ 0) : (a * c) / (b * c) = a / b :=
by rewrite [(mul.comm a), (mul.comm b), (mul_div_mul_left' Hc)]
-- this one is odd -- I am not sure what to call it, but again, the prefix is right
definition div_mul_eq_mul_div_comm' : (b / c) * a = b * (a / c) :=
decidable.by_cases
(assume Hc : c = 0, by rewrite [Hc, div_zero, zero_mul, -(mul_zero b), -(@div_zero A s a)])
(assume Hc : c ≠ 0, div_mul_eq_mul_div_comm Hc)
definition one_div_div' : 1 / (a / b) = b / a :=
decidable.by_cases
(assume Ha : a = 0, by rewrite [Ha, zero_div, 2 div_zero])
(assume Ha : a ≠ 0,
decidable.by_cases
(assume Hb : b = 0, by rewrite [Hb, 2 div_zero, zero_div])
(assume Hb : b ≠ 0, one_div_div Ha Hb))
definition div_div_eq_mul_div' : a / (b / c) = (a * c) / b :=
by rewrite [div_eq_mul_one_div, one_div_div', -mul_div_assoc]
definition div_div_eq_div_mul' : (a / b) / c = a / (b * c) :=
by rewrite [div_eq_mul_one_div, div_mul_div', mul_one]
definition div_div_div_div' : (a / b) / (c / d) = (a * d) / (b * c) :=
by rewrite [div_div_eq_mul_div', div_mul_eq_mul_div, div_div_eq_div_mul']
end discrete_field
end algebra
/-
decidable.by_cases
(assume Ha : a = 0, sorry)
(assume Ha : a ≠ 0, sorry)
-/

View file

@ -5,14 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.group
Authors: Jeremy Avigad, Leonardo de Moura
Various multiplicative and additive structures. Partially modeled on Isabelle's library.
Various multiplicative and additive structures.
Ported from the standard library
-/
import algebra.binary
open eq is_trunc binary -- note: ⁻¹ will be overloaded
namespace path_algebra
namespace algebra
variable {A : Type}
@ -45,77 +46,75 @@ notation 0 := !has_zero.zero
--a second notation for the inverse, which is not overloaded
postfix [parsing-only] `⁻¹ᵍ`:std.prec.max_plus := has_inv.inv
/- semigroup -/
structure semigroup [class] (A : Type) extends has_mul A :=
(carrier_hset : is_hset A)
(is_hset_carrier : is_hset A)
(mul_assoc : ∀a b c, mul (mul a b) c = mul a (mul b c))
attribute semigroup.carrier_hset [instance]
attribute semigroup.is_hset_carrier [instance]
theorem mul_assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
theorem mul.assoc [s : semigroup A] (a b c : A) : a * b * c = a * (b * c) :=
!semigroup.mul_assoc
structure comm_semigroup [class] (A : Type) extends semigroup A :=
(mul_comm : ∀a b, mul a b = mul b a)
theorem mul_comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
theorem mul.comm [s : comm_semigroup A] (a b : A) : a * b = b * a :=
!comm_semigroup.mul_comm
theorem mul_left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
binary.left_comm (@mul_comm A s) (@mul_assoc A s) a b c
theorem mul.left_comm [s : comm_semigroup A] (a b c : A) : a * (b * c) = b * (a * c) :=
binary.left_comm (@mul.comm A s) (@mul.assoc A s) a b c
theorem mul_right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
binary.right_comm (@mul_comm A s) (@mul_assoc A s) a b c
theorem mul.right_comm [s : comm_semigroup A] (a b c : A) : (a * b) * c = (a * c) * b :=
binary.right_comm (@mul.comm A s) (@mul.assoc A s) a b c
structure left_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_left_cancel : ∀a b c, mul a b = mul a c → b = c)
theorem mul_left_cancel [s : left_cancel_semigroup A] {a b c : A} :
theorem mul.left_cancel [s : left_cancel_semigroup A] {a b c : A} :
a * b = a * c → b = c :=
!left_cancel_semigroup.mul_left_cancel
structure right_cancel_semigroup [class] (A : Type) extends semigroup A :=
(mul_right_cancel : ∀a b c, mul a b = mul c b → a = c)
theorem mul_right_cancel [s : right_cancel_semigroup A] {a b c : A} :
theorem mul.right_cancel [s : right_cancel_semigroup A] {a b c : A} :
a * b = c * b → a = c :=
!right_cancel_semigroup.mul_right_cancel
/- additive semigroup -/
structure add_semigroup [class] (A : Type) extends has_add A :=
(add_assoc : ∀a b c, add (add a b) c = add a (add b c))
theorem add_assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
theorem add.assoc [s : add_semigroup A] (a b c : A) : a + b + c = a + (b + c) :=
!add_semigroup.add_assoc
structure add_comm_semigroup [class] (A : Type) extends add_semigroup A :=
(add_comm : ∀a b, add a b = add b a)
theorem add_comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
theorem add.comm [s : add_comm_semigroup A] (a b : A) : a + b = b + a :=
!add_comm_semigroup.add_comm
theorem add_left_comm [s : add_comm_semigroup A] (a b c : A) :
theorem add.left_comm [s : add_comm_semigroup A] (a b c : A) :
a + (b + c) = b + (a + c) :=
binary.left_comm (@add_comm A s) (@add_assoc A s) a b c
binary.left_comm (@add.comm A s) (@add.assoc A s) a b c
theorem add_right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
binary.right_comm (@add_comm A s) (@add_assoc A s) a b c
theorem add.right_comm [s : add_comm_semigroup A] (a b c : A) : (a + b) + c = (a + c) + b :=
binary.right_comm (@add.comm A s) (@add.assoc A s) a b c
structure add_left_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_left_cancel : ∀a b c, add a b = add a c → b = c)
theorem add_left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
theorem add.left_cancel [s : add_left_cancel_semigroup A] {a b c : A} :
a + b = a + c → b = c :=
!add_left_cancel_semigroup.add_left_cancel
structure add_right_cancel_semigroup [class] (A : Type) extends add_semigroup A :=
(add_right_cancel : ∀a b c, add a b = add c b → a = c)
theorem add_right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
theorem add.right_cancel [s : add_right_cancel_semigroup A] {a b c : A} :
a + b = c + b → a = c :=
!add_right_cancel_semigroup.add_right_cancel
@ -130,7 +129,6 @@ theorem mul_one [s : monoid A] (a : A) : a * 1 = a := !monoid.mul_one
structure comm_monoid [class] (A : Type) extends monoid A, comm_semigroup A
/- additive monoid -/
structure add_monoid [class] (A : Type) extends add_semigroup A, has_zero A :=
@ -142,8 +140,6 @@ theorem add_zero [s : add_monoid A] (a : A) : a + 0 = a := !add_monoid.add_zero
structure add_comm_monoid [class] (A : Type) extends add_monoid A, add_comm_semigroup A
/- group -/
structure group [class] (A : Type) extends monoid A, has_inv A :=
@ -156,131 +152,114 @@ section group
variable [s : group A]
include s
theorem mul_left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
theorem mul.left_inv (a : A) : a⁻¹ * a = 1 := !group.mul_left_inv
theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
calc
a⁻¹ * (a * b) = a⁻¹ * a * b : mul_assoc
... = 1 * b : mul_left_inv
... = b : one_mul
by rewrite [-mul.assoc, mul.left_inv, one_mul]
theorem inv_mul_cancel_right (a b : A) : a * b⁻¹ * b = a :=
calc
a * b⁻¹ * b = a * (b⁻¹ * b) : mul_assoc
... = a * 1 : mul_left_inv
... = a : mul_one
by rewrite [mul.assoc, mul.left_inv, mul_one]
theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
calc
a⁻¹ = a⁻¹ * 1 : mul_one
... = a⁻¹ * (a * b) : H
... = b : inv_mul_cancel_left
by rewrite [-mul_one a⁻¹, -H, inv_mul_cancel_left]
theorem inv_one : 1⁻¹ = 1 := inv_eq_of_mul_eq_one (one_mul 1)
theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul_left_inv a)
theorem inv_inv (a : A) : (a⁻¹)⁻¹ = a := inv_eq_of_mul_eq_one (mul.left_inv a)
theorem inv_inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
calc
a = (a⁻¹)⁻¹ : inv_inv
... = b : inv_eq_of_mul_eq_one (H⁻¹ ▸ (mul_left_inv _))
theorem inv.inj {a b : A} (H : a⁻¹ = b⁻¹) : a = b :=
by rewrite [-inv_inv, H, inv_inv]
--theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
--iff.intro (assume H, inv_inj H) (assume H, congr_arg _ H)
theorem inv_eq_inv_iff_eq (a b : A) : a⁻¹ = b⁻¹ ↔ a = b :=
iff.intro (assume H, inv.inj H) (assume H, ap _ H)
--theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
--inv_one ▸ !inv_eq_inv_iff_eq
theorem inv_eq_one_iff_eq_one (a b : A) : a⁻¹ = 1 ↔ a = 1 :=
inv_one ▸ inv_eq_inv_iff_eq a 1
theorem eq_inv_imp_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
H⁻¹ ▸ (inv_inv b)⁻¹
theorem eq_inv_of_eq_inv {a b : A} (H : a = b⁻¹) : b = a⁻¹ :=
by rewrite [H, inv_inv]
--theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
--iff.intro !eq_inv_imp_eq_inv !eq_inv_imp_eq_inv
theorem eq_inv_iff_eq_inv (a b : A) : a = b⁻¹ ↔ b = a⁻¹ :=
iff.intro !eq_inv_of_eq_inv !eq_inv_of_eq_inv
theorem mul_right_inv (a : A) : a * a⁻¹ = 1 :=
theorem mul.right_inv (a : A) : a * a⁻¹ = 1 :=
calc
a * a⁻¹ = (a⁻¹)⁻¹ * a⁻¹ : inv_inv
... = 1 : mul_left_inv
... = 1 : mul.left_inv
theorem mul_inv_cancel_left (a b : A) : a * (a⁻¹ * b) = b :=
calc
a * (a⁻¹ * b) = a * a⁻¹ * b : mul_assoc
... = 1 * b : mul_right_inv
... = b : one_mul
a * (a⁻¹ * b) = a * a⁻¹ * b : by rewrite mul.assoc
... = 1 * b : mul.right_inv
... = b : one_mul
theorem mul_inv_cancel_right (a b : A) : a * b * b⁻¹ = a :=
calc
a * b * b⁻¹ = a * (b * b⁻¹) : mul_assoc
... = a * 1 : mul_right_inv
a * b * b⁻¹ = a * (b * b⁻¹) : mul.assoc
... = a * 1 : mul.right_inv
... = a : mul_one
theorem inv_mul (a b : A) : (a * b)⁻¹ = b⁻¹ * a⁻¹ :=
inv_eq_of_mul_eq_one
(calc
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul_assoc
... = a * a⁻¹ : mul_inv_cancel_left
... = 1 : mul_right_inv)
a * b * (b⁻¹ * a⁻¹) = a * (b * (b⁻¹ * a⁻¹)) : mul.assoc
... = a * a⁻¹ : mul_inv_cancel_left
... = 1 : mul.right_inv)
theorem eq_of_mul_inv_eq_one {a b : A} (H : a * b⁻¹ = 1) : a = b :=
calc
a = a * b⁻¹ * b : inv_mul_cancel_right
... = 1 * b : H
... = b : one_mul
a = a * b⁻¹ * b : by rewrite inv_mul_cancel_right
... = 1 * b : H
... = b : one_mul
-- TODO: better names for the next eight theorems? (Also for additive ones.)
theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * b = c) : a = c * b⁻¹ :=
H ▸ !mul_inv_cancel_right⁻¹
theorem eq_mul_inv_of_mul_eq {a b c : A} (H : a * c = b) : a = b * c⁻¹ :=
by rewrite [-H, mul_inv_cancel_right]
theorem eq_inv_mul_of_mul_eq {a b c : A} (H : a * b = c) : b = a⁻¹ * c :=
H ▸ !inv_mul_cancel_left⁻¹
theorem eq_inv_mul_of_mul_eq {a b c : A} (H : b * a = c) : a = b⁻¹ * c :=
by rewrite [-H, inv_mul_cancel_left]
theorem inv_mul_eq_of_eq_mul {a b c : A} (H : a = b * c) : b⁻¹ * a = c :=
H⁻¹ ▸ !inv_mul_cancel_left
theorem inv_mul_eq_of_eq_mul {a b c : A} (H : b = a * c) : a⁻¹ * b = c :=
by rewrite [H, inv_mul_cancel_left]
theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = b * c) : a * c⁻¹ = b :=
H⁻¹ ▸ !mul_inv_cancel_right
theorem mul_inv_eq_of_eq_mul {a b c : A} (H : a = c * b) : a * b⁻¹ = c :=
by rewrite [H, mul_inv_cancel_right]
theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * b⁻¹ = c) : a = c * b :=
theorem eq_mul_of_mul_inv_eq {a b c : A} (H : a * c⁻¹ = b) : a = b * c :=
!inv_inv ▸ (eq_mul_inv_of_mul_eq H)
theorem eq_mul_of_inv_mul_eq {a b c : A} (H : a⁻¹ * b = c) : b = a * c :=
theorem eq_mul_of_inv_mul_eq {a b c : A} (H : b⁻¹ * a = c) : a = b * c :=
!inv_inv ▸ (eq_inv_mul_of_mul_eq H)
theorem mul_eq_of_eq_inv_mul {a b c : A} (H : a = b⁻¹ * c) : b * a = c :=
theorem mul_eq_of_eq_inv_mul {a b c : A} (H : b = a⁻¹ * c) : a * b = c :=
!inv_inv ▸ (inv_mul_eq_of_eq_mul H)
theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = b * c⁻¹) : a * c = b :=
theorem mul_eq_of_eq_mul_inv {a b c : A} (H : a = c * b⁻¹) : a * b = c :=
!inv_inv ▸ (mul_inv_eq_of_eq_mul H)
--theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
--iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
theorem mul_eq_iff_eq_inv_mul (a b c : A) : a * b = c ↔ b = a⁻¹ * c :=
iff.intro eq_inv_mul_of_mul_eq mul_eq_of_eq_inv_mul
--theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
--iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
theorem mul_eq_iff_eq_mul_inv (a b c : A) : a * b = c ↔ a = c * b⁻¹ :=
iff.intro eq_mul_inv_of_mul_eq mul_eq_of_eq_mul_inv
definition group.to_left_cancel_semigroup [instance] : left_cancel_semigroup A :=
left_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b = a * c,
calc
b = a⁻¹ * (a * b) : inv_mul_cancel_left
... = a⁻¹ * (a * c) : H
... = c : inv_mul_cancel_left)
theorem mul_left_cancel {a b c : A} (H : a * b = a * c) : b = c :=
by rewrite [-inv_mul_cancel_left a b, H, inv_mul_cancel_left]
definition group.to_right_cancel_semigroup [instance] : right_cancel_semigroup A :=
right_cancel_semigroup.mk (@group.mul A s) (@group.carrier_hset A s) (@group.mul_assoc A s)
(take a b c,
assume H : a * b = c * b,
calc
a = (a * b) * b⁻¹ : mul_inv_cancel_right
... = (c * b) * b⁻¹ : H
... = c : mul_inv_cancel_right)
theorem mul_right_cancel {a b c : A} (H : a * b = c * b) : a = c :=
by rewrite [-mul_inv_cancel_right a b, H, mul_inv_cancel_right]
definition group.to_left_cancel_semigroup [instance] [coercion] [reducible] : left_cancel_semigroup A :=
⦃ left_cancel_semigroup, s,
mul_left_cancel := @mul_left_cancel A s ⦄
definition group.to_right_cancel_semigroup [instance] [coercion] [reducible] : right_cancel_semigroup A :=
⦃ right_cancel_semigroup, s,
mul_right_cancel := @mul_right_cancel A s ⦄
end group
structure comm_group [class] (A : Type) extends group A, comm_monoid A
/- additive group -/
structure add_group [class] (A : Type) extends add_monoid A, has_neg A :=
@ -291,120 +270,108 @@ section add_group
variables [s : add_group A]
include s
theorem add_left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
theorem add.left_inv (a : A) : -a + a = 0 := !add_group.add_left_inv
theorem neg_add_cancel_left (a b : A) : -a + (a + b) = b :=
calc
-a + (a + b) = -a + a + b : add_assoc
... = 0 + b : add_left_inv
... = b : zero_add
by rewrite [-add.assoc, add.left_inv, zero_add]
theorem neg_add_cancel_right (a b : A) : a + -b + b = a :=
calc
a + -b + b = a + (-b + b) : add_assoc
... = a + 0 : add_left_inv
... = a : add_zero
by rewrite [add.assoc, add.left_inv, add_zero]
theorem neq_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
calc
-a = -a + 0 : add_zero
... = -a + (a + b) : H
... = b : neg_add_cancel_left
theorem neg_eq_of_add_eq_zero {a b : A} (H : a + b = 0) : -a = b :=
by rewrite [-add_zero, -H, neg_add_cancel_left]
theorem neg_zero : -0 = 0 := neq_eq_of_add_eq_zero (zero_add 0)
theorem neg_zero : -0 = 0 := neg_eq_of_add_eq_zero (zero_add 0)
theorem neg_neg (a : A) : -(-a) = a := neq_eq_of_add_eq_zero (add_left_inv a)
theorem neg_neg (a : A) : -(-a) = a := neg_eq_of_add_eq_zero (add.left_inv a)
theorem neg_inj {a b : A} (H : -a = -b) : a = b :=
theorem eq_neg_of_add_eq_zero {a b : A} (H : a + b = 0) : a = -b :=
by rewrite [-neg_eq_of_add_eq_zero H, neg_neg]
theorem neg.inj {a b : A} (H : -a = -b) : a = b :=
calc
a = -(-a) : neg_neg
... = b : neq_eq_of_add_eq_zero (H⁻¹ ▸ (add_left_inv _))
... = b : neg_eq_of_add_eq_zero (H⁻¹ ▸ (add.left_inv _))
--theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
--iff.intro (assume H, neg_inj H) (assume H, congr_arg _ H)
theorem neg_eq_neg_iff_eq (a b : A) : -a = -b ↔ a = b :=
iff.intro (assume H, neg.inj H) (assume H, ap _ H)
--theorem neg_eq_zero_iff_eq_zero (a b : A) : -a = 0 ↔ a = 0 :=
--neg_zero ▸ !neg_eq_neg_iff_eq
theorem neg_eq_zero_iff_eq_zero (a : A) : -a = 0 ↔ a = 0 :=
neg_zero ▸ !neg_eq_neg_iff_eq
theorem eq_neq_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
theorem eq_neg_of_eq_neg {a b : A} (H : a = -b) : b = -a :=
H⁻¹ ▸ (neg_neg b)⁻¹
--theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
--iff.intro !eq_neq_of_eq_neg !eq_neq_of_eq_neg
theorem eq_neg_iff_eq_neg (a b : A) : a = -b ↔ b = -a :=
iff.intro !eq_neg_of_eq_neg !eq_neg_of_eq_neg
theorem add_right_inv (a : A) : a + -a = 0 :=
theorem add.right_inv (a : A) : a + -a = 0 :=
calc
a + -a = -(-a) + -a : neg_neg
... = 0 : add_left_inv
... = 0 : add.left_inv
theorem add_neg_cancel_left (a b : A) : a + (-a + b) = b :=
calc
a + (-a + b) = a + -a + b : add_assoc
... = 0 + b : add_right_inv
... = b : zero_add
by rewrite [-add.assoc, add.right_inv, zero_add]
theorem add_neg_cancel_right (a b : A) : a + b + -b = a :=
calc
a + b + -b = a + (b + -b) : add_assoc
... = a + 0 : add_right_inv
... = a : add_zero
by rewrite [add.assoc, add.right_inv, add_zero]
theorem neq_add_rev (a b : A) : -(a + b) = -b + -a :=
neq_eq_of_add_eq_zero
(calc
a + b + (-b + -a) = a + (b + (-b + -a)) : add_assoc
... = a + -a : add_neg_cancel_left
... = 0 : add_right_inv)
theorem neg_add_rev (a b : A) : -(a + b) = -b + -a :=
neg_eq_of_add_eq_zero
begin
rewrite [add.assoc, add_neg_cancel_left, add.right_inv]
end
theorem eq_add_neq_of_add_eq {a b c : A} (H : a + b = c) : a = c + -b :=
-- TODO: delete these in favor of sub rules?
theorem eq_add_neg_of_add_eq {a b c : A} (H : a + c = b) : a = b + -c :=
H ▸ !add_neg_cancel_right⁻¹
theorem eq_neg_add_of_add_eq {a b c : A} (H : a + b = c) : b = -a + c :=
theorem eq_neg_add_of_add_eq {a b c : A} (H : b + a = c) : a = -b + c :=
H ▸ !neg_add_cancel_left⁻¹
theorem neg_add_eq_of_eq_add {a b c : A} (H : a = b + c) : -b + a = c :=
theorem neg_add_eq_of_eq_add {a b c : A} (H : b = a + c) : -a + b = c :=
H⁻¹ ▸ !neg_add_cancel_left
theorem add_neg_eq_of_eq_add {a b c : A} (H : a = b + c) : a + -c = b :=
theorem add_neg_eq_of_eq_add {a b c : A} (H : a = c + b) : a + -b = c :=
H⁻¹ ▸ !add_neg_cancel_right
theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -b = c) : a = c + b :=
!neg_neg ▸ (eq_add_neq_of_add_eq H)
theorem eq_add_of_add_neg_eq {a b c : A} (H : a + -c = b) : a = b + c :=
!neg_neg ▸ (eq_add_neg_of_add_eq H)
theorem eq_add_of_neg_add_eq {a b c : A} (H : -a + b = c) : b = a + c :=
theorem eq_add_of_neg_add_eq {a b c : A} (H : -b + a = c) : a = b + c :=
!neg_neg ▸ (eq_neg_add_of_add_eq H)
theorem add_eq_of_eq_neg_add {a b c : A} (H : a = -b + c) : b + a = c :=
theorem add_eq_of_eq_neg_add {a b c : A} (H : b = -a + c) : a + b = c :=
!neg_neg ▸ (neg_add_eq_of_eq_add H)
theorem add_eq_of_eq_add_neg {a b c : A} (H : a = b + -c) : a + c = b :=
theorem add_eq_of_eq_add_neg {a b c : A} (H : a = c + -b) : a + b = c :=
!neg_neg ▸ (add_neg_eq_of_eq_add H)
--theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
--iff.intro eq_neg_add_of_add_eq add_eq_of_eq_neg_add
theorem add_eq_iff_eq_neg_add (a b c : A) : a + b = c ↔ b = -a + c :=
iff.intro eq_neg_add_of_add_eq add_eq_of_eq_neg_add
--theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
--iff.intro eq_add_neq_of_add_eq add_eq_of_eq_add_neg
theorem add_eq_iff_eq_add_neg (a b c : A) : a + b = c ↔ a = c + -b :=
iff.intro eq_add_neg_of_add_eq add_eq_of_eq_add_neg
definition add_group.to_left_cancel_semigroup [instance] :
theorem add_left_cancel {a b c : A} (H : a + b = a + c) : b = c :=
calc b = -a + (a + b) : !neg_add_cancel_left⁻¹
... = -a + (a + c) : H
... = c : neg_add_cancel_left
theorem add_right_cancel {a b c : A} (H : a + b = c + b) : a = c :=
calc a = (a + b) + -b : !add_neg_cancel_right⁻¹
... = (c + b) + -b : H
... = c : add_neg_cancel_right
definition add_group.to_left_cancel_semigroup [instance] [coercion] [reducible] :
add_left_cancel_semigroup A :=
add_left_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
assume H : a + b = a + c,
calc
b = -a + (a + b) : neg_add_cancel_left
... = -a + (a + c) : H
... = c : neg_add_cancel_left)
⦃ add_left_cancel_semigroup, s,
add_left_cancel := @add_left_cancel A s ⦄
definition add_group.to_add_right_cancel_semigroup [instance] :
definition add_group.to_add_right_cancel_semigroup [instance] [coercion] [reducible] :
add_right_cancel_semigroup A :=
add_right_cancel_semigroup.mk (@add_group.add A s) (@add_group.add_assoc A s)
(take a b c,
assume H : a + b = c + b,
calc
a = (a + b) + -b : add_neg_cancel_right
... = (c + b) + -b : H
... = c : add_neg_cancel_right)
⦃ add_right_cancel_semigroup, s,
add_right_cancel := @add_right_cancel A s ⦄
/- sub -/
@ -413,7 +380,9 @@ section add_group
infix `-` := sub
theorem sub_self (a : A) : a - a = 0 := !add_right_inv
theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
theorem sub_self (a : A) : a - a = 0 := !add.right_inv
theorem sub_add_cancel (a b : A) : a - b + b = a := !neg_add_cancel_right
@ -421,79 +390,92 @@ section add_group
theorem eq_of_sub_eq_zero {a b : A} (H : a - b = 0) : a = b :=
calc
a = (a - b) + b : sub_add_cancel
a = (a - b) + b : !sub_add_cancel⁻¹
... = 0 + b : H
... = b : zero_add
--theorem eq_iff_minus_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
--iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
theorem eq_iff_sub_eq_zero (a b : A) : a = b ↔ a - b = 0 :=
iff.intro (assume H, H ▸ !sub_self) (assume H, eq_of_sub_eq_zero H)
theorem zero_sub (a : A) : 0 - a = -a := !zero_add
theorem sub_zero (a : A) : a - 0 = a := neg_zero⁻¹ ▸ !add_zero
theorem sub_zero (a : A) : a - 0 = a := subst (eq.symm neg_zero) !add_zero
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ idp
theorem sub_neg_eq_add (a b : A) : a - (-b) = a + b := !neg_neg ▸ rfl
theorem neg_sub (a b : A) : -(a - b) = b - a :=
neq_eq_of_add_eq_zero
neg_eq_of_add_eq_zero
(calc
a - b + (b - a) = a - b + b - a : add_assoc
... = a - a : sub_add_cancel
... = 0 : sub_self)
a - b + (b - a) = a - b + b - a : by rewrite -add.assoc
... = a - a : sub_add_cancel
... = 0 : sub_self)
theorem add_sub (a b c : A) : a + (b - c) = a + b - c := !add_assoc⁻¹
theorem add_sub (a b c : A) : a + (b - c) = a + b - c := !add.assoc⁻¹
theorem sub_add_eq_sub_sub_swap (a b c : A) : a - (b + c) = a - c - b :=
calc
a - (b + c) = a + (-c - b) : neq_add_rev
... = a - c - b : add_assoc
a - (b + c) = a + (-c - b) : neg_add_rev
... = a - c - b : by rewrite add.assoc
--theorem minus_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
--iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)
theorem sub_eq_iff_eq_add (a b c : A) : a - b = c ↔ a = c + b :=
iff.intro (assume H, eq_add_of_add_neg_eq H) (assume H, add_neg_eq_of_eq_add H)
--theorem eq_minus_iff_add_eq (a b c : A) : a = b - c ↔ a + c = b :=
--iff.intro (assume H, add_eq_of_eq_add_neg H) (assume H, eq_add_neq_of_add_eq H)
theorem eq_sub_iff_add_eq (a b c : A) : a = b - c ↔ a + c = b :=
iff.intro (assume H, add_eq_of_eq_add_neg H) (assume H, eq_add_neg_of_add_eq H)
--theorem minus_eq_minus_iff {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
--calc
-- a = b ↔ a - b = 0 : eq_iff_minus_eq_zero
-- ... ↔ c - d = 0 : H ▸ !iff.refl
-- ... ↔ c = d : iff.symm (eq_iff_minus_eq_zero c d)
theorem eq_iff_eq_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a = b ↔ c = d :=
calc
a = b ↔ a - b = 0 : eq_iff_sub_eq_zero
... = (c - d = 0) : H
... ↔ c = d : iff.symm (eq_iff_sub_eq_zero c d)
theorem eq_sub_of_add_eq {a b c : A} (H : a + c = b) : a = b - c :=
!eq_add_neg_of_add_eq H
theorem sub_eq_of_eq_add {a b c : A} (H : a = c + b) : a - b = c :=
!add_neg_eq_of_eq_add H
theorem eq_add_of_sub_eq {a b c : A} (H : a - c = b) : a = b + c :=
eq_add_of_add_neg_eq H
theorem add_eq_of_eq_sub {a b c : A} (H : a = c - b) : a + b = c :=
add_eq_of_eq_add_neg H
end add_group
structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
section add_comm_group
variable [s : add_comm_group A]
include s
variable [s : add_comm_group A]
include s
theorem sub_add_eq_sub_sub (a b c : A) : a - (b + c) = a - b - c :=
!add_comm ▸ !sub_add_eq_sub_sub_swap
!add.comm ▸ !sub_add_eq_sub_sub_swap
theorem neq_add_eq_sub (a b : A) : -a + b = b - a := !add_comm
theorem neg_add_eq_sub (a b : A) : -a + b = b - a := !add.comm
theorem neg_add_distrib (a b : A) : -(a + b) = -a + -b := !add_comm ▸ !neq_add_rev
theorem neg_add (a b : A) : -(a + b) = -a + -b := add.comm (-b) (-a) ▸ neg_add_rev a b
theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add_right_comm
theorem sub_add_eq_add_sub (a b c : A) : a - b + c = a + c - b := !add.right_comm
theorem sub_sub (a b c : A) : a - b - c = a - (b + c) :=
calc
a - b - c = a + (-b + -c) : add_assoc
... = a + -(b + c) : neg_add_distrib
... = a - (b + c) : idp
by rewrite [▸ a + -b + -c = _, add.assoc, -neg_add]
theorem add_sub_add_left_eq_sub (a b c : A) : (c + a) - (c + b) = a - b :=
calc
(c + a) - (c + b) = c + a - c - b : sub_add_eq_sub_sub
... = a + c - c - b : add_comm a c
... = a - b : add_sub_cancel
by rewrite [sub_add_eq_sub_sub, (add.comm c a), add_sub_cancel]
theorem eq_sub_of_add_eq' {a b c : A} (H : c + a = b) : a = b - c :=
!eq_sub_of_add_eq (!add.comm ▸ H)
theorem sub_eq_of_eq_add' {a b c : A} (H : a = b + c) : a - b = c :=
!sub_eq_of_eq_add (!add.comm ▸ H)
theorem eq_add_of_sub_eq' {a b c : A} (H : a - b = c) : a = b + c :=
!add.comm ▸ eq_add_of_sub_eq H
theorem add_eq_of_eq_sub' {a b c : A} (H : b = c - a) : a + b = c :=
!add.comm ▸ add_eq_of_eq_sub H
end add_comm_group
/- bundled structures -/
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
@ -567,4 +549,4 @@ structure AddCommGroup :=
attribute AddCommGroup.carrier [coercion]
attribute AddCommGroup.struct [instance]
end path_algebra
end algebra

355
hott/algebra/order.hlean Normal file
View file

@ -0,0 +1,355 @@
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.order
Author: Jeremy Avigad
Various types of orders. We develop weak orders "≤" and strict orders "<" separately. We also
consider structures with both, where the two are related by
x < y ↔ (x ≤ y × x ≠ y) (order_pair)
x ≤ y ↔ (x < y ⊎ x = y) (strong_order_pair)
These might not hold constructively in some applications, but we can define additional structures
with both < and ≤ as needed.
Ported from the standard library
-/
--import logic.eq logic.connectives
open core prod
namespace algebra
variable {A : Type}
/- overloaded symbols -/
structure has_le.{l} [class] (A : Type.{l}) : Type.{l+1} :=
(le : A → A → Type.{l})
structure has_lt [class] (A : Type) :=
(lt : A → A → Type₀)
infixl `<=` := has_le.le
infixl `≤` := has_le.le
infixl `<` := has_lt.lt
definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a
notation a ≥ b := has_le.ge a b
notation a >= b := has_le.ge a b
definition has_lt.gt [reducible] {A : Type} [s : has_lt A] (a b : A) := b < a
notation a > b := has_lt.gt a b
/- weak orders -/
structure weak_order [class] (A : Type) extends has_le A :=
(le_refl : Πa, le a a)
(le_trans : Πa b c, le a b → le b c → le a c)
(le_antisymm : Πa b, le a b → le b a → a = b)
section
variable [s : weak_order A]
include s
definition le.refl (a : A) : a ≤ a := !weak_order.le_refl
definition le.trans [trans] {a b c : A} : a ≤ b → b ≤ c → a ≤ c := !weak_order.le_trans
definition ge.trans [trans] {a b c : A} (H1 : a ≥ b) (H2: b ≥ c) : a ≥ c := le.trans H2 H1
definition le.antisymm {a b : A} : a ≤ b → b ≤ a → a = b := !weak_order.le_antisymm
end
structure linear_weak_order [class] (A : Type) extends weak_order A : Type :=
(le_total : Πa b, le a b ⊎ le b a)
definition le.total [s : linear_weak_order A] (a b : A) : a ≤ b ⊎ b ≤ a :=
!linear_weak_order.le_total
/- strict orders -/
structure strict_order [class] (A : Type) extends has_lt A :=
(lt_irrefl : Πa, ¬ lt a a)
(lt_trans : Πa b c, lt a b → lt b c → lt a c)
section
variable [s : strict_order A]
include s
definition lt.irrefl (a : A) : ¬ a < a := !strict_order.lt_irrefl
definition lt.trans [trans] {a b c : A} : a < b → b < c → a < c := !strict_order.lt_trans
definition gt.trans [trans] {a b c : A} (H1 : a > b) (H2: b > c) : a > c := lt.trans H2 H1
definition ne_of_lt {a b : A} (lt_ab : a < b) : a ≠ b :=
assume eq_ab : a = b,
show empty, from lt.irrefl b (eq_ab ▸ lt_ab)
definition ne_of_gt {a b : A} (gt_ab : a > b) : a ≠ b :=
ne.symm (ne_of_lt gt_ab)
definition lt.asymm {a b : A} (H : a < b) : ¬ b < a :=
assume H1 : b < a, lt.irrefl _ (lt.trans H H1)
end
/- well-founded orders -/
-- TODO: do these duplicate what Leo has done? if so, eliminate
structure wf_strict_order [class] (A : Type) extends strict_order A :=
(wf_rec : ΠP : A → Type, (Πx, (Πy, lt y x → P y) → P x) → Πx, P x)
definition wf.rec_on {A : Type} [s : wf_strict_order A] {P : A → Type}
(x : A) (H : Πx, (Πy, wf_strict_order.lt y x → P y) → P x) : P x :=
wf_strict_order.wf_rec P H x
definition wf.ind_on := @wf.rec_on
/- structures with a weak and a strict order -/
structure order_pair [class] (A : Type) extends weak_order A, has_lt A :=
(lt_iff_le_and_ne : Πa b, lt a b ↔ (le a b × a ≠ b))
section
variable [s : order_pair A]
variables {a b c : A}
include s
definition lt_iff_le_and_ne : a < b ↔ (a ≤ b × a ≠ b) :=
!order_pair.lt_iff_le_and_ne
definition le_of_lt (H : a < b) : a ≤ b :=
pr1 (iff.mp lt_iff_le_and_ne H)
definition lt_of_le_of_ne (H1 : a ≤ b) (H2 : a ≠ b) : a < b :=
iff.mp (iff.symm lt_iff_le_and_ne) (pair H1 H2)
private definition lt_irrefl (s' : order_pair A) (a : A) : ¬ a < a :=
assume H : a < a,
have H1 : a ≠ a, from pr2 (iff.mp !lt_iff_le_and_ne H),
H1 rfl
private definition lt_trans (s' : order_pair A) (a b c: A) (lt_ab : a < b) (lt_bc : b < c) : a < c :=
have le_ab : a ≤ b, from le_of_lt lt_ab,
have le_bc : b ≤ c, from le_of_lt lt_bc,
have le_ac : a ≤ c, from le.trans le_ab le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le.antisymm le_ab le_ba,
have ne_ab : a ≠ b, from pr2 (iff.mp lt_iff_le_and_ne lt_ab),
ne_ab eq_ab,
show a < c, from lt_of_le_of_ne le_ac ne_ac
definition order_pair.to_strict_order [instance] [coercion] [reducible] : strict_order A :=
⦃ strict_order, s, lt_irrefl := lt_irrefl s, lt_trans := lt_trans s ⦄
definition lt_of_lt_of_le [trans] : a < b → b ≤ c → a < c :=
assume lt_ab : a < b,
assume le_bc : b ≤ c,
have le_ac : a ≤ c, from le.trans (le_of_lt lt_ab) le_bc,
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_ba : b ≤ a, from eq_ac⁻¹ ▸ le_bc,
have eq_ab : a = b, from le.antisymm (le_of_lt lt_ab) le_ba,
show empty, from ne_of_lt lt_ab eq_ab,
show a < c, from lt_of_le_of_ne le_ac ne_ac
definition lt_of_le_of_lt [trans] : a ≤ b → b < c → a < c :=
assume le_ab : a ≤ b,
assume lt_bc : b < c,
have le_ac : a ≤ c, from le.trans le_ab (le_of_lt lt_bc),
have ne_ac : a ≠ c, from
assume eq_ac : a = c,
have le_cb : c ≤ b, from eq_ac ▸ le_ab,
have eq_bc : b = c, from le.antisymm (le_of_lt lt_bc) le_cb,
show empty, from ne_of_lt lt_bc eq_bc,
show a < c, from lt_of_le_of_ne le_ac ne_ac
definition gt_of_gt_of_ge [trans] (H1 : a > b) (H2 : b ≥ c) : a > c := lt_of_le_of_lt H2 H1
definition gt_of_ge_of_gt [trans] (H1 : a ≥ b) (H2 : b > c) : a > c := lt_of_lt_of_le H2 H1
definition not_le_of_lt (H : a < b) : ¬ b ≤ a :=
assume H1 : b ≤ a,
lt.irrefl _ (lt_of_lt_of_le H H1)
definition not_lt_of_le (H : a ≤ b) : ¬ b < a :=
assume H1 : b < a,
lt.irrefl _ (lt_of_le_of_lt H H1)
end
structure strong_order_pair [class] (A : Type) extends order_pair A :=
(le_iff_lt_or_eq : Πa b, le a b ↔ lt a b ⊎ a = b)
definition le_iff_lt_or_eq [s : strong_order_pair A] {a b : A} : a ≤ b ↔ a < b ⊎ a = b :=
!strong_order_pair.le_iff_lt_or_eq
definition lt_or_eq_of_le [s : strong_order_pair A] {a b : A} (le_ab : a ≤ b) : a < b ⊎ a = b :=
iff.mp le_iff_lt_or_eq le_ab
-- We can also construct a strong order pair by defining a strict order, and then defining
-- x ≤ y ↔ x < y ⊎ x = y
structure strict_order_with_le [class] (A : Type) extends strict_order A, has_le A :=
(le_iff_lt_or_eq : Πa b, le a b ↔ lt a b ⊎ a = b)
private definition le_refl (s : strict_order_with_le A) (a : A) : a ≤ a :=
iff.mp (iff.symm !strict_order_with_le.le_iff_lt_or_eq) (sum.inr rfl)
private definition le_trans (s : strict_order_with_le A) (a b c : A) (le_ab : a ≤ b) (le_bc : b ≤ c) : a ≤ c :=
sum.rec_on (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
(assume lt_ab : a < b,
sum.rec_on (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_bc)
(assume lt_bc : b < c,
iff.elim_right
!strict_order_with_le.le_iff_lt_or_eq (sum.inl (lt.trans lt_ab lt_bc)))
(assume eq_bc : b = c, eq_bc ▸ le_ab))
(assume eq_ab : a = b,
eq_ab⁻¹ ▸ le_bc)
private definition le_antisymm (s : strict_order_with_le A) (a b : A) (le_ab : a ≤ b) (le_ba : b ≤ a) : a = b :=
sum.rec_on (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ab)
(assume lt_ab : a < b,
sum.rec_on (iff.mp !strict_order_with_le.le_iff_lt_or_eq le_ba)
(assume lt_ba : b < a, absurd (lt.trans lt_ab lt_ba) (lt.irrefl a))
(assume eq_ba : b = a, eq_ba⁻¹))
(assume eq_ab : a = b, eq_ab)
private definition lt_iff_le_ne (s : strict_order_with_le A) (a b : A) : a < b ↔ a ≤ b × a ≠ b :=
iff.intro
(assume lt_ab : a < b,
have le_ab : a ≤ b, from
iff.elim_right !strict_order_with_le.le_iff_lt_or_eq (sum.inl lt_ab),
show a ≤ b × a ≠ b, from pair le_ab (ne_of_lt lt_ab))
(assume H : a ≤ b × a ≠ b,
have H1 : a < b ⊎ a = b, from
iff.mp !strict_order_with_le.le_iff_lt_or_eq (pr1 H),
show a < b, from sum_resolve_left H1 (pr2 H))
definition strict_order_with_le.to_order_pair [instance] [coercion] [reducible] [s : strict_order_with_le A] :
strong_order_pair A :=
⦃ strong_order_pair, s,
le_refl := le_refl s,
le_trans := le_trans s,
le_antisymm := le_antisymm s,
lt_iff_le_and_ne := lt_iff_le_ne s ⦄
/- linear orders -/
structure linear_order_pair [class] (A : Type) extends order_pair A, linear_weak_order A
structure linear_strong_order_pair [class] (A : Type) extends strong_order_pair A,
linear_weak_order A
section
variable [s : linear_strong_order_pair A]
variables (a b c : A)
include s
definition lt.trichotomy : a < b ⊎ a = b ⊎ b < a :=
sum.rec_on (le.total a b)
(assume H : a ≤ b,
sum.rec_on (iff.mp !le_iff_lt_or_eq H) (assume H1, sum.inl H1) (assume H1, sum.inr (sum.inl H1)))
(assume H : b ≤ a,
sum.rec_on (iff.mp !le_iff_lt_or_eq H)
(assume H1, sum.inr (sum.inr H1))
(assume H1, sum.inr (sum.inl (H1⁻¹))))
definition lt.by_cases {a b : A} {P : Type}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
sum.rec_on !lt.trichotomy
(assume H, H1 H)
(assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
definition linear_strong_order_pair.to_linear_order_pair [instance] [coercion] [reducible]
: linear_order_pair A :=
⦃ linear_order_pair, s ⦄
definition le_of_not_lt {a b : A} (H : ¬ a < b) : b ≤ a :=
lt.by_cases (assume H', absurd H' H) (assume H', H' ▸ !le.refl) (assume H', le_of_lt H')
definition lt_of_not_le {a b : A} (H : ¬ a ≤ b) : b < a :=
lt.by_cases
(assume H', absurd (le_of_lt H') H)
(assume H', absurd (H' ▸ !le.refl) H)
(assume H', H')
definition lt_or_ge : a < b ⊎ a ≥ b :=
lt.by_cases
(assume H1 : a < b, sum.inl H1)
(assume H1 : a = b, sum.inr (H1 ▸ le.refl a))
(assume H1 : a > b, sum.inr (le_of_lt H1))
definition le_or_gt : a ≤ b ⊎ a > b :=
!sum.swap (lt_or_ge b a)
definition lt_or_gt_of_ne {a b : A} (H : a ≠ b) : a < b ⊎ a > b :=
lt.by_cases (assume H1, sum.inl H1) (assume H1, absurd H1 H) (assume H1, sum.inr H1)
end
structure decidable_linear_order [class] (A : Type) extends linear_strong_order_pair A :=
(decidable_lt : decidable_rel lt)
section
variable [s : decidable_linear_order A]
variables {a b c d : A}
include s
open decidable
definition decidable_lt [instance] : decidable (a < b) :=
@decidable_linear_order.decidable_lt _ _ _ _
definition decidable_le [instance] : decidable (a ≤ b) :=
by_cases
(assume H : a < b, inl (le_of_lt H))
(assume H : ¬ a < b,
have H1 : b ≤ a, from le_of_not_lt H,
by_cases
(assume H2 : b < a, inr (not_le_of_lt H2))
(assume H2 : ¬ b < a, inl (le_of_not_lt H2)))
definition decidable_eq [instance] : decidable (a = b) :=
by_cases
(assume H : a ≤ b,
by_cases
(assume H1 : b ≤ a, inl (le.antisymm H H1))
(assume H1 : ¬ b ≤ a, inr (assume H2 : a = b, H1 (H2 ▸ le.refl a))))
(assume H : ¬ a ≤ b,
(inr (assume H1 : a = b, H (H1 ▸ !le.refl))))
-- testing equality first may result in more definitional equalities
definition lt.cases {B : Type} (a b : A) (t_lt t_eq t_gt : B) : B :=
if a = b then t_eq else (if a < b then t_lt else t_gt)
definition lt.cases_of_eq {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a = b) :
lt.cases a b t_lt t_eq t_gt = t_eq := if_pos H
definition lt.cases_of_lt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a < b) :
lt.cases a b t_lt t_eq t_gt = t_lt :=
if_neg (ne_of_lt H) ⬝ if_pos H
definition lt.cases_of_gt {B : Type} {a b : A} {t_lt t_eq t_gt : B} (H : a > b) :
lt.cases a b t_lt t_eq t_gt = t_gt :=
if_neg (ne.symm (ne_of_lt H)) ⬝ if_neg (lt.asymm H)
end
end algebra
/-
For reference, these are all the transitivity rules defined in this file:
calc_trans le.trans
calc_trans lt.trans
calc_trans lt_of_lt_of_le
calc_trans lt_of_le_of_lt
calc_trans ge.trans
calc_trans gt.trans
calc_trans gt_of_gt_of_ge
calc_trans gt_of_ge_of_gt
-/

View file

@ -0,0 +1,550 @@
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.ordered_group
Authors: Jeremy Avigad
Partially ordered additive groups, modeled on Isabelle's library. We could refine the structures,
but we would have to declare more inheritance paths.
Ported from the standard library
-/
import .order .group
open core
namespace algebra
variable {A : Type}
/- partially ordered monoids, such as the natural numbers -/
structure ordered_cancel_comm_monoid [class] (A : Type) extends add_comm_monoid A,
add_left_cancel_semigroup A, add_right_cancel_semigroup A, order_pair A :=
(add_le_add_left : Πa b, le a b → Πc, le (add c a) (add c b))
(le_of_add_le_add_left : Πa b c, le (add a b) (add a c) → le b c)
section
variables [s : ordered_cancel_comm_monoid A]
variables {a b c d e : A}
include s
definition add_le_add_left (H : a ≤ b) (c : A) : c + a ≤ c + b :=
!ordered_cancel_comm_monoid.add_le_add_left H c
definition add_le_add_right (H : a ≤ b) (c : A) : a + c ≤ b + c :=
(add.comm c a) ▸ (add.comm c b) ▸ (add_le_add_left H c)
definition add_le_add (Hab : a ≤ b) (Hcd : c ≤ d) : a + c ≤ b + d :=
le.trans (add_le_add_right Hab c) (add_le_add_left Hcd b)
definition add_lt_add_left (H : a < b) (c : A) : c + a < c + b :=
have H1 : c + a ≤ c + b, from add_le_add_left (le_of_lt H) c,
have H2 : c + a ≠ c + b, from
take H3 : c + a = c + b,
have H4 : a = b, from add.left_cancel H3,
ne_of_lt H H4,
lt_of_le_of_ne H1 H2
definition add_lt_add_right (H : a < b) (c : A) : a + c < b + c :=
begin
rewrite [add.comm, {b + _}add.comm],
exact (add_lt_add_left H c)
end
definition le_add_of_nonneg_right (H : b ≥ 0) : a ≤ a + b :=
begin
have H1 : a + b ≥ a + 0, from add_le_add_left H a,
rewrite add_zero at H1,
exact H1
end
definition le_add_of_nonneg_left (H : b ≥ 0) : a ≤ b + a :=
begin
have H1 : 0 + a ≤ b + a, from add_le_add_right H a,
rewrite zero_add at H1,
exact H1
end
definition add_lt_add (Hab : a < b) (Hcd : c < d) : a + c < b + d :=
lt.trans (add_lt_add_right Hab c) (add_lt_add_left Hcd b)
definition add_lt_add_of_le_of_lt (Hab : a ≤ b) (Hcd : c < d) : a + c < b + d :=
lt_of_le_of_lt (add_le_add_right Hab c) (add_lt_add_left Hcd b)
definition add_lt_add_of_lt_of_le (Hab : a < b) (Hcd : c ≤ d) : a + c < b + d :=
lt_of_lt_of_le (add_lt_add_right Hab c) (add_le_add_left Hcd b)
definition lt_add_of_pos_right (H : b > 0) : a < a + b := !add_zero ▸ add_lt_add_left H a
definition lt_add_of_pos_left (H : b > 0) : a < b + a := !zero_add ▸ add_lt_add_right H a
-- here we start using le_of_add_le_add_left.
definition le_of_add_le_add_left (H : a + b ≤ a + c) : b ≤ c :=
!ordered_cancel_comm_monoid.le_of_add_le_add_left H
definition le_of_add_le_add_right (H : a + b ≤ c + b) : a ≤ c :=
le_of_add_le_add_left (show b + a ≤ b + c, begin rewrite [add.comm, {b + _}add.comm], exact H end)
definition lt_of_add_lt_add_left (H : a + b < a + c) : b < c :=
have H1 : b ≤ c, from le_of_add_le_add_left (le_of_lt H),
have H2 : b ≠ c, from
assume H3 : b = c, lt.irrefl _ (H3 ▸ H),
lt_of_le_of_ne H1 H2
definition lt_of_add_lt_add_right (H : a + b < c + b) : a < c :=
lt_of_add_lt_add_left ((add.comm a b) ▸ (add.comm c b) ▸ H)
definition add_le_add_left_iff (a b c : A) : a + b ≤ a + c ↔ b ≤ c :=
iff.intro le_of_add_le_add_left (assume H, add_le_add_left H _)
definition add_le_add_right_iff (a b c : A) : a + b ≤ c + b ↔ a ≤ c :=
iff.intro le_of_add_le_add_right (assume H, add_le_add_right H _)
definition add_lt_add_left_iff (a b c : A) : a + b < a + c ↔ b < c :=
iff.intro lt_of_add_lt_add_left (assume H, add_lt_add_left H _)
definition add_lt_add_right_iff (a b c : A) : a + b < c + b ↔ a < c :=
iff.intro lt_of_add_lt_add_right (assume H, add_lt_add_right H _)
-- here we start using properties of zero.
definition add_nonneg (Ha : 0 ≤ a) (Hb : 0 ≤ b) : 0 ≤ a + b :=
!zero_add ▸ (add_le_add Ha Hb)
definition add_pos (Ha : 0 < a) (Hb : 0 < b) : 0 < a + b :=
!zero_add ▸ (add_lt_add Ha Hb)
definition add_pos_of_pos_of_nonneg (Ha : 0 < a) (Hb : 0 ≤ b) : 0 < a + b :=
!zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
definition add_pos_of_nonneg_of_pos (Ha : 0 ≤ a) (Hb : 0 < b) : 0 < a + b :=
!zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
definition add_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : a + b ≤ 0 :=
!zero_add ▸ (add_le_add Ha Hb)
definition add_neg (Ha : a < 0) (Hb : b < 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add Ha Hb)
definition add_neg_of_neg_of_nonpos (Ha : a < 0) (Hb : b ≤ 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add_of_lt_of_le Ha Hb)
definition add_neg_of_nonpos_of_neg (Ha : a ≤ 0) (Hb : b < 0) : a + b < 0 :=
!zero_add ▸ (add_lt_add_of_le_of_lt Ha Hb)
-- TODO: add nonpos version (will be easier with simplifier)
definition add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg
(Ha : 0 ≤ a) (Hb : 0 ≤ b) : a + b = 0 ↔ a = 0 × b = 0 :=
iff.intro
(assume Hab : a + b = 0,
have Ha' : a ≤ 0, from
calc
a = a + 0 : by rewrite add_zero
... ≤ a + b : add_le_add_left Hb
... = 0 : Hab,
have Haz : a = 0, from le.antisymm Ha' Ha,
have Hb' : b ≤ 0, from
calc
b = 0 + b : by rewrite zero_add
... ≤ a + b : add_le_add_right Ha
... = 0 : Hab,
have Hbz : b = 0, from le.antisymm Hb' Hb,
pair Haz Hbz)
(assume Hab : a = 0 × b = 0,
match Hab with
| pair Ha' Hb' := by rewrite [Ha', Hb', add_zero]
end)
definition le_add_of_nonneg_of_le (Ha : 0 ≤ a) (Hbc : b ≤ c) : b ≤ a + c :=
!zero_add ▸ add_le_add Ha Hbc
definition le_add_of_le_of_nonneg (Hbc : b ≤ c) (Ha : 0 ≤ a) : b ≤ c + a :=
!add_zero ▸ add_le_add Hbc Ha
definition lt_add_of_pos_of_le (Ha : 0 < a) (Hbc : b ≤ c) : b < a + c :=
!zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc
definition lt_add_of_le_of_pos (Hbc : b ≤ c) (Ha : 0 < a) : b < c + a :=
!add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha
definition add_le_of_nonpos_of_le (Ha : a ≤ 0) (Hbc : b ≤ c) : a + b ≤ c :=
!zero_add ▸ add_le_add Ha Hbc
definition add_le_of_le_of_nonpos (Hbc : b ≤ c) (Ha : a ≤ 0) : b + a ≤ c :=
!add_zero ▸ add_le_add Hbc Ha
definition add_lt_of_neg_of_le (Ha : a < 0) (Hbc : b ≤ c) : a + b < c :=
!zero_add ▸ add_lt_add_of_lt_of_le Ha Hbc
definition add_lt_of_le_of_neg (Hbc : b ≤ c) (Ha : a < 0) : b + a < c :=
!add_zero ▸ add_lt_add_of_le_of_lt Hbc Ha
definition lt_add_of_nonneg_of_lt (Ha : 0 ≤ a) (Hbc : b < c) : b < a + c :=
!zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
definition lt_add_of_lt_of_nonneg (Hbc : b < c) (Ha : 0 ≤ a) : b < c + a :=
!add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
definition lt_add_of_pos_of_lt (Ha : 0 < a) (Hbc : b < c) : b < a + c :=
!zero_add ▸ add_lt_add Ha Hbc
definition lt_add_of_lt_of_pos (Hbc : b < c) (Ha : 0 < a) : b < c + a :=
!add_zero ▸ add_lt_add Hbc Ha
definition add_lt_of_nonpos_of_lt (Ha : a ≤ 0) (Hbc : b < c) : a + b < c :=
!zero_add ▸ add_lt_add_of_le_of_lt Ha Hbc
definition add_lt_of_lt_of_nonpos (Hbc : b < c) (Ha : a ≤ 0) : b + a < c :=
!add_zero ▸ add_lt_add_of_lt_of_le Hbc Ha
definition add_lt_of_neg_of_lt (Ha : a < 0) (Hbc : b < c) : a + b < c :=
!zero_add ▸ add_lt_add Ha Hbc
definition add_lt_of_lt_of_neg (Hbc : b < c) (Ha : a < 0) : b + a < c :=
!add_zero ▸ add_lt_add Hbc Ha
end
-- TODO: add properties of max and min
/- partially ordered groups -/
structure ordered_comm_group [class] (A : Type) extends add_comm_group A, order_pair A :=
(add_le_add_left : Πa b, le a b → Πc, le (add c a) (add c b))
definition ordered_comm_group.le_of_add_le_add_left [s : ordered_comm_group A] {a b c : A} (H : a + b ≤ a + c) : b ≤ c :=
assert H' : -a + (a + b) ≤ -a + (a + c), from ordered_comm_group.add_le_add_left _ _ H _,
by rewrite *neg_add_cancel_left at H'; exact H'
definition ordered_comm_group.to_ordered_cancel_comm_monoid [instance] [coercion] [reducible]
[s : ordered_comm_group A] : ordered_cancel_comm_monoid A :=
⦃ ordered_cancel_comm_monoid, s,
add_left_cancel := @add.left_cancel A s,
add_right_cancel := @add.right_cancel A s,
le_of_add_le_add_left := @ordered_comm_group.le_of_add_le_add_left A s ⦄
section
variables [s : ordered_comm_group A] (a b c d e : A)
include s
definition neg_le_neg {a b : A} (H : a ≤ b) : -b ≤ -a :=
have H1 : 0 ≤ -a + b, from !add.left_inv ▸ !(add_le_add_left H),
!add_neg_cancel_right ▸ !zero_add ▸ add_le_add_right H1 (-b)
definition le_of_neg_le_neg {a b : A} (H : -b ≤ -a) : a ≤ b :=
neg_neg a ▸ neg_neg b ▸ neg_le_neg H
definition neg_le_neg_iff_le : -a ≤ -b ↔ b ≤ a :=
iff.intro le_of_neg_le_neg neg_le_neg
definition nonneg_of_neg_nonpos {a : A} (H : -a ≤ 0) : 0 ≤ a :=
le_of_neg_le_neg (neg_zero⁻¹ ▸ H)
definition neg_nonpos_of_nonneg {a : A} (H : 0 ≤ a) : -a ≤ 0 :=
neg_zero ▸ neg_le_neg H
definition neg_nonpos_iff_nonneg : -a ≤ 0 ↔ 0 ≤ a :=
iff.intro nonneg_of_neg_nonpos neg_nonpos_of_nonneg
definition nonpos_of_neg_nonneg {a : A} (H : 0 ≤ -a) : a ≤ 0 :=
le_of_neg_le_neg (neg_zero⁻¹ ▸ H)
definition neg_nonneg_of_nonpos {a : A} (H : a ≤ 0) : 0 ≤ -a :=
neg_zero ▸ neg_le_neg H
definition neg_nonneg_iff_nonpos : 0 ≤ -a ↔ a ≤ 0 :=
iff.intro nonpos_of_neg_nonneg neg_nonneg_of_nonpos
definition neg_lt_neg {a b : A} (H : a < b) : -b < -a :=
have H1 : 0 < -a + b, from !add.left_inv ▸ !(add_lt_add_left H),
!add_neg_cancel_right ▸ !zero_add ▸ add_lt_add_right H1 (-b)
definition lt_of_neg_lt_neg {a b : A} (H : -b < -a) : a < b :=
neg_neg a ▸ neg_neg b ▸ neg_lt_neg H
definition neg_lt_neg_iff_lt : -a < -b ↔ b < a :=
iff.intro lt_of_neg_lt_neg neg_lt_neg
definition pos_of_neg_neg {a : A} (H : -a < 0) : 0 < a :=
lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H)
definition neg_neg_of_pos {a : A} (H : 0 < a) : -a < 0 :=
neg_zero ▸ neg_lt_neg H
definition neg_neg_iff_pos : -a < 0 ↔ 0 < a :=
iff.intro pos_of_neg_neg neg_neg_of_pos
definition neg_of_neg_pos {a : A} (H : 0 < -a) : a < 0 :=
lt_of_neg_lt_neg (neg_zero⁻¹ ▸ H)
definition neg_pos_of_neg {a : A} (H : a < 0) : 0 < -a :=
neg_zero ▸ neg_lt_neg H
definition neg_pos_iff_neg : 0 < -a ↔ a < 0 :=
iff.intro neg_of_neg_pos neg_pos_of_neg
definition le_neg_iff_le_neg : a ≤ -b ↔ b ≤ -a := !neg_neg ▸ !neg_le_neg_iff_le
definition neg_le_iff_neg_le : -a ≤ b ↔ -b ≤ a := !neg_neg ▸ !neg_le_neg_iff_le
definition lt_neg_iff_lt_neg : a < -b ↔ b < -a := !neg_neg ▸ !neg_lt_neg_iff_lt
definition neg_lt_iff_neg_lt : -a < b ↔ -b < a := !neg_neg ▸ !neg_lt_neg_iff_lt
definition sub_nonneg_iff_le : 0 ≤ a - b ↔ b ≤ a := !sub_self ▸ !add_le_add_right_iff
definition sub_nonpos_iff_le : a - b ≤ 0 ↔ a ≤ b := !sub_self ▸ !add_le_add_right_iff
definition sub_pos_iff_lt : 0 < a - b ↔ b < a := !sub_self ▸ !add_lt_add_right_iff
definition sub_neg_iff_lt : a - b < 0 ↔ a < b := !sub_self ▸ !add_lt_add_right_iff
definition add_le_iff_le_neg_add : a + b ≤ c ↔ b ≤ -a + c :=
have H: a + b ≤ c ↔ -a + (a + b) ≤ -a + c, from iff.symm (!add_le_add_left_iff),
!neg_add_cancel_left ▸ H
definition add_le_iff_le_sub_left : a + b ≤ c ↔ b ≤ c - a :=
by rewrite [sub_eq_add_neg, {c+_}add.comm]; apply add_le_iff_le_neg_add
definition add_le_iff_le_sub_right : a + b ≤ c ↔ a ≤ c - b :=
have H: a + b ≤ c ↔ a + b - b ≤ c - b, from iff.symm (!add_le_add_right_iff),
!add_neg_cancel_right ▸ H
definition le_add_iff_neg_add_le : a ≤ b + c ↔ -b + a ≤ c :=
assert H: a ≤ b + c ↔ -b + a ≤ -b + (b + c), from iff.symm (!add_le_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
definition le_add_iff_sub_left_le : a ≤ b + c ↔ a - b ≤ c :=
by rewrite [sub_eq_add_neg, {a+_}add.comm]; apply le_add_iff_neg_add_le
definition le_add_iff_sub_right_le : a ≤ b + c ↔ a - c ≤ b :=
assert H: a ≤ b + c ↔ a - c ≤ b + c - c, from iff.symm (!add_le_add_right_iff),
by rewrite add_neg_cancel_right at H; exact H
definition add_lt_iff_lt_neg_add_left : a + b < c ↔ b < -a + c :=
assert H: a + b < c ↔ -a + (a + b) < -a + c, from iff.symm (!add_lt_add_left_iff),
begin rewrite neg_add_cancel_left at H, exact H end
definition add_lt_iff_lt_neg_add_right : a + b < c ↔ a < -b + c :=
by rewrite add.comm; apply add_lt_iff_lt_neg_add_left
definition add_lt_iff_lt_sub_left : a + b < c ↔ b < c - a :=
begin
rewrite [sub_eq_add_neg, {c+_}add.comm],
apply add_lt_iff_lt_neg_add_left
end
definition add_lt_add_iff_lt_sub_right : a + b < c ↔ a < c - b :=
assert H: a + b < c ↔ a + b - b < c - b, from iff.symm (!add_lt_add_right_iff),
by rewrite add_neg_cancel_right at H; exact H
definition lt_add_iff_neg_add_lt_left : a < b + c ↔ -b + a < c :=
assert H: a < b + c ↔ -b + a < -b + (b + c), from iff.symm (!add_lt_add_left_iff),
by rewrite neg_add_cancel_left at H; exact H
definition lt_add_iff_neg_add_lt_right : a < b + c ↔ -c + a < b :=
by rewrite add.comm; apply lt_add_iff_neg_add_lt_left
definition lt_add_iff_sub_lt_left : a < b + c ↔ a - b < c :=
by rewrite [sub_eq_add_neg, {a + _}add.comm]; apply lt_add_iff_neg_add_lt_left
definition lt_add_iff_sub_lt_right : a < b + c ↔ a - c < b :=
by rewrite add.comm; apply lt_add_iff_sub_lt_left
-- TODO: the Isabelle library has varations on a + b ≤ b ↔ a ≤ 0
definition le_iff_le_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a ≤ b ↔ c ≤ d :=
calc
a ≤ b ↔ a - b ≤ 0 : iff.symm (sub_nonpos_iff_le a b)
... = (c - d ≤ 0) : by rewrite H
... ↔ c ≤ d : sub_nonpos_iff_le c d
definition lt_iff_lt_of_sub_eq_sub {a b c d : A} (H : a - b = c - d) : a < b ↔ c < d :=
calc
a < b ↔ a - b < 0 : iff.symm (sub_neg_iff_lt a b)
... = (c - d < 0) : by rewrite H
... ↔ c < d : sub_neg_iff_lt c d
definition sub_le_sub_left {a b : A} (H : a ≤ b) (c : A) : c - b ≤ c - a :=
add_le_add_left (neg_le_neg H) c
definition sub_le_sub_right {a b : A} (H : a ≤ b) (c : A) : a - c ≤ b - c := add_le_add_right H (-c)
definition sub_le_sub {a b c d : A} (Hab : a ≤ b) (Hcd : c ≤ d) : a - d ≤ b - c :=
add_le_add Hab (neg_le_neg Hcd)
definition sub_lt_sub_left {a b : A} (H : a < b) (c : A) : c - b < c - a :=
add_lt_add_left (neg_lt_neg H) c
definition sub_lt_sub_right {a b : A} (H : a < b) (c : A) : a - c < b - c := add_lt_add_right H (-c)
definition sub_lt_sub {a b c d : A} (Hab : a < b) (Hcd : c < d) : a - d < b - c :=
add_lt_add Hab (neg_lt_neg Hcd)
definition sub_lt_sub_of_le_of_lt {a b c d : A} (Hab : a ≤ b) (Hcd : c < d) : a - d < b - c :=
add_lt_add_of_le_of_lt Hab (neg_lt_neg Hcd)
definition sub_lt_sub_of_lt_of_le {a b c d : A} (Hab : a < b) (Hcd : c ≤ d) : a - d < b - c :=
add_lt_add_of_lt_of_le Hab (neg_le_neg Hcd)
definition sub_le_self (a : A) {b : A} (H : b ≥ 0) : a - b ≤ a :=
calc
a - b = a + -b : rfl
... ≤ a + 0 : add_le_add_left (neg_nonpos_of_nonneg H)
... = a : by rewrite add_zero
definition sub_lt_self (a : A) {b : A} (H : b > 0) : a - b < a :=
calc
a - b = a + -b : rfl
... < a + 0 : add_lt_add_left (neg_neg_of_pos H)
... = a : by rewrite add_zero
end
structure decidable_linear_ordered_comm_group [class] (A : Type)
extends ordered_comm_group A, decidable_linear_order A
section
variables [s : decidable_linear_ordered_comm_group A]
variables {a b c d e : A}
include s
definition eq_zero_of_neg_eq (H : -a = a) : a = 0 :=
lt.by_cases
(assume H1 : a < 0,
have H2: a > 0, from H ▸ neg_pos_of_neg H1,
absurd H1 (lt.asymm H2))
(assume H1 : a = 0, H1)
(assume H1 : a > 0,
have H2: a < 0, from H ▸ neg_neg_of_pos H1,
absurd H1 (lt.asymm H2))
definition abs (a : A) : A := if 0 ≤ a then a else -a
definition abs_of_nonneg (H : a ≥ 0) : abs a = a := if_pos H
definition abs_of_pos (H : a > 0) : abs a = a := if_pos (le_of_lt H)
definition abs_of_neg (H : a < 0) : abs a = -a := if_neg (not_le_of_lt H)
definition abs_zero : abs 0 = 0 := abs_of_nonneg (le.refl _)
definition abs_of_nonpos (H : a ≤ 0) : abs a = -a :=
decidable.by_cases
(assume H1 : a = 0, by rewrite [H1, abs_zero, neg_zero])
(assume H1 : a ≠ 0,
have H2 : a < 0, from lt_of_le_of_ne H H1,
abs_of_neg H2)
definition abs_neg (a : A) : abs (-a) = abs a :=
sum.rec_on (le.total 0 a)
(assume H1 : 0 ≤ a, by rewrite [abs_of_nonpos (neg_nonpos_of_nonneg H1), neg_neg, abs_of_nonneg H1])
(assume H1 : a ≤ 0, by rewrite [abs_of_nonneg (neg_nonneg_of_nonpos H1), abs_of_nonpos H1])
definition abs_nonneg (a : A) : abs a ≥ 0 :=
sum.rec_on (le.total 0 a)
(assume H : 0 ≤ a, by rewrite (abs_of_nonneg H); exact H)
(assume H : a ≤ 0,
calc
0 ≤ -a : neg_nonneg_of_nonpos H
... = abs a : abs_of_nonpos H)
definition abs_abs (a : A) : abs (abs a) = abs a := abs_of_nonneg !abs_nonneg
definition le_abs_self (a : A) : a ≤ abs a :=
sum.rec_on (le.total 0 a)
(assume H : 0 ≤ a, abs_of_nonneg H ▸ !le.refl)
(assume H : a ≤ 0, le.trans H !abs_nonneg)
definition neg_le_abs_self (a : A) : -a ≤ abs a :=
!abs_neg ▸ !le_abs_self
definition eq_zero_of_abs_eq_zero (H : abs a = 0) : a = 0 :=
have H1 : a ≤ 0, from H ▸ le_abs_self a,
have H2 : -a ≤ 0, from H ▸ abs_neg a ▸ le_abs_self (-a),
le.antisymm H1 (nonneg_of_neg_nonpos H2)
definition abs_eq_zero_iff_eq_zero (a : A) : abs a = 0 ↔ a = 0 :=
iff.intro eq_zero_of_abs_eq_zero (assume H, ap abs H ⬝ !abs_zero)
definition abs_pos_of_pos (H : a > 0) : abs a > 0 :=
by rewrite (abs_of_pos H); exact H
definition abs_pos_of_neg (H : a < 0) : abs a > 0 :=
!abs_neg ▸ abs_pos_of_pos (neg_pos_of_neg H)
definition abs_pos_of_ne_zero (H : a ≠ 0) : abs a > 0 :=
sum.rec_on (lt_or_gt_of_ne H) abs_pos_of_neg abs_pos_of_pos
definition abs_sub (a b : A) : abs (a - b) = abs (b - a) :=
by rewrite [-neg_sub, abs_neg]
definition abs.by_cases {P : A → Type} {a : A} (H1 : P a) (H2 : P (-a)) : P (abs a) :=
sum.rec_on (le.total 0 a)
(assume H : 0 ≤ a, (abs_of_nonneg H)⁻¹ ▸ H1)
(assume H : a ≤ 0, (abs_of_nonpos H)⁻¹ ▸ H2)
definition abs_le_of_le_of_neg_le (H1 : a ≤ b) (H2 : -a ≤ b) : abs a ≤ b :=
abs.by_cases H1 H2
definition abs_lt_of_lt_of_neg_lt (H1 : a < b) (H2 : -a < b) : abs a < b :=
abs.by_cases H1 H2
-- the triangle inequality
section
private lemma aux1 {a b : A} (H1 : a + b ≥ 0) (H2 : a ≥ 0) : abs (a + b) ≤ abs a + abs b :=
decidable.by_cases
(assume H3 : b ≥ 0,
calc
abs (a + b) ≤ abs (a + b) : le.refl
... = a + b : by rewrite (abs_of_nonneg H1)
... = abs a + b : by rewrite (abs_of_nonneg H2)
... = abs a + abs b : by rewrite (abs_of_nonneg H3))
(assume H3 : ¬ b ≥ 0,
assert H4 : b ≤ 0, from le_of_lt (lt_of_not_le H3),
calc
abs (a + b) = a + b : by rewrite (abs_of_nonneg H1)
... = abs a + b : by rewrite (abs_of_nonneg H2)
... ≤ abs a + 0 : add_le_add_left H4
... ≤ abs a + -b : add_le_add_left (neg_nonneg_of_nonpos H4)
... = abs a + abs b : by rewrite (abs_of_nonpos H4))
private lemma aux2 {a b : A} (H1 : a + b ≥ 0) : abs (a + b) ≤ abs a + abs b :=
sum.rec_on (le.total b 0)
(assume H2 : b ≤ 0,
have H3 : ¬ a < 0, from
assume H4 : a < 0,
have H5 : a + b < 0, from !add_zero ▸ add_lt_add_of_lt_of_le H4 H2,
not_lt_of_le H1 H5,
aux1 H1 (le_of_not_lt H3))
(assume H2 : 0 ≤ b,
begin
have H3 : abs (b + a) ≤ abs b + abs a,
begin
rewrite add.comm at H1,
exact aux1 H1 H2
end,
rewrite [add.comm, {abs a + _}add.comm],
exact H3
end)
definition abs_add_le_abs_add_abs (a b : A) : abs (a + b) ≤ abs a + abs b :=
sum.rec_on (le.total 0 (a + b))
(assume H2 : 0 ≤ a + b, aux2 H2)
(assume H2 : a + b ≤ 0,
assert H3 : -a + -b = -(a + b), by rewrite neg_add,
assert H4 : -(a + b) ≥ 0, from iff.mp' (neg_nonneg_iff_nonpos (a+b)) H2,
have H5 : -a + -b ≥ 0, begin rewrite -H3 at H4, exact H4 end,
calc
abs (a + b) = abs (-a + -b) : by rewrite [-abs_neg, neg_add]
... ≤ abs (-a) + abs (-b) : aux2 H5
... = abs a + abs b : by rewrite *abs_neg)
end
definition abs_sub_abs_le_abs_sub (a b : A) : abs a - abs b ≤ abs (a - b) :=
have H1 : abs a - abs b + abs b ≤ abs (a - b) + abs b, from
calc
abs a - abs b + abs b = abs a : by rewrite sub_add_cancel
... = abs (a - b + b) : by rewrite sub_add_cancel
... ≤ abs (a - b) + abs b : abs_add_le_abs_add_abs,
algebra.le_of_add_le_add_right H1
end
end algebra

View file

@ -0,0 +1,591 @@
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.ordered_ring
Authors: Jeremy Avigad
Here an "ordered_ring" is partially ordered ring, which is ordered with respect to both a weak
order and an associated strict order. Our numeric structures (int, rat, and real) will be instances
of "linear_ordered_comm_ring". This development is modeled after Isabelle's library.
Ported from the standard library
-/
import algebra.ordered_group algebra.ring
open core
namespace algebra
variable {A : Type}
definition absurd_a_lt_a {B : Type} {a : A} [s : strict_order A] (H : a < a) : B :=
absurd H (lt.irrefl a)
structure ordered_semiring [class] (A : Type)
extends has_mul A, has_zero A, has_lt A, -- TODO: remove hack for improving performance
semiring A, ordered_cancel_comm_monoid A, zero_ne_one_class A :=
(mul_le_mul_of_nonneg_left: Πa b c, le a b → le zero c → le (mul c a) (mul c b))
(mul_le_mul_of_nonneg_right: Πa b c, le a b → le zero c → le (mul a c) (mul b c))
(mul_lt_mul_of_pos_left: Πa b c, lt a b → lt zero c → lt (mul c a) (mul c b))
(mul_lt_mul_of_pos_right: Πa b c, lt a b → lt zero c → lt (mul a c) (mul b c))
section
variable [s : ordered_semiring A]
variables (a b c d e : A)
include s
definition mul_le_mul_of_nonneg_left {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
c * a ≤ c * b := !ordered_semiring.mul_le_mul_of_nonneg_left Hab Hc
definition mul_le_mul_of_nonneg_right {a b c : A} (Hab : a ≤ b) (Hc : 0 ≤ c) :
a * c ≤ b * c := !ordered_semiring.mul_le_mul_of_nonneg_right Hab Hc
-- TODO: there are four variations, depending on which variables we assume to be nonneg
definition mul_le_mul {a b c d : A} (Hac : a ≤ c) (Hbd : b ≤ d) (nn_b : 0 ≤ b) (nn_c : 0 ≤ c) :
a * b ≤ c * d :=
calc
a * b ≤ c * b : mul_le_mul_of_nonneg_right Hac nn_b
... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
definition mul_nonneg {a b : A} (Ha : a ≥ 0) (Hb : b ≥ 0) : a * b ≥ 0 :=
begin
have H : 0 * b ≤ a * b, from mul_le_mul_of_nonneg_right Ha Hb,
rewrite zero_mul at H,
exact H
end
definition mul_nonpos_of_nonneg_of_nonpos {a b : A} (Ha : a ≥ 0) (Hb : b ≤ 0) : a * b ≤ 0 :=
begin
have H : a * b ≤ a * 0, from mul_le_mul_of_nonneg_left Hb Ha,
rewrite mul_zero at H,
exact H
end
definition mul_nonpos_of_nonpos_of_nonneg {a b : A} (Ha : a ≤ 0) (Hb : b ≥ 0) : a * b ≤ 0 :=
begin
have H : a * b ≤ 0 * b, from mul_le_mul_of_nonneg_right Ha Hb,
rewrite zero_mul at H,
exact H
end
definition mul_lt_mul_of_pos_left {a b c : A} (Hab : a < b) (Hc : 0 < c) :
c * a < c * b := !ordered_semiring.mul_lt_mul_of_pos_left Hab Hc
definition mul_lt_mul_of_pos_right {a b c : A} (Hab : a < b) (Hc : 0 < c) :
a * c < b * c := !ordered_semiring.mul_lt_mul_of_pos_right Hab Hc
-- TODO: once again, there are variations
definition mul_lt_mul {a b c d : A} (Hac : a < c) (Hbd : b ≤ d) (pos_b : 0 < b) (nn_c : 0 ≤ c) :
a * b < c * d :=
calc
a * b < c * b : mul_lt_mul_of_pos_right Hac pos_b
... ≤ c * d : mul_le_mul_of_nonneg_left Hbd nn_c
definition mul_pos {a b : A} (Ha : a > 0) (Hb : b > 0) : a * b > 0 :=
begin
have H : 0 * b < a * b, from mul_lt_mul_of_pos_right Ha Hb,
rewrite zero_mul at H,
exact H
end
definition mul_neg_of_pos_of_neg {a b : A} (Ha : a > 0) (Hb : b < 0) : a * b < 0 :=
begin
have H : a * b < a * 0, from mul_lt_mul_of_pos_left Hb Ha,
rewrite mul_zero at H,
exact H
end
definition mul_neg_of_neg_of_pos {a b : A} (Ha : a < 0) (Hb : b > 0) : a * b < 0 :=
begin
have H : a * b < 0 * b, from mul_lt_mul_of_pos_right Ha Hb,
rewrite zero_mul at H,
exact H
end
end
structure linear_ordered_semiring [class] (A : Type)
extends ordered_semiring A, linear_strong_order_pair A
section
variable [s : linear_ordered_semiring A]
variables {a b c : A}
include s
definition lt_of_mul_lt_mul_left (H : c * a < c * b) (Hc : c ≥ 0) : a < b :=
lt_of_not_le
(assume H1 : b ≤ a,
have H2 : c * b ≤ c * a, from mul_le_mul_of_nonneg_left H1 Hc,
not_lt_of_le H2 H)
definition lt_of_mul_lt_mul_right (H : a * c < b * c) (Hc : c ≥ 0) : a < b :=
lt_of_not_le
(assume H1 : b ≤ a,
have H2 : b * c ≤ a * c, from mul_le_mul_of_nonneg_right H1 Hc,
not_lt_of_le H2 H)
definition le_of_mul_le_mul_left (H : c * a ≤ c * b) (Hc : c > 0) : a ≤ b :=
le_of_not_lt
(assume H1 : b < a,
have H2 : c * b < c * a, from mul_lt_mul_of_pos_left H1 Hc,
not_le_of_lt H2 H)
definition le_of_mul_le_mul_right (H : a * c ≤ b * c) (Hc : c > 0) : a ≤ b :=
le_of_not_lt
(assume H1 : b < a,
have H2 : b * c < a * c, from mul_lt_mul_of_pos_right H1 Hc,
not_le_of_lt H2 H)
definition pos_of_mul_pos_left (H : 0 < a * b) (H1 : 0 ≤ a) : 0 < b :=
lt_of_not_le
(assume H2 : b ≤ 0,
have H3 : a * b ≤ 0, from mul_nonpos_of_nonneg_of_nonpos H1 H2,
not_lt_of_le H3 H)
definition pos_of_mul_pos_right (H : 0 < a * b) (H1 : 0 ≤ b) : 0 < a :=
lt_of_not_le
(assume H2 : a ≤ 0,
have H3 : a * b ≤ 0, from mul_nonpos_of_nonpos_of_nonneg H2 H1,
not_lt_of_le H3 H)
end
structure ordered_ring [class] (A : Type) extends ring A, ordered_comm_group A, zero_ne_one_class A :=
(mul_nonneg : Πa b, le zero a → le zero b → le zero (mul a b))
(mul_pos : Πa b, lt zero a → lt zero b → lt zero (mul a b))
definition ordered_ring.mul_le_mul_of_nonneg_left [s : ordered_ring A] {a b c : A}
(Hab : a ≤ b) (Hc : 0 ≤ c) : c * a ≤ c * b :=
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
assert H2 : 0 ≤ c * (b - a), from ordered_ring.mul_nonneg _ _ Hc H1,
begin
rewrite mul_sub_left_distrib at H2,
exact (iff.mp !sub_nonneg_iff_le H2)
end
definition ordered_ring.mul_le_mul_of_nonneg_right [s : ordered_ring A] {a b c : A}
(Hab : a ≤ b) (Hc : 0 ≤ c) : a * c ≤ b * c :=
have H1 : 0 ≤ b - a, from iff.elim_right !sub_nonneg_iff_le Hab,
assert H2 : 0 ≤ (b - a) * c, from ordered_ring.mul_nonneg _ _ H1 Hc,
begin
rewrite mul_sub_right_distrib at H2,
exact (iff.mp !sub_nonneg_iff_le H2)
end
definition ordered_ring.mul_lt_mul_of_pos_left [s : ordered_ring A] {a b c : A}
(Hab : a < b) (Hc : 0 < c) : c * a < c * b :=
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
assert H2 : 0 < c * (b - a), from ordered_ring.mul_pos _ _ Hc H1,
begin
rewrite mul_sub_left_distrib at H2,
exact (iff.mp !sub_pos_iff_lt H2)
end
definition ordered_ring.mul_lt_mul_of_pos_right [s : ordered_ring A] {a b c : A}
(Hab : a < b) (Hc : 0 < c) : a * c < b * c :=
have H1 : 0 < b - a, from iff.elim_right !sub_pos_iff_lt Hab,
assert H2 : 0 < (b - a) * c, from ordered_ring.mul_pos _ _ H1 Hc,
begin
rewrite mul_sub_right_distrib at H2,
exact (iff.mp !sub_pos_iff_lt H2)
end
definition ordered_ring.to_ordered_semiring [instance] [coercion] [reducible] [s : ordered_ring A] :
ordered_semiring A :=
⦃ ordered_semiring, s,
mul_zero := mul_zero,
zero_mul := zero_mul,
add_left_cancel := @add.left_cancel A s,
add_right_cancel := @add.right_cancel A s,
le_of_add_le_add_left := @le_of_add_le_add_left A s,
mul_le_mul_of_nonneg_left := @ordered_ring.mul_le_mul_of_nonneg_left A s,
mul_le_mul_of_nonneg_right := @ordered_ring.mul_le_mul_of_nonneg_right A s,
mul_lt_mul_of_pos_left := @ordered_ring.mul_lt_mul_of_pos_left A s,
mul_lt_mul_of_pos_right := @ordered_ring.mul_lt_mul_of_pos_right A s ⦄
section
variable [s : ordered_ring A]
variables {a b c : A}
include s
definition mul_le_mul_of_nonpos_left (H : b ≤ a) (Hc : c ≤ 0) : c * a ≤ c * b :=
have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
assert H1 : -c * b ≤ -c * a, from mul_le_mul_of_nonneg_left H Hc',
have H2 : -(c * b) ≤ -(c * a),
begin
rewrite [-*neg_mul_eq_neg_mul at H1],
exact H1
end,
iff.mp !neg_le_neg_iff_le H2
definition mul_le_mul_of_nonpos_right (H : b ≤ a) (Hc : c ≤ 0) : a * c ≤ b * c :=
have Hc' : -c ≥ 0, from iff.mp' !neg_nonneg_iff_nonpos Hc,
assert H1 : b * -c ≤ a * -c, from mul_le_mul_of_nonneg_right H Hc',
have H2 : -(b * c) ≤ -(a * c),
begin
rewrite [-*neg_mul_eq_mul_neg at H1],
exact H1
end,
iff.mp !neg_le_neg_iff_le H2
definition mul_nonneg_of_nonpos_of_nonpos (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a * b :=
begin
have H : 0 * b ≤ a * b, from mul_le_mul_of_nonpos_right Ha Hb,
rewrite zero_mul at H,
exact H
end
definition mul_lt_mul_of_neg_left (H : b < a) (Hc : c < 0) : c * a < c * b :=
have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
assert H1 : -c * b < -c * a, from mul_lt_mul_of_pos_left H Hc',
have H2 : -(c * b) < -(c * a),
begin
rewrite [-*neg_mul_eq_neg_mul at H1],
exact H1
end,
iff.mp !neg_lt_neg_iff_lt H2
definition mul_lt_mul_of_neg_right (H : b < a) (Hc : c < 0) : a * c < b * c :=
have Hc' : -c > 0, from iff.mp' !neg_pos_iff_neg Hc,
assert H1 : b * -c < a * -c, from mul_lt_mul_of_pos_right H Hc',
have H2 : -(b * c) < -(a * c),
begin
rewrite [-*neg_mul_eq_mul_neg at H1],
exact H1
end,
iff.mp !neg_lt_neg_iff_lt H2
definition mul_pos_of_neg_of_neg (Ha : a < 0) (Hb : b < 0) : 0 < a * b :=
begin
have H : 0 * b < a * b, from mul_lt_mul_of_neg_right Ha Hb,
rewrite zero_mul at H,
exact H
end
end
-- TODO: we can eliminate mul_pos_of_pos, but now it is not worth the effort to redeclare the
-- class instance
structure linear_ordered_ring [class] (A : Type) extends ordered_ring A, linear_strong_order_pair A
-- print fields linear_ordered_semiring
definition linear_ordered_ring.to_linear_ordered_semiring [instance] [coercion] [reducible]
[s : linear_ordered_ring A] :
linear_ordered_semiring A :=
⦃ linear_ordered_semiring, s,
mul_zero := mul_zero,
zero_mul := zero_mul,
add_left_cancel := @add.left_cancel A s,
add_right_cancel := @add.right_cancel A s,
le_of_add_le_add_left := @le_of_add_le_add_left A s,
mul_le_mul_of_nonneg_left := @mul_le_mul_of_nonneg_left A s,
mul_le_mul_of_nonneg_right := @mul_le_mul_of_nonneg_right A s,
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left A s,
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right A s,
le_total := linear_ordered_ring.le_total ⦄
structure linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_ring A, comm_monoid A
definition linear_ordered_comm_ring.eq_zero_or_eq_zero_of_mul_eq_zero [s : linear_ordered_comm_ring A]
{a b : A} (H : a * b = 0) : a = 0 ⊎ b = 0 :=
lt.by_cases
(assume Ha : 0 < a,
lt.by_cases
(assume Hb : 0 < b,
begin
have H1 : 0 < a * b, from mul_pos Ha Hb,
rewrite H at H1,
apply absurd_a_lt_a H1
end)
(assume Hb : 0 = b, sum.inr (Hb⁻¹))
(assume Hb : 0 > b,
begin
have H1 : 0 > a * b, from mul_neg_of_pos_of_neg Ha Hb,
rewrite H at H1,
apply absurd_a_lt_a H1
end))
(assume Ha : 0 = a, sum.inl (Ha⁻¹))
(assume Ha : 0 > a,
lt.by_cases
(assume Hb : 0 < b,
begin
have H1 : 0 > a * b, from mul_neg_of_neg_of_pos Ha Hb,
rewrite H at H1,
apply absurd_a_lt_a H1
end)
(assume Hb : 0 = b, sum.inr (Hb⁻¹))
(assume Hb : 0 > b,
begin
have H1 : 0 < a * b, from mul_pos_of_neg_of_neg Ha Hb,
rewrite H at H1,
apply absurd_a_lt_a H1
end))
-- Linearity implies no zero divisors. Doesn't need commutativity.
definition linear_ordered_comm_ring.to_integral_domain [instance] [coercion] [reducible]
[s: linear_ordered_comm_ring A] : integral_domain A :=
⦃ integral_domain, s,
eq_zero_or_eq_zero_of_mul_eq_zero :=
@linear_ordered_comm_ring.eq_zero_or_eq_zero_of_mul_eq_zero A s ⦄
section
variable [s : linear_ordered_ring A]
variables (a b c : A)
include s
definition mul_self_nonneg : a * a ≥ 0 :=
sum.rec_on (le.total 0 a)
(assume H : a ≥ 0, mul_nonneg H H)
(assume H : a ≤ 0, mul_nonneg_of_nonpos_of_nonpos H H)
definition zero_le_one : 0 ≤ 1 := one_mul 1 ▸ mul_self_nonneg (1 : A)
definition zero_lt_one : 0 < 1 := lt_of_le_of_ne zero_le_one zero_ne_one
definition pos_and_pos_or_neg_and_neg_of_mul_pos {a b : A} (Hab : a * b > 0) :
(a > 0 × b > 0) ⊎ (a < 0 × b < 0) :=
lt.by_cases
(assume Ha : 0 < a,
lt.by_cases
(assume Hb : 0 < b, sum.inl (pair Ha Hb))
(assume Hb : 0 = b,
begin
rewrite [-Hb at Hab, mul_zero at Hab],
apply absurd_a_lt_a Hab
end)
(assume Hb : b < 0,
absurd Hab (lt.asymm (mul_neg_of_pos_of_neg Ha Hb))))
(assume Ha : 0 = a,
begin
rewrite [-Ha at Hab, zero_mul at Hab],
apply absurd_a_lt_a Hab
end)
(assume Ha : a < 0,
lt.by_cases
(assume Hb : 0 < b,
absurd Hab (lt.asymm (mul_neg_of_neg_of_pos Ha Hb)))
(assume Hb : 0 = b,
begin
rewrite [-Hb at Hab, mul_zero at Hab],
apply absurd_a_lt_a Hab
end)
(assume Hb : b < 0, sum.inr (pair Ha Hb)))
definition gt_of_mul_lt_mul_neg_left {a b c : A} (H : c * a < c * b) (Hc : c ≤ 0) : a > b :=
have nhc : -c ≥ 0, from neg_nonneg_of_nonpos Hc,
have H2 : -(c * b) < -(c * a), from iff.mp' (neg_lt_neg_iff_lt _ _) H,
have H3 : (-c) * b < (-c) * a, from calc
(-c) * b = - (c * b) : neg_mul_eq_neg_mul
... < -(c * a) : H2
... = (-c) * a : neg_mul_eq_neg_mul,
lt_of_mul_lt_mul_left H3 nhc
definition zero_gt_neg_one : -1 < (0 : A) :=
neg_zero ▸ (neg_lt_neg zero_lt_one)
end
/- TODO: Isabelle's library has all kinds of cancelation rules for the simplifier.
Search on mult_le_cancel_right1 in Rings.thy. -/
structure decidable_linear_ordered_comm_ring [class] (A : Type) extends linear_ordered_comm_ring A,
decidable_linear_ordered_comm_group A
section
variable [s : decidable_linear_ordered_comm_ring A]
variables {a b c : A}
include s
definition sign (a : A) : A := lt.cases a 0 (-1) 0 1
definition sign_of_neg (H : a < 0) : sign a = -1 := lt.cases_of_lt H
definition sign_zero : sign 0 = 0 := lt.cases_of_eq rfl
definition sign_of_pos (H : a > 0) : sign a = 1 := lt.cases_of_gt H
definition sign_one : sign 1 = 1 := sign_of_pos zero_lt_one
definition sign_neg_one : sign (-1) = -1 := sign_of_neg (neg_neg_of_pos zero_lt_one)
definition sign_sign (a : A) : sign (sign a) = sign a :=
lt.by_cases
(assume H : a > 0,
calc
sign (sign a) = sign 1 : by rewrite (sign_of_pos H)
... = 1 : by rewrite sign_one
... = sign a : by rewrite (sign_of_pos H))
(assume H : 0 = a,
calc
sign (sign a) = sign (sign 0) : by rewrite H
... = sign 0 : by rewrite sign_zero at {1}
... = sign a : by rewrite -H)
(assume H : a < 0,
calc
sign (sign a) = sign (-1) : by rewrite (sign_of_neg H)
... = -1 : by rewrite sign_neg_one
... = sign a : by rewrite (sign_of_neg H))
definition pos_of_sign_eq_one (H : sign a = 1) : a > 0 :=
lt.by_cases
(assume H1 : 0 < a, H1)
(assume H1 : 0 = a,
begin
rewrite [-H1 at H, sign_zero at H],
apply absurd H zero_ne_one
end)
(assume H1 : 0 > a,
have H2 : -1 = 1, from (sign_of_neg H1)⁻¹ ⬝ H,
absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one)
definition eq_zero_of_sign_eq_zero (H : sign a = 0) : a = 0 :=
lt.by_cases
(assume H1 : 0 < a,
absurd (H⁻¹ ⬝ sign_of_pos H1) zero_ne_one)
(assume H1 : 0 = a, H1⁻¹)
(assume H1 : 0 > a,
have H2 : 0 = -1, from H⁻¹ ⬝ sign_of_neg H1,
have H3 : 1 = 0, from eq_neg_of_eq_neg H2 ⬝ neg_zero,
absurd (H3⁻¹) zero_ne_one)
definition neg_of_sign_eq_neg_one (H : sign a = -1) : a < 0 :=
lt.by_cases
(assume H1 : 0 < a,
have H2 : -1 = 1, from H⁻¹ ⬝ (sign_of_pos H1),
absurd ((eq_zero_of_neg_eq H2)⁻¹) zero_ne_one)
(assume H1 : 0 = a,
have H2 : 0 = -1,
begin
rewrite [-H1 at H, sign_zero at H],
exact H
end,
have H3 : 1 = 0, from eq_neg_of_eq_neg H2 ⬝ neg_zero,
absurd (H3⁻¹) zero_ne_one)
(assume H1 : 0 > a, H1)
definition sign_neg (a : A) : sign (-a) = -(sign a) :=
lt.by_cases
(assume H1 : 0 < a,
calc
sign (-a) = -1 : sign_of_neg (neg_neg_of_pos H1)
... = -(sign a) : by rewrite (sign_of_pos H1))
(assume H1 : 0 = a,
calc
sign (-a) = sign (-0) : by rewrite H1
... = sign 0 : by rewrite neg_zero
... = 0 : by rewrite sign_zero
... = -0 : by rewrite neg_zero
... = -(sign 0) : by rewrite sign_zero
... = -(sign a) : by rewrite -H1)
(assume H1 : 0 > a,
calc
sign (-a) = 1 : sign_of_pos (neg_pos_of_neg H1)
... = -(-1) : by rewrite neg_neg
... = -(sign a) : sign_of_neg H1)
definition sign_mul (a b : A) : sign (a * b) = sign a * sign b :=
lt.by_cases
(assume z_lt_a : 0 < a,
lt.by_cases
(assume z_lt_b : 0 < b,
by rewrite [sign_of_pos z_lt_a, sign_of_pos z_lt_b,
sign_of_pos (mul_pos z_lt_a z_lt_b), one_mul])
(assume z_eq_b : 0 = b, by rewrite [-z_eq_b, mul_zero, *sign_zero, mul_zero])
(assume z_gt_b : 0 > b,
by rewrite [sign_of_pos z_lt_a, sign_of_neg z_gt_b,
sign_of_neg (mul_neg_of_pos_of_neg z_lt_a z_gt_b), one_mul]))
(assume z_eq_a : 0 = a, by rewrite [-z_eq_a, zero_mul, *sign_zero, zero_mul])
(assume z_gt_a : 0 > a,
lt.by_cases
(assume z_lt_b : 0 < b,
by rewrite [sign_of_neg z_gt_a, sign_of_pos z_lt_b,
sign_of_neg (mul_neg_of_neg_of_pos z_gt_a z_lt_b), mul_one])
(assume z_eq_b : 0 = b, by rewrite [-z_eq_b, mul_zero, *sign_zero, mul_zero])
(assume z_gt_b : 0 > b,
by rewrite [sign_of_neg z_gt_a, sign_of_neg z_gt_b,
sign_of_pos (mul_pos_of_neg_of_neg z_gt_a z_gt_b),
neg_mul_neg, one_mul]))
definition abs_eq_sign_mul (a : A) : abs a = sign a * a :=
lt.by_cases
(assume H1 : 0 < a,
calc
abs a = a : abs_of_pos H1
... = 1 * a : by rewrite one_mul
... = sign a * a : by rewrite (sign_of_pos H1))
(assume H1 : 0 = a,
calc
abs a = abs 0 : by rewrite H1
... = 0 : by rewrite abs_zero
... = 0 * a : by rewrite zero_mul
... = sign 0 * a : by rewrite sign_zero
... = sign a * a : by rewrite H1)
(assume H1 : a < 0,
calc
abs a = -a : abs_of_neg H1
... = -1 * a : by rewrite neg_eq_neg_one_mul
... = sign a * a : by rewrite (sign_of_neg H1))
definition eq_sign_mul_abs (a : A) : a = sign a * abs a :=
lt.by_cases
(assume H1 : 0 < a,
calc
a = abs a : abs_of_pos H1
... = 1 * abs a : by rewrite one_mul
... = sign a * abs a : by rewrite (sign_of_pos H1))
(assume H1 : 0 = a,
calc
a = 0 : H1⁻¹
... = 0 * abs a : by rewrite zero_mul
... = sign 0 * abs a : by rewrite sign_zero
... = sign a * abs a : by rewrite H1)
(assume H1 : a < 0,
calc
a = -(-a) : by rewrite neg_neg
... = -abs a : by rewrite (abs_of_neg H1)
... = -1 * abs a : by rewrite neg_eq_neg_one_mul
... = sign a * abs a : by rewrite (sign_of_neg H1))
definition abs_dvd_iff_dvd (a b : A) : abs a b ↔ a b :=
abs.by_cases !iff.refl !neg_dvd_iff_dvd
definition dvd_abs_iff (a b : A) : a abs b ↔ a b :=
abs.by_cases !iff.refl !dvd_neg_iff_dvd
definition abs_mul (a b : A) : abs (a * b) = abs a * abs b :=
sum.rec_on (le.total 0 a)
(assume H1 : 0 ≤ a,
sum.rec_on (le.total 0 b)
(assume H2 : 0 ≤ b,
calc
abs (a * b) = a * b : abs_of_nonneg (mul_nonneg H1 H2)
... = abs a * b : by rewrite (abs_of_nonneg H1)
... = abs a * abs b : by rewrite (abs_of_nonneg H2))
(assume H2 : b ≤ 0,
calc
abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonneg_of_nonpos H1 H2)
... = a * -b : by rewrite neg_mul_eq_mul_neg
... = abs a * -b : by rewrite (abs_of_nonneg H1)
... = abs a * abs b : by rewrite (abs_of_nonpos H2)))
(assume H1 : a ≤ 0,
sum.rec_on (le.total 0 b)
(assume H2 : 0 ≤ b,
calc
abs (a * b) = -(a * b) : abs_of_nonpos (mul_nonpos_of_nonpos_of_nonneg H1 H2)
... = -a * b : by rewrite neg_mul_eq_neg_mul
... = abs a * b : by rewrite (abs_of_nonpos H1)
... = abs a * abs b : by rewrite (abs_of_nonneg H2))
(assume H2 : b ≤ 0,
calc
abs (a * b) = a * b : abs_of_nonneg (mul_nonneg_of_nonpos_of_nonpos H1 H2)
... = -a * -b : by rewrite neg_mul_neg
... = abs a * -b : by rewrite (abs_of_nonpos H1)
... = abs a * abs b : by rewrite (abs_of_nonpos H2)))
definition abs_mul_self (a : A) : abs a * abs a = a * a :=
abs.by_cases rfl !neg_mul_neg
end
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
end algebra

363
hott/algebra/ring.hlean Normal file
View file

@ -0,0 +1,363 @@
/-
Copyright (c) 2014 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: algebra.ring
Authors: Jeremy Avigad, Leonardo de Moura
Structures with multiplicative and additive components, including semirings, rings, and fields.
The development is modeled after Isabelle's library.
Ported from the standard library
-/
import algebra.group
open core
namespace algebra
variable {A : Type}
/- auxiliary classes -/
structure distrib [class] (A : Type) extends has_mul A, has_add A :=
(left_distrib : Πa b c, mul a (add b c) = add (mul a b) (mul a c))
(right_distrib : Πa b c, mul (add a b) c = add (mul a c) (mul b c))
definition left_distrib [s : distrib A] (a b c : A) : a * (b + c) = a * b + a * c :=
!distrib.left_distrib
definition right_distrib [s: distrib A] (a b c : A) : (a + b) * c = a * c + b * c :=
!distrib.right_distrib
structure mul_zero_class [class] (A : Type) extends has_mul A, has_zero A :=
(zero_mul : Πa, mul zero a = zero)
(mul_zero : Πa, mul a zero = zero)
definition zero_mul [s : mul_zero_class A] (a : A) : 0 * a = 0 := !mul_zero_class.zero_mul
definition mul_zero [s : mul_zero_class A] (a : A) : a * 0 = 0 := !mul_zero_class.mul_zero
structure zero_ne_one_class [class] (A : Type) extends has_zero A, has_one A :=
(zero_ne_one : zero ≠ one)
definition zero_ne_one [s: zero_ne_one_class A] : 0 ≠ 1 := @zero_ne_one_class.zero_ne_one A s
/- semiring -/
structure semiring [class] (A : Type) extends add_comm_monoid A, monoid A, distrib A,
mul_zero_class A
section semiring
variables [s : semiring A] (a b c : A)
include s
definition ne_zero_of_mul_ne_zero_right {a b : A} (H : a * b ≠ 0) : a ≠ 0 :=
assume H1 : a = 0,
have H2 : a * b = 0, from H1⁻¹ ▸ zero_mul b,
H H2
definition ne_zero_of_mul_ne_zero_left {a b : A} (H : a * b ≠ 0) : b ≠ 0 :=
assume H1 : b = 0,
have H2 : a * b = 0, from H1⁻¹ ▸ mul_zero a,
H H2
end semiring
/- comm semiring -/
structure comm_semiring [class] (A : Type) extends semiring A, comm_semigroup A
-- TODO: we could also define a cancelative comm_semiring, i.e. satisfying
-- c ≠ 0 → c * a = c * b → a = b.
section comm_semiring
variables [s : comm_semiring A] (a b c : A)
include s
definition dvd (a b : A) : Type := Σc, b = a * c
notation a b := dvd a b
definition dvd.intro {a b c : A} (H : a * c = b) : a b :=
sigma.mk _ H⁻¹
definition dvd.intro_left {a b c : A} (H : c * a = b) : a b :=
dvd.intro (!mul.comm ▸ H)
definition exists_eq_mul_right_of_dvd {a b : A} (H : a b) : Σc, b = a * c := H
definition dvd.elim {P : Type} {a b : A} (H₁ : a b) (H₂ : Πc, b = a * c → P) : P :=
sigma.rec_on H₁ H₂
definition exists_eq_mul_left_of_dvd {a b : A} (H : a b) : Σc, b = c * a :=
dvd.elim H (take c, assume H1 : b = a * c, sigma.mk c (H1 ⬝ !mul.comm))
definition dvd.elim_left {P : Type} {a b : A} (H₁ : a b) (H₂ : Πc, b = c * a → P) : P :=
sigma.rec_on (exists_eq_mul_left_of_dvd H₁) (take c, assume H₃ : b = c * a, H₂ c H₃)
definition dvd.refl : a a := dvd.intro !mul_one
definition dvd.trans {a b c : A} (H₁ : a b) (H₂ : b c) : a c :=
dvd.elim H₁
(take d, assume H₃ : b = a * d,
dvd.elim H₂
(take e, assume H₄ : c = b * e,
dvd.intro
(show a * (d * e) = c, by rewrite [-mul.assoc, -H₃, H₄])))
definition eq_zero_of_zero_dvd {a : A} (H : 0 a) : a = 0 :=
dvd.elim H (take c, assume H' : a = 0 * c, H' ⬝ !zero_mul)
definition dvd_zero : a 0 := dvd.intro !mul_zero
definition one_dvd : 1 a := dvd.intro !one_mul
definition dvd_mul_right : a a * b := dvd.intro rfl
definition dvd_mul_left : a b * a := mul.comm a b ▸ dvd_mul_right a b
definition dvd_mul_of_dvd_left {a b : A} (H : a b) (c : A) : a b * c :=
dvd.elim H
(take d,
assume H₁ : b = a * d,
dvd.intro
(show a * (d * c) = b * c, from by rewrite [-mul.assoc, H₁]))
definition dvd_mul_of_dvd_right {a b : A} (H : a b) (c : A) : a c * b :=
!mul.comm ▸ (dvd_mul_of_dvd_left H _)
definition mul_dvd_mul {a b c d : A} (dvd_ab : (a b)) (dvd_cd : c d) : a * c b * d :=
dvd.elim dvd_ab
(take e, assume Haeb : b = a * e,
dvd.elim dvd_cd
(take f, assume Hcfd : d = c * f,
dvd.intro
(show a * c * (e * f) = b * d,
by rewrite [mul.assoc, {c*_}mul.left_comm, -mul.assoc, Haeb, Hcfd])))
definition dvd_of_mul_right_dvd {a b c : A} (H : a * b c) : a c :=
dvd.elim H (take d, assume Habdc : c = a * b * d, dvd.intro (!mul.assoc⁻¹ ⬝ Habdc⁻¹))
definition dvd_of_mul_left_dvd {a b c : A} (H : a * b c) : b c :=
dvd_of_mul_right_dvd (mul.comm a b ▸ H)
definition dvd_add {a b c : A} (Hab : a b) (Hac : a c) : a b + c :=
dvd.elim Hab
(take d, assume Hadb : b = a * d,
dvd.elim Hac
(take e, assume Haec : c = a * e,
dvd.intro (show a * (d + e) = b + c,
by rewrite [left_distrib, -Hadb, -Haec])))
end comm_semiring
/- ring -/
structure ring [class] (A : Type) extends add_comm_group A, monoid A, distrib A
definition ring.mul_zero [s : ring A] (a : A) : a * 0 = 0 :=
have H : a * 0 + 0 = a * 0 + a * 0, from calc
a * 0 + 0 = a * 0 : by rewrite add_zero
... = a * (0 + 0) : by rewrite add_zero
... = a * 0 + a * 0 : by rewrite {a*_}ring.left_distrib,
show a * 0 = 0, from (add.left_cancel H)⁻¹
definition ring.zero_mul [s : ring A] (a : A) : 0 * a = 0 :=
have H : 0 * a + 0 = 0 * a + 0 * a, from calc
0 * a + 0 = 0 * a : by rewrite add_zero
... = (0 + 0) * a : by rewrite add_zero
... = 0 * a + 0 * a : by rewrite {_*a}ring.right_distrib,
show 0 * a = 0, from (add.left_cancel H)⁻¹
definition ring.to_semiring [instance] [coercion] [reducible] [s : ring A] : semiring A :=
⦃ semiring, s,
mul_zero := ring.mul_zero,
zero_mul := ring.zero_mul ⦄
section
variables [s : ring A] (a b c d e : A)
include s
definition neg_mul_eq_neg_mul : -(a * b) = -a * b :=
neg_eq_of_add_eq_zero
begin
rewrite [-right_distrib, add.right_inv, zero_mul]
end
definition neg_mul_eq_mul_neg : -(a * b) = a * -b :=
neg_eq_of_add_eq_zero
begin
rewrite [-left_distrib, add.right_inv, mul_zero]
end
definition neg_mul_neg : -a * -b = a * b :=
calc
-a * -b = -(a * -b) : by rewrite -neg_mul_eq_neg_mul
... = - -(a * b) : by rewrite -neg_mul_eq_mul_neg
... = a * b : by rewrite neg_neg
definition neg_mul_comm : -a * b = a * -b := !neg_mul_eq_neg_mul⁻¹ ⬝ !neg_mul_eq_mul_neg
definition neg_eq_neg_one_mul : -a = -1 * a :=
calc
-a = -(1 * a) : by rewrite one_mul
... = -1 * a : by rewrite neg_mul_eq_neg_mul
definition mul_sub_left_distrib : a * (b - c) = a * b - a * c :=
calc
a * (b - c) = a * b + a * -c : left_distrib
... = a * b + - (a * c) : by rewrite -neg_mul_eq_mul_neg
... = a * b - a * c : rfl
definition mul_sub_right_distrib : (a - b) * c = a * c - b * c :=
calc
(a - b) * c = a * c + -b * c : right_distrib
... = a * c + - (b * c) : by rewrite neg_mul_eq_neg_mul
... = a * c - b * c : rfl
-- TODO: can calc mode be improved to make this easier?
-- TODO: there is also the other direction. It will be easier when we
-- have the simplifier.
definition mul_add_eq_mul_add_iff_sub_mul_add_eq : a * e + c = b * e + d ↔ (a - b) * e + c = d :=
calc
a * e + c = b * e + d ↔ a * e + c = d + b * e : by rewrite {b*e+_}add.comm
... ↔ a * e + c - b * e = d : iff.symm !sub_eq_iff_eq_add
... ↔ a * e - b * e + c = d : by rewrite sub_add_eq_add_sub
... ↔ (a - b) * e + c = d : by rewrite mul_sub_right_distrib
definition mul_neg_one_eq_neg : a * (-1) = -a :=
have H : a + a * -1 = 0, from calc
a + a * -1 = a * 1 + a * -1 : mul_one
... = a * (1 + -1) : left_distrib
... = a * 0 : add.right_inv
... = 0 : mul_zero,
inverse (neg_eq_of_add_eq_zero H)
definition mul_ne_zero_imp_ne_zero {a b} (H : a * b ≠ 0) : a ≠ 0 × b ≠ 0 :=
have Ha : a ≠ 0, from
(assume Ha1 : a = 0,
have H1 : a * b = 0, by rewrite [Ha1, zero_mul],
absurd H1 H),
have Hb : b ≠ 0, from
(assume Hb1 : b = 0,
have H1 : a * b = 0, by rewrite [Hb1, mul_zero],
absurd H1 H),
pair Ha Hb
end
structure comm_ring [class] (A : Type) extends ring A, comm_semigroup A
definition comm_ring.to_comm_semiring [instance] [coercion] [reducible] [s : comm_ring A] : comm_semiring A :=
⦃ comm_semiring, s,
mul_zero := mul_zero,
zero_mul := zero_mul ⦄
section
variables [s : comm_ring A] (a b c d e : A)
include s
definition mul_self_sub_mul_self_eq : a * a - b * b = (a + b) * (a - b) :=
by rewrite [left_distrib, *right_distrib, add.assoc, -{b*a + _}add.assoc,
-*neg_mul_eq_mul_neg, {a*b}mul.comm, add.right_inv, zero_add]
definition mul_self_sub_one_eq : a * a - 1 = (a + 1) * (a - 1) :=
mul_one 1 ▸ mul_self_sub_mul_self_eq a 1
definition dvd_neg_iff_dvd : (a -b) ↔ (a b) :=
iff.intro
(assume H : (a -b),
dvd.elim H
(take c, assume H' : -b = a * c,
dvd.intro
(show a * -c = b,
by rewrite [-neg_mul_eq_mul_neg, -H', neg_neg])))
(assume H : (a b),
dvd.elim H
(take c, assume H' : b = a * c,
dvd.intro
(show a * -c = -b,
by rewrite [-neg_mul_eq_mul_neg, -H'])))
definition neg_dvd_iff_dvd : (-a b) ↔ (a b) :=
iff.intro
(assume H : (-a b),
dvd.elim H
(take c, assume H' : b = -a * c,
dvd.intro
(show a * -c = b, by rewrite [-neg_mul_comm, H'])))
(assume H : (a b),
dvd.elim H
(take c, assume H' : b = a * c,
dvd.intro
(show -a * -c = b, by rewrite [neg_mul_neg, H'])))
definition dvd_sub (H₁ : (a b)) (H₂ : (a c)) : (a b - c) :=
dvd_add H₁ (iff.elim_right !dvd_neg_iff_dvd H₂)
end
/- integral domains -/
structure no_zero_divisors [class] (A : Type) extends has_mul A, has_zero A :=
(eq_zero_or_eq_zero_of_mul_eq_zero : Πa b, mul a b = zero → a = zero ⊎ b = zero)
definition eq_zero_or_eq_zero_of_mul_eq_zero {A : Type} [s : no_zero_divisors A] {a b : A}
(H : a * b = 0) :
a = 0 ⊎ b = 0 := !no_zero_divisors.eq_zero_or_eq_zero_of_mul_eq_zero H
structure integral_domain [class] (A : Type) extends comm_ring A, no_zero_divisors A
section
variables [s : integral_domain A] (a b c d e : A)
include s
definition mul_ne_zero {a b : A} (H1 : a ≠ 0) (H2 : b ≠ 0) : a * b ≠ 0 :=
assume H : a * b = 0,
sum.rec_on (eq_zero_or_eq_zero_of_mul_eq_zero H) (assume H3, H1 H3) (assume H4, H2 H4)
definition mul.cancel_right {a b c : A} (Ha : a ≠ 0) (H : b * a = c * a) : b = c :=
have H1 : b * a - c * a = 0, from iff.mp !eq_iff_sub_eq_zero H,
have H2 : (b - c) * a = 0, using H1, by rewrite [mul_sub_right_distrib, H1],
have H3 : b - c = 0, from sum_resolve_left (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
iff.elim_right !eq_iff_sub_eq_zero H3
definition mul.cancel_left {a b c : A} (Ha : a ≠ 0) (H : a * b = a * c) : b = c :=
have H1 : a * b - a * c = 0, from iff.mp !eq_iff_sub_eq_zero H,
have H2 : a * (b - c) = 0, using H1, by rewrite [mul_sub_left_distrib, H1],
have H3 : b - c = 0, from sum_resolve_right (eq_zero_or_eq_zero_of_mul_eq_zero H2) Ha,
iff.elim_right !eq_iff_sub_eq_zero H3
-- TODO: do we want the iff versions?
definition mul_self_eq_mul_self_iff (a b : A) : a * a = b * b ↔ a = b ⊎ a = -b :=
iff.intro
(λ H : a * a = b * b,
have aux₁ : (a - b) * (a + b) = 0,
by rewrite [mul.comm, -mul_self_sub_mul_self_eq, H, sub_self],
assert aux₂ : a - b = 0 ⊎ a + b = 0, from !eq_zero_or_eq_zero_of_mul_eq_zero aux₁,
sum.rec_on aux₂
(λ H : a - b = 0, sum.inl (eq_of_sub_eq_zero H))
(λ H : a + b = 0, sum.inr (eq_neg_of_add_eq_zero H)))
(λ H : a = b ⊎ a = -b, sum.rec_on H
(λ a_eq_b, by rewrite a_eq_b)
(λ a_eq_mb, by rewrite [a_eq_mb, neg_mul_neg]))
definition mul_self_eq_one_iff (a : A) : a * a = 1 ↔ a = 1 ⊎ a = -1 :=
assert aux : a * a = 1 * 1 ↔ a = 1 ⊎ a = -1, from mul_self_eq_mul_self_iff a 1,
by rewrite mul_one at aux; exact aux
-- TODO: c - b * c → c = 0 ⊎ b = 1 and variants
definition dvd_of_mul_dvd_mul_left {a b c : A} (Ha : a ≠ 0) (Hdvd : (a * b a * c)) : (b c) :=
dvd.elim Hdvd
(take d,
assume H : a * c = a * b * d,
have H1 : b * d = c, from mul.cancel_left Ha (mul.assoc a b d ▸ H⁻¹),
dvd.intro H1)
definition dvd_of_mul_dvd_mul_right {a b c : A} (Ha : a ≠ 0) (Hdvd : (b * a c * a)) : (b c) :=
dvd.elim Hdvd
(take d,
assume H : c * a = b * a * d,
have H1 : b * d * a = c * a, from by rewrite [mul.right_comm, -H],
have H2 : b * d = c, from mul.cancel_right Ha H1,
dvd.intro H2)
end
end algebra

View file

@ -2,7 +2,7 @@
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.pathover
Module: cubical.pathover
Author: Floris van Doorn
Theorems about pathovers

View file

@ -2,7 +2,7 @@
Copyright (c) 2015 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.square
Module: cubical.square
Author: Floris van Doorn
Theorems about square

View file

@ -73,7 +73,7 @@ namespace sphere
end ops
definition bool_of_sphere [reducible] : sphere 0 → bool :=
suspension.rec tt ff (λx, empty.elim _ x)
suspension.rec tt ff (λx, empty.elim x)
definition sphere_of_bool [reducible] : bool → sphere 0
| tt := !north

View file

@ -15,9 +15,10 @@ import init.ua init.funext
import init.hedberg init.nat init.hit
namespace core
export bool empty unit sum sigma
export bool empty unit sum
export sigma (hiding pr1 pr2)
export [notations] prod
export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd)
export eq (idp idpath concat inverse transport ap ap10 cast tr_inv homotopy ap11 apd refl)
export [declarations] function
export equiv (to_inv to_right_inv to_left_inv)
export is_equiv (inv right_inv left_inv)

View file

@ -151,6 +151,8 @@ namespace iff
definition elim_right (H : a ↔ b) : b → a :=
elim (assume H₁ H₂, H₂) H
definition mp' := @elim_right
definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b :=
intro
(assume Hna, mt (elim_right H₁) Hna)
@ -360,3 +362,24 @@ decidable.rec
definition dite_ite_eq (c : Type) [H : decidable c] {A : Type} (t : A) (e : A) : dite c (λh, t) (λh, e) = ite c t e :=
rfl
end
open eq.ops unit
definition is_unit (c : Type) [H : decidable c] : Type₀ :=
if c then unit else empty
definition is_empty (c : Type) [H : decidable c] : Type₀ :=
if c then empty else unit
theorem of_is_unit {c : Type} [H₁ : decidable c] (H₂ : is_unit c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, empty.rec _ (if_neg Hnc ▸ H₂))
notation `dec_trivial` := of_is_unit star
theorem not_of_not_is_unit {c : Type} [H₁ : decidable c] (H₂ : ¬ is_unit c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, absurd star (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem not_of_is_empty {c : Type} [H₁ : decidable c] (H₂ : is_empty c) : ¬ c :=
decidable.rec_on H₁ (λ Hc, empty.rec _ (if_pos Hc ▸ H₂)) (λ Hnc, Hnc)
theorem of_not_is_empty {c : Type} [H₁ : decidable c] (H₂ : ¬ is_empty c) : c :=
decidable.rec_on H₁ (λ Hc, Hc) (λ Hnc, absurd star (if_neg Hnc ▸ H₂))

View file

@ -2,20 +2,18 @@
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module init.nat
Module: init.nat
Authors: Floris van Doorn, Leonardo de Moura
-/
prelude
import init.wf init.tactic init.hedberg init.util init.types
open eq.ops decidable sum
open eq decidable sum lift
namespace nat
open lift
notation `` := nat
inductive lt (a : nat) : nat → Type :=
inductive lt (a : nat) : nat → Type :=
| base : lt a (succ a)
| step : Π {b}, lt a b → lt a (succ b)
@ -31,43 +29,33 @@ namespace nat
protected definition is_inhabited [instance] : inhabited nat :=
inhabited.mk zero
protected definition has_decidable_eq [instance] : decidable_eq nat :=
λn m : nat,
have general : ∀n, decidable (n = m), from
nat.rec_on m
(λ n, nat.cases_on n
(inl rfl)
(λ m, inr (by contradiction)))
(λ (m' : nat) (ih : ∀n, decidable (n = m')) (n : nat), nat.cases_on n
(inr (λ h, down (nat.no_confusion h)))
(λ (n' : nat),
decidable.rec_on (ih n')
(assume Heq : n' = m', inl (eq.rec_on Heq rfl))
(assume Hne : n' ≠ m',
have H1 : succ n' ≠ succ m', from
assume Heq, down (nat.no_confusion Heq (λ e : n' = m', Hne e)),
inr H1))),
general n
protected definition has_decidable_eq [instance] : ∀ x y : nat, decidable (x = y)
| has_decidable_eq zero zero := inl rfl
| has_decidable_eq (succ x) zero := inr (by contradiction)
| has_decidable_eq zero (succ y) := inr (by contradiction)
| has_decidable_eq (succ x) (succ y) :=
match has_decidable_eq x y with
| inl xeqy := inl (by rewrite xeqy)
| inr xney := inr (λ h : succ x = succ y, by injection h with xeqy; exact absurd xeqy xney)
end
-- less-than is well-founded
definition lt.wf [instance] : well_founded lt :=
well_founded.intro (λn, nat.rec_on n
(acc.intro zero (λ (y : nat) (hlt : y < zero),
have aux : ∀ {n₁}, y < n₁ → zero = n₁ → acc lt y, from
λ n₁ hlt, lt.cases_on hlt
(λ heq, down (nat.no_confusion heq))
(λ b hlt heq, down (nat.no_confusion heq)),
λ n₁ hlt, nat.lt.cases_on hlt
(by contradiction)
(by contradiction),
aux hlt rfl))
(λ (n : nat) (ih : acc lt n),
acc.intro (succ n) (λ (m : nat) (hlt : m < succ n),
have aux : ∀ {n₁} (hlt : m < n₁), succ n = n₁ → acc lt m, from
λ n₁ hlt, lt.cases_on hlt
(λ (heq : succ n = succ m),
down (nat.no_confusion heq (λ (e : n = m),
eq.rec_on e ih)))
(λ b (hlt : m < b) (heq : succ n = succ b),
down (nat.no_confusion heq (λ (e : n = b),
acc.inv (eq.rec_on e ih) hlt))),
λ n₁ hlt, nat.lt.cases_on hlt
(λ (sn_eq_sm : succ n = succ m),
by injection sn_eq_sm with neqm; rewrite neqm at ih; exact ih)
(λ b (hlt : m < b) (sn_eq_sb : succ n = succ b),
by injection sn_eq_sb with neqb; rewrite neqb at ih; exact acc.inv ih hlt),
aux hlt rfl)))
definition measure {A : Type} (f : A → nat) : A → A → Type₀ :=
@ -77,7 +65,7 @@ namespace nat
inv_image.wf f lt.wf
definition not_lt_zero (a : nat) : ¬ a < zero :=
have aux : {b}, a < b → b = zero → empty, from
have aux : Π {b}, a < b → b = zero → empty, from
λ b H, lt.cases_on H
(by contradiction)
(by contradiction),
@ -89,70 +77,68 @@ namespace nat
(λ a (hlt : zero < succ a), lt.step hlt)
definition lt.trans [trans] {a b c : nat} (H₁ : a < b) (H₂ : b < c) : a < c :=
have aux : ∀ {d}, d < c → b = d → a < b → a < c, from
(λ d H, lt.rec_on H
(λ h₁ h₂, lt.step (eq.rec_on h₁ h₂))
(λ b hl ih h₁ h₂, lt.step (ih h₁ h₂))),
aux H₂ rfl H₁
have aux : a < b → a < c, from
lt.rec_on H
(λ h₁, lt.step h₁)
(λ b₁ bb₁ ih h₁, lt.step (ih h₁)),
aux H₁
definition lt.succ_of_lt {a b : nat} (H : a < b) : succ a < succ b :=
definition succ_lt_succ {a b : nat} (H : a < b) : succ a < succ b :=
lt.rec_on H
(lt.base (succ a))
(λ b hlt ih, lt.trans ih (lt.base (succ b)))
definition lt.of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
have aux : ∀ {a₁}, a₁ < b → succ a = a₁ → a < b, from
λ a₁ H, lt.rec_on H
(λ e₁, eq.rec_on e₁ (lt.step (lt.base a)))
(λ d hlt ih e₁, lt.step (ih e₁)),
aux H rfl
definition lt_of_succ_lt {a b : nat} (H : succ a < b) : a < b :=
lt.rec_on H
(lt.step (lt.base a))
(λ b h ih, lt.step ih)
definition lt.of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
definition lt_of_succ_lt_succ {a b : nat} (H : succ a < succ b) : a < b :=
have aux : pred (succ a) < pred (succ b), from
lt.rec_on H
(lt.base a)
(λ (b : nat) (hlt : succ a < b) ih,
show pred (succ a) < pred (succ b), from
lt.of_succ_lt hlt),
lt_of_succ_lt hlt),
aux
definition decidable_lt [instance] : decidable_rel lt :=
λ a b, nat.rec_on b
(λ (a : nat), inr (not_lt_zero a))
(λ (b₁ : nat) (ih : a, decidable (a < b₁)) (a : nat), nat.cases_on a
(λ (b₁ : nat) (ih : Π a, decidable (a < b₁)) (a : nat), nat.cases_on a
(inl !zero_lt_succ)
(λ a, decidable.rec_on (ih a)
(λ h_pos : a < b₁, inl (lt.succ_of_lt h_pos))
(λ h_pos : a < b₁, inl (succ_lt_succ h_pos))
(λ h_neg : ¬ a < b₁,
have aux : ¬ succ a < succ b₁, from
λ h : succ a < succ b₁, h_neg (lt.of_succ_lt_succ h),
λ h : succ a < succ b₁, h_neg (lt_of_succ_lt_succ h),
inr aux)))
a
definition le.refl (a : nat) : a ≤ a :=
lt.base a
definition le.of_lt {a b : nat} (H : a < b) : a ≤ b :=
definition le_of_lt {a b : nat} (H : a < b) : a ≤ b :=
lt.step H
definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : sum (a = b) (a < b) :=
have aux : Π (a₁ b₁ : nat) (hlt : a₁ < b₁), a₁ = a → b₁ = (succ b) → sum (a = b) (a < b), from
λ a₁ b₁ hlt, lt.rec_on hlt
(λ h₁, eq.rec_on h₁ (λ h₂, down (nat.no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inl rfl)))))
(λ b₁ hlt ih h₁, eq.rec_on h₁ (λ h₂, down (nat.no_confusion h₂ (λ h₃, eq.rec_on h₃ (sum.inr hlt))))),
aux a (succ b) H rfl rfl
definition eq_or_lt_of_le {a b : nat} (H : a ≤ b) : a = b ⊎ a < b :=
begin
cases H with b hlt,
apply sum.inl rfl,
apply sum.inr hlt
end
definition le.of_eq_or_lt {a b : nat} (H : sum (a = b) (a < b)) : a ≤ b :=
definition le_of_eq_or_lt {a b : nat} (H : a = b ⊎ a < b) : a ≤ b :=
sum.rec_on H
(λ hl, eq.rec_on hl !le.refl)
(λ hr, le.of_lt hr)
(λ hr, le_of_lt hr)
definition decidable_le [instance] : decidable_rel le :=
λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
λ a b, decidable_iff_equiv _ (iff.intro le_of_eq_or_lt eq_or_lt_of_le)
definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : b, a < b → P b) : P b :=
definition le.rec_on {a : nat} {P : nat → Type} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : Π b, a < b → P b) : P b :=
begin
cases H with b' hlt,
cases H with b hlt,
apply H₁,
apply H₂ b hlt
end
@ -161,25 +147,25 @@ namespace nat
nat.rec_on a
!not_lt_zero
(λ (a : nat) (ih : ¬ a < a) (h : succ a < succ a),
ih (lt.of_succ_lt_succ h))
ih (lt_of_succ_lt_succ h))
definition lt.asymm {a b : nat} (H : a < b) : ¬ b < a :=
lt.rec_on H
(λ h : succ a < a, !lt.irrefl (lt.of_succ_lt h))
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt.of_succ_lt h))
(λ h : succ a < a, !lt.irrefl (lt_of_succ_lt h))
(λ b hlt (ih : ¬ b < a) (h : succ b < a), ih (lt_of_succ_lt h))
definition lt.trichotomy (a b : nat) : a < b ⊎ a = b ⊎ b < a :=
nat.rec_on b
(λa, nat.cases_on a
(sum.inr (sum.inl rfl))
(λ a₁, sum.inr (sum.inr !zero_lt_succ)))
(λ b₁ (ih : a, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), nat.cases_on a
(λ b₁ (ih : Πa, a < b₁ ⊎ a = b₁ ⊎ b₁ < a) (a : nat), nat.cases_on a
(sum.inl !zero_lt_succ)
(λ a, sum.rec_on (ih a)
(λ h : a < b₁, sum.inl (lt.succ_of_lt h))
(λ h : a < b₁, sum.inl (succ_lt_succ h))
(λ h, sum.rec_on h
(λ h : a = b₁, sum.inr (sum.inl (eq.rec_on h rfl)))
(λ h : b₁ < a, sum.inr (sum.inr (lt.succ_of_lt h))))))
(λ h : b₁ < a, sum.inr (sum.inr (succ_lt_succ h))))))
a
definition eq_or_lt_of_not_lt {a b : nat} (hnlt : ¬ a < b) : a = b ⊎ b < a :=
@ -191,13 +177,13 @@ namespace nat
h
definition lt_of_succ_le {a b : nat} (h : succ a ≤ b) : a < b :=
lt.of_succ_lt_succ h
lt_of_succ_lt_succ h
definition le.step {a b : nat} (h : a ≤ b) : a ≤ succ b :=
definition le_succ_of_le {a b : nat} (h : a ≤ b) : a ≤ succ b :=
lt.step h
definition succ_le_of_lt {a b : nat} (h : a < b) : succ a ≤ b :=
lt.succ_of_lt h
succ_lt_succ h
definition le.trans [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b ≤ c) : a ≤ c :=
begin
@ -206,18 +192,18 @@ namespace nat
apply lt.trans hlt h₂
end
definition lt.of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
definition lt_of_le_of_lt [trans] {a b c : nat} (h₁ : a ≤ b) (h₂ : b < c) : a < c :=
begin
cases h₁ with b' hlt,
apply h₂,
apply lt.trans hlt h₂
end
definition lt.of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
definition lt_of_lt_of_le [trans] {a b c : nat} (h₁ : a < b) (h₂ : b ≤ c) : a < c :=
begin
cases h₁ with b' hlt,
apply lt.of_succ_lt_succ h₂,
apply lt.trans hlt (lt.of_succ_lt_succ h₂)
apply lt_of_succ_lt_succ h₂,
apply lt.trans hlt (lt_of_succ_lt_succ h₂)
end
definition max (a b : nat) : nat :=
@ -226,40 +212,44 @@ namespace nat
definition min (a b : nat) : nat :=
if a < b then a else b
definition max_a_a (a : nat) : a = max a a :=
definition max_self (a : nat) : max a a = a :=
eq.rec_on !if_t_t rfl
definition max.eq_right {a b : nat} (H : a < b) : max a b = b :=
definition max_eq_right {a b : nat} (H : a < b) : max a b = b :=
if_pos H
definition max.eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
definition max_eq_left {a b : nat} (H : ¬ a < b) : max a b = a :=
if_neg H
definition max.right_eq {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (max.eq_right H) rfl
definition eq_max_right {a b : nat} (H : a < b) : b = max a b :=
eq.rec_on (max_eq_right H) rfl
definition max.left_eq {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (max.eq_left H) rfl
definition eq_max_left {a b : nat} (H : ¬ a < b) : a = max a b :=
eq.rec_on (max_eq_left H) rfl
definition max.left (a b : nat) : a ≤ max a b :=
definition le_max_left (a b : nat) : a ≤ max a b :=
by_cases
(λ h : a < b, le.of_lt (eq.rec_on (max.right_eq h) h))
(λ h : ¬ a < b, eq.rec_on (max.eq_left h) !le.refl)
(λ h : a < b, le_of_lt (eq.rec_on (eq_max_right h) h))
(λ h : ¬ a < b, eq.rec_on (eq_max_left h) !le.refl)
definition max.right (a b : nat) : b ≤ max a b :=
definition le_max_right (a b : nat) : b ≤ max a b :=
by_cases
(λ h : a < b, eq.rec_on (max.eq_right h) !le.refl)
(λ h : a < b, eq.rec_on (eq_max_right h) !le.refl)
(λ h : ¬ a < b, sum.rec_on (eq_or_lt_of_not_lt h)
(λ heq, eq.rec_on heq (eq.rec_on (max_a_a a) !le.refl))
(λ heq, eq.rec_on heq (eq.rec_on (inverse (max_self a)) !le.refl))
(λ h : b < a,
have aux : a = max a b, from max.left_eq (lt.asymm h),
eq.rec_on aux (le.of_lt h)))
have aux : a = max a b, from eq_max_left (lt.asymm h),
eq.rec_on aux (le_of_lt h)))
abbreviation gt a b := lt b a
definition gt [reducible] a b := lt b a
definition decidable_gt [instance] : decidable_rel gt :=
_
notation a > b := gt a b
abbreviation ge a b := le b a
definition ge [reducible] a b := le b a
definition decidable_ge [instance] : decidable_rel ge :=
_
notation a ≥ b := ge a b
@ -275,12 +265,14 @@ namespace nat
notation a * b := mul a b
section
local attribute sub [reducible]
definition succ_sub_succ_eq_sub (a b : nat) : succ a - succ b = a - b :=
nat.rec_on b
rfl
(λ b₁ (ih : succ a - succ b₁ = a - b₁),
eq.rec_on ih (eq.refl (pred (succ a - succ b₁))))
end
definition sub_eq_succ_sub_succ (a b : nat) : a - b = succ a - succ b :=
eq.rec_on (succ_sub_succ_eq_sub a b) rfl
@ -288,15 +280,12 @@ namespace nat
definition zero_sub_eq_zero (a : nat) : zero - a = zero :=
nat.rec_on a
rfl
(λ a₁ (ih : zero - a₁ = zero), calc
zero - succ a₁ = pred (zero - a₁) : rfl
... = pred zero : ih
... = zero : rfl)
(λ a₁ (ih : zero - a₁ = zero), ap pred ih)
definition zero_eq_zero_sub (a : nat) : zero = zero - a :=
eq.rec_on (zero_sub_eq_zero a) rfl
definition sub.lt {a b : nat} : zero < a → zero < b → a - b < a :=
definition sub_lt {a b : nat} : zero < a → zero < b → a - b < a :=
have aux : Π {a}, zero < a → Π {b}, zero < b → a - b < a, from
λa h₁, lt.rec_on h₁
(λb h₂, lt.cases_on h₂
@ -314,7 +303,7 @@ namespace nat
definition pred_le (a : nat) : pred a ≤ a :=
nat.cases_on a
(le.refl zero)
(λ a₁, le.of_lt (lt.base a₁))
(λ a₁, le_of_lt (lt.base a₁))
definition sub_le (a b : nat) : a - b ≤ a :=
nat.rec_on b

View file

@ -132,7 +132,7 @@ namespace is_trunc
have base : ∀k A, k ≤ -2 → is_trunc k A → (is_trunc -2 A), from
λ k A, trunc_index.cases_on k
(λh1 h2, h2)
(λk h1 h2, empty.elim (is_trunc -2 A) (trunc_index.empty_of_succ_le_minus_two h1)),
(λk h1 h2, empty.elim (trunc_index.empty_of_succ_le_minus_two h1)),
have step : Π (m : trunc_index)
(IHm : Π (n : trunc_index) (A : Type), n ≤ m → is_trunc n A → is_trunc m A)
(n : trunc_index) (A : Type)

View file

@ -14,7 +14,7 @@ import .num .wf
namespace empty
protected theorem elim (A : Type) (H : empty) : A :=
protected theorem elim {A : Type} (H : empty) : A :=
empty.rec (λe, A) H
end empty
@ -57,6 +57,22 @@ namespace sum
reserve infixr `+`:25 -- conflicts with notation for addition
infixr `+` := sum
end low_precedence_plus
variables {a b c d : Type}
definition sum_of_sum_of_imp_of_imp (H₁ : a ⊎ b) (H₂ : a → c) (H₃ : b → d) : c ⊎ d :=
sum.rec_on H₁
(assume Ha : a, sum.inl (H₂ Ha))
(assume Hb : b, sum.inr (H₃ Hb))
definition sum_of_sum_of_imp_left (H₁ : a ⊎ c) (H : a → b) : b ⊎ c :=
sum.rec_on H₁
(assume H₂ : a, sum.inl (H H₂))
(assume H₂ : c, sum.inr H₂)
definition sum_of_sum_of_imp_right (H₁ : c ⊎ a) (H : a → b) : c ⊎ b :=
sum.rec_on H₁
(assume H₂ : c, sum.inl H₂)
(assume H₂ : a, sum.inr (H H₂))
end sum
-- Product type

784
hott/types/int/basic.hlean Normal file
View file

@ -0,0 +1,784 @@
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: int.basic
Authors: Floris van Doorn, Jeremy Avigad
The integers, with addition, multiplication, and subtraction. The representation of the integers is
chosen to compute efficiently.
To faciliate proving things about these operations, we show that the integers are a quotient of
× with the usual equivalence relation, ≡, and functions
abstr : ×
repr : ×
satisfying:
abstr_repr (a : ) : abstr (repr a) = a
repr_abstr (p : × ) : repr (abstr p) ≡ p
abstr_eq (p q : × ) : p ≡ q → abstr p = abstr q
For example, to "lift" statements about add to statements about padd, we need to prove the
following:
repr_add (a b : ) : repr (a + b) = padd (repr a) (repr b)
padd_congr (p p' q q' : × ) (H1 : p ≡ p') (H2 : q ≡ q') : padd p q ≡ p' q'
Ported from standard library
-/
import types.nat.sub algebra.relation types.prod
open core nat decidable prod relation prod
/- the type of integers -/
inductive int : Type :=
| of_nat : nat → int
| neg_succ_of_nat : nat → int
notation `` := int
attribute int.of_nat [coercion]
definition int.of_num [coercion] [reducible] (n : num) : := int.of_nat (nat.of_num n)
namespace int
/- definitions of basic functions -/
definition neg_of_nat (m : ) : :=
nat.cases_on m 0 (take m', neg_succ_of_nat m')
definition sub_nat_nat (m n : ) : :=
nat.cases_on (n - m)
(of_nat (m - n)) -- m ≥ n
(take k, neg_succ_of_nat k) -- m < n, and n - m = succ k
definition neg (a : ) : :=
int.cases_on a
(take m, -- a = of_nat m
nat.cases_on m 0 (take m', neg_succ_of_nat m'))
(take m, of_nat (succ m)) -- a = neg_succ_of_nat m
definition add (a b : ) : :=
int.cases_on a
(take m, -- a = of_nat m
int.cases_on b
(take n, of_nat (m + n)) -- b = of_nat n
(take n, sub_nat_nat m (succ n))) -- b = neg_succ_of_nat n
(take m, -- a = neg_succ_of_nat m
int.cases_on b
(take n, sub_nat_nat n (succ m)) -- b = of_nat n
(take n, neg_of_nat (succ m + succ n))) -- b = neg_succ_of_nat n
definition mul (a b : ) : :=
int.cases_on a
(take m, -- a = of_nat m
int.cases_on b
(take n, of_nat (m * n)) -- b = of_nat n
(take n, neg_of_nat (m * succ n))) -- b = neg_succ_of_nat n
(take m, -- a = neg_succ_of_nat m
int.cases_on b
(take n, neg_of_nat (succ m * n)) -- b = of_nat n
(take n, of_nat (succ m * succ n))) -- b = neg_succ_of_nat n
/- notation -/
notation `-[` n `+1]` := int.neg_succ_of_nat n -- for pretty-printing output
prefix - := int.neg
infix + := int.add
infix * := int.mul
/- some basic functions and properties -/
definition of_nat.inj {m n : } (H : of_nat m = of_nat n) : m = n :=
by injection H; assumption
definition neg_succ_of_nat.inj {m n : } (H : neg_succ_of_nat m = neg_succ_of_nat n) : m = n :=
by injection H; assumption
definition neg_succ_of_nat_eq (n : ) : -[n +1] = -(n + 1) := rfl
definition has_decidable_eq [instance] : decidable_eq :=
take a b,
int.cases_on a
(take m,
int.cases_on b
(take n,
if H : m = n then inl (ap of_nat H) else inr (take H1, H (of_nat.inj H1)))
(take n', inr (by contradiction)))
(take m',
int.cases_on b
(take n, inr (by contradiction))
(take n',
(if H : m' = n' then inl (ap neg_succ_of_nat H) else
inr (take H1, H (neg_succ_of_nat.inj H1)))))
definition of_nat_add_of_nat (n m : nat) : of_nat n + of_nat m = #nat n + m := rfl
definition of_nat_succ (n : ) : of_nat (succ n) = of_nat n + 1 := rfl
definition of_nat_mul_of_nat (n m : ) : of_nat n * of_nat m = n * m := rfl
definition sub_nat_nat_of_ge {m n : } (H : m ≥ n) : sub_nat_nat m n = of_nat (m - n) :=
have H1 : n - m = 0, from sub_eq_zero_of_le H,
calc
sub_nat_nat m n = nat.cases_on 0 (of_nat (m - n)) _ : H1 ▸ rfl
... = of_nat (m - n) : rfl
section
local attribute sub_nat_nat [reducible]
definition sub_nat_nat_of_lt {m n : } (H : m < n) :
sub_nat_nat m n = neg_succ_of_nat (pred (n - m)) :=
have H1 : n - m = succ (pred (n - m)), from (succ_pred_of_pos (sub_pos_of_lt H))⁻¹,
calc
sub_nat_nat m n = nat.cases_on (succ (pred (n - m))) (of_nat (m - n))
(take k, neg_succ_of_nat k) : H1 ▸ rfl
... = neg_succ_of_nat (pred (n - m)) : rfl
end
definition nat_abs (a : ) : := int.cases_on a (take n, n) (take n', succ n')
definition nat_abs_of_nat (n : ) : nat_abs (of_nat n) = n := rfl
definition nat_abs_eq_zero {a : } : nat_abs a = 0 → a = 0 :=
int.cases_on a
(take m, assume H : nat_abs (of_nat m) = 0, ap of_nat H)
(take m', assume H : nat_abs (neg_succ_of_nat m') = 0, absurd H (succ_ne_zero _))
/- int is a quotient of ordered pairs of natural numbers -/
protected definition equiv (p q : × ) : Type₀ := pr1 p + pr2 q = pr2 p + pr1 q
local infix `≡` := int.equiv
protected theorem equiv.refl [refl] {p : × } : p ≡ p := !add.comm
protected theorem equiv.symm [symm] {p q : × } (H : p ≡ q) : q ≡ p :=
calc
pr1 q + pr2 p = pr2 p + pr1 q : !add.comm
... = pr1 p + pr2 q : H⁻¹
... = pr2 q + pr1 p : !add.comm
protected theorem equiv.trans [trans] {p q r : × } (H1 : p ≡ q) (H2 : q ≡ r) : p ≡ r :=
have H3 : pr1 p + pr2 r + pr2 q = pr2 p + pr1 r + pr2 q, from
calc
pr1 p + pr2 r + pr2 q = pr1 p + pr2 q + pr2 r : by exact sorry
... = pr2 p + pr1 q + pr2 r : {H1}
... = pr2 p + (pr1 q + pr2 r) : by exact sorry
... = pr2 p + (pr2 q + pr1 r) : {H2}
... = pr2 p + pr1 r + pr2 q : by exact sorry,
show pr1 p + pr2 r = pr2 p + pr1 r, from add.cancel_right H3
protected definition equiv_equiv : is_equivalence equiv :=
is_equivalence.mk @equiv.refl @equiv.symm @equiv.trans
protected definition equiv_cases {p q : × } (H : equiv p q) :
(pr1 p ≥ pr2 p × pr1 q ≥ pr2 q) ⊎ (pr1 p < pr2 p × pr1 q < pr2 q) :=
sum.rec_on (@le_or_gt (pr2 p) (pr1 p))
(assume H1: pr1 p ≥ pr2 p,
have H2 : pr2 p + pr1 q ≥ pr2 p + pr2 q, from H ▸ add_le_add_right H1 (pr2 q),
sum.inl (pair H1 (le_of_add_le_add_left H2)))
(assume H1: pr1 p < pr2 p,
have H2 : pr2 p + pr1 q < pr2 p + pr2 q, from H ▸ add_lt_add_right H1 (pr2 q),
sum.inr (pair H1 (lt_of_add_lt_add_left H2)))
protected definition equiv_of_eq {p q : × } (H : p = q) : p ≡ q := H ▸ equiv.refl
/- the representation and abstraction functions -/
definition abstr (a : × ) : := sub_nat_nat (pr1 a) (pr2 a)
definition abstr_of_ge {p : × } (H : pr1 p ≥ pr2 p) : abstr p = of_nat (pr1 p - pr2 p) :=
sub_nat_nat_of_ge H
definition abstr_of_lt {p : × } (H : pr1 p < pr2 p) :
abstr p = neg_succ_of_nat (pred (pr2 p - pr1 p)) :=
sub_nat_nat_of_lt H
definition repr (a : ) : × := int.cases_on a (take m, (m, 0)) (take m, (0, succ m))
definition abstr_repr (a : ) : abstr (repr a) = a :=
int.cases_on a (take m, (sub_nat_nat_of_ge (zero_le m))) (take m, rfl)
definition repr_sub_nat_nat (m n : ) : repr (sub_nat_nat m n) ≡ (m, n) :=
sum.rec_on (@le_or_gt n m)
(take H : m ≥ n,
have H1 : repr (sub_nat_nat m n) = (m - n, 0), from sub_nat_nat_of_ge H ▸ rfl,
H1⁻¹ ▸
(calc
m - n + n = m : sub_add_cancel H
... = 0 + m : zero_add))
(take H : m < n,
have H1 : repr (sub_nat_nat m n) = (0, succ (pred (n - m))), from sub_nat_nat_of_lt H ▸ rfl,
H1⁻¹ ▸
(calc
0 + n = n : zero_add
... = n - m + m : sub_add_cancel (le_of_lt H)
... = succ (pred (n - m)) + m : (succ_pred_of_pos (sub_pos_of_lt H))⁻¹ᵖ))
definition repr_abstr (p : × ) : repr (abstr p) ≡ p :=
!prod.eta ▸ !repr_sub_nat_nat
definition abstr_eq {p q : × } (Hequiv : p ≡ q) : abstr p = abstr q :=
sum.rec_on (equiv_cases Hequiv)
(assume H2,
have H3 : pr1 p ≥ pr2 p, from prod.pr1 H2,
have H4 : pr1 q ≥ pr2 q, from prod.pr2 H2,
have H5 : pr1 p = pr1 q - pr2 q + pr2 p, from
calc
pr1 p = pr1 p + pr2 q - pr2 q : add_sub_cancel
... = pr2 p + pr1 q - pr2 q : by rewrite [↑int.equiv at Hequiv,Hequiv]
... = pr2 p + (pr1 q - pr2 q) : add_sub_assoc H4
... = pr1 q - pr2 q + pr2 p : add.comm,
have H6 : pr1 p - pr2 p = pr1 q - pr2 q, from
calc
pr1 p - pr2 p = pr1 q - pr2 q + pr2 p - pr2 p : H5
... = pr1 q - pr2 q : add_sub_cancel,
abstr_of_ge H3 ⬝ ap of_nat H6 ⬝ (abstr_of_ge H4)⁻¹)
(assume H2,
have H3 : pr1 p < pr2 p, from prod.pr1 H2,
have H4 : pr1 q < pr2 q, from prod.pr2 H2,
have H5 : pr2 p = pr2 q - pr1 q + pr1 p, from
calc
pr2 p = pr2 p + pr1 q - pr1 q : add_sub_cancel
... = pr1 p + pr2 q - pr1 q : by rewrite [↑int.equiv at Hequiv,Hequiv]
... = pr1 p + (pr2 q - pr1 q) : add_sub_assoc (le_of_lt H4)
... = pr2 q - pr1 q + pr1 p : add.comm,
have H6 : pr2 p - pr1 p = pr2 q - pr1 q, from
calc
pr2 p - pr1 p = pr2 q - pr1 q + pr1 p - pr1 p : H5
... = pr2 q - pr1 q : add_sub_cancel,
abstr_of_lt H3 ⬝ ap neg_succ_of_nat (ap pred H6)⬝ (abstr_of_lt H4)⁻¹)
definition equiv_iff (p q : × ) : (p ≡ q) ↔ ((p ≡ p) × (q ≡ q) × (abstr p = abstr q)) :=
iff.intro
(assume H : equiv p q,
pair !equiv.refl (pair !equiv.refl (abstr_eq H)))
(assume H : equiv p p × equiv q q × abstr p = abstr q,
have H1 : abstr p = abstr q, from prod.pr2 (prod.pr2 H),
equiv.trans (H1 ▸ equiv.symm (repr_abstr p)) (repr_abstr q))
definition eq_abstr_of_equiv_repr {a : } {p : × } (Hequiv : repr a ≡ p) : a = abstr p :=
calc
a = abstr (repr a) : abstr_repr
... = abstr p : abstr_eq Hequiv
definition eq_of_repr_equiv_repr {a b : } (H : repr a ≡ repr b) : a = b :=
calc
a = abstr (repr a) : abstr_repr
... = abstr (repr b) : abstr_eq H
... = b : abstr_repr
section
local attribute abstr [reducible]
local attribute dist [reducible]
definition nat_abs_abstr (p : × ) : nat_abs (abstr p) = dist (pr1 p) (pr2 p) :=
let m := pr1 p, n := pr2 p in
sum.rec_on (@le_or_gt n m)
(assume H : m ≥ n,
calc
nat_abs (abstr (m, n)) = nat_abs (of_nat (m - n)) : int.abstr_of_ge H
... = dist m n : dist_eq_sub_of_ge H)
(assume H : m < n,
calc
nat_abs (abstr (m, n)) = nat_abs (neg_succ_of_nat (pred (n - m))) : int.abstr_of_lt H
... = succ (pred (n - m)) : rfl
... = n - m : succ_pred_of_pos (sub_pos_of_lt H)
... = dist m n : dist_eq_sub_of_le (le_of_lt H))
end
definition cases_of_nat (a : ) : (Σn : , a = of_nat n) ⊎ (Σn : , a = - of_nat n) :=
int.cases_on a
(take n, sum.inl (sigma.mk n rfl))
(take n', sum.inr (sigma.mk (succ n') rfl))
definition cases_of_nat_succ (a : ) : (Σn : , a = of_nat n) ⊎ (Σn : , a = - (of_nat (succ n))) :=
int.cases_on a (take m, sum.inl (sigma.mk _ rfl)) (take m, sum.inr (sigma.mk _ rfl))
definition by_cases_of_nat {P : → Type} (a : )
(H1 : Πn : , P (of_nat n)) (H2 : Πn : , P (- of_nat n)) :
P a :=
sum.rec_on (cases_of_nat a)
(assume H, obtain (n : ) (H3 : a = n), from H, H3⁻¹ ▸ H1 n)
(assume H, obtain (n : ) (H3 : a = -n), from H, H3⁻¹ ▸ H2 n)
definition by_cases_of_nat_succ {P : → Type} (a : )
(H1 : Πn : , P (of_nat n)) (H2 : Πn : , P (- of_nat (succ n))) :
P a :=
sum.rec_on (cases_of_nat_succ a)
(assume H, obtain (n : ) (H3 : a = n), from H, H3⁻¹ ▸ H1 n)
(assume H, obtain (n : ) (H3 : a = -(succ n)), from H, H3⁻¹ ▸ H2 n)
/-
int is a ring
-/
/- addition -/
definition padd (p q : × ) : × := (pr1 p + pr1 q, pr2 p + pr2 q)
definition repr_add (a b : ) : repr (add a b) ≡ padd (repr a) (repr b) :=
int.cases_on a
(take m,
int.cases_on b
(take n, !equiv.refl)
(take n',
have H1 : equiv (repr (add (of_nat m) (neg_succ_of_nat n'))) (m, succ n'),
from !repr_sub_nat_nat,
have H2 : padd (repr (of_nat m)) (repr (neg_succ_of_nat n')) = (m, 0 + succ n'),
from rfl,
(!zero_add ▸ H2)⁻¹ ▸ H1))
(take m',
int.cases_on b
(take n,
have H1 : equiv (repr (add (neg_succ_of_nat m') (of_nat n))) (n, succ m'),
from !repr_sub_nat_nat,
have H2 : padd (repr (neg_succ_of_nat m')) (repr (of_nat n)) = (0 + n, succ m'),
from rfl,
(!zero_add ▸ H2)⁻¹ ▸ H1)
(take n',!repr_sub_nat_nat))
definition padd_congr {p p' q q' : × } (Ha : p ≡ p') (Hb : q ≡ q') : padd p q ≡ padd p' q' :=
calc
pr1 (padd p q) + pr2 (padd p' q') = pr1 p + pr2 p' + (pr1 q + pr2 q') : by exact sorry
... = pr2 p + pr1 p' + (pr1 q + pr2 q') : {Ha}
... = pr2 p + pr1 p' + (pr2 q + pr1 q') : {Hb}
... = pr2 (padd p q) + pr1 (padd p' q') : by exact sorry
definition padd_comm (p q : × ) : padd p q = padd q p :=
calc
padd p q = (pr1 p + pr1 q, pr2 p + pr2 q) : rfl
... = (pr1 q + pr1 p, pr2 p + pr2 q) : add.comm
... = (pr1 q + pr1 p, pr2 q + pr2 p) : add.comm
... = padd q p : rfl
definition padd_assoc (p q r : × ) : padd (padd p q) r = padd p (padd q r) :=
calc
padd (padd p q) r = (pr1 p + pr1 q + pr1 r, pr2 p + pr2 q + pr2 r) : rfl
... = (pr1 p + (pr1 q + pr1 r), pr2 p + pr2 q + pr2 r) : add.assoc
... = (pr1 p + (pr1 q + pr1 r), pr2 p + (pr2 q + pr2 r)) : add.assoc
... = padd p (padd q r) : rfl
definition add.comm (a b : ) : a + b = b + a :=
begin
apply eq_of_repr_equiv_repr,
apply equiv.trans,
apply repr_add,
apply equiv.symm,
apply eq.subst (padd_comm (repr b) (repr a)),
apply repr_add
end
definition add.assoc (a b c : ) : a + b + c = a + (b + c) :=
assert H1 : repr (a + b + c) ≡ padd (padd (repr a) (repr b)) (repr c), from
equiv.trans (repr_add (a + b) c) (padd_congr !repr_add !equiv.refl),
assert H2 : repr (a + (b + c)) ≡ padd (repr a) (padd (repr b) (repr c)), from
equiv.trans (repr_add a (b + c)) (padd_congr !equiv.refl !repr_add),
begin
apply eq_of_repr_equiv_repr,
apply equiv.trans,
apply H1,
apply eq.subst (padd_assoc _ _ _)⁻¹,
apply equiv.symm,
apply H2
end
definition add_zero (a : ) : a + 0 = a := int.cases_on a (take m, rfl) (take m', rfl)
definition zero_add (a : ) : 0 + a = a := add.comm a 0 ▸ add_zero a
/- negation -/
definition pneg (p : × ) : × := (pr2 p, pr1 p)
-- note: this is =, not just ≡
definition repr_neg (a : ) : repr (- a) = pneg (repr a) :=
int.cases_on a
(take m,
nat.cases_on m rfl (take m', rfl))
(take m', rfl)
definition pneg_congr {p p' : × } (H : p ≡ p') : pneg p ≡ pneg p' := inverse H
definition pneg_pneg (p : × ) : pneg (pneg p) = p := !prod.eta
definition nat_abs_neg (a : ) : nat_abs (-a) = nat_abs a :=
calc
nat_abs (-a) = nat_abs (abstr (repr (-a))) : abstr_repr
... = nat_abs (abstr (pneg (repr a))) : repr_neg
... = dist (pr1 (pneg (repr a))) (pr2 (pneg (repr a))) : nat_abs_abstr
... = dist (pr2 (pneg (repr a))) (pr1 (pneg (repr a))) : dist.comm
... = nat_abs (abstr (repr a)) : nat_abs_abstr
... = nat_abs a : abstr_repr
definition padd_pneg (p : × ) : padd p (pneg p) ≡ (0, 0) :=
show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add.comm ▸ rfl
definition padd_padd_pneg (p q : × ) : padd (padd p q) (pneg q) ≡ p :=
show pr1 p + pr1 q + pr2 q + pr2 p = pr2 p + pr2 q + pr1 q + pr1 p, from by exact sorry
definition add.left_inv (a : ) : -a + a = 0 :=
have H : repr (-a + a) ≡ repr 0, from
calc
repr (-a + a) ≡ padd (repr (neg a)) (repr a) : repr_add
... ≡ padd (pneg (repr a)) (repr a) : sorry
... ≡ repr 0 : padd_pneg,
eq_of_repr_equiv_repr H
/- nat abs -/
definition pabs (p : × ) : := dist (pr1 p) (pr2 p)
definition pabs_congr {p q : × } (H : p ≡ q) : pabs p = pabs q :=
calc
pabs p = nat_abs (abstr p) : nat_abs_abstr
... = nat_abs (abstr q) : abstr_eq H
... = pabs q : nat_abs_abstr
definition nat_abs_eq_pabs_repr (a : ) : nat_abs a = pabs (repr a) :=
calc
nat_abs a = nat_abs (abstr (repr a)) : abstr_repr
... = pabs (repr a) : nat_abs_abstr
definition nat_abs_add_le (a b : ) : nat_abs (a + b) ≤ nat_abs a + nat_abs b :=
have H : nat_abs (a + b) = pabs (padd (repr a) (repr b)), from
calc
nat_abs (a + b) = pabs (repr (a + b)) : nat_abs_eq_pabs_repr
... = pabs (padd (repr a) (repr b)) : pabs_congr !repr_add,
have H1 : nat_abs a = pabs (repr a), from !nat_abs_eq_pabs_repr,
have H2 : nat_abs b = pabs (repr b), from !nat_abs_eq_pabs_repr,
have H3 : pabs (padd (repr a) (repr b)) ≤ pabs (repr a) + pabs (repr b),
from !dist_add_add_le_add_dist_dist,
H⁻¹ ▸ H1⁻¹ ▸ H2⁻¹ ▸ H3
section
local attribute nat_abs [reducible]
definition mul_nat_abs (a b : ) : nat_abs (a * b) = #nat (nat_abs a) * (nat_abs b) :=
int.cases_on a
(take m,
int.cases_on b
(take n, rfl)
(take n', !nat_abs_neg ▸ rfl))
(take m',
int.cases_on b
(take n, !nat_abs_neg ▸ rfl)
(take n', rfl))
end
/- multiplication -/
definition pmul (p q : × ) : × :=
(pr1 p * pr1 q + pr2 p * pr2 q, pr1 p * pr2 q + pr2 p * pr1 q)
definition repr_neg_of_nat (m : ) : repr (neg_of_nat m) = (0, m) :=
nat.cases_on m rfl (take m', rfl)
-- note: we have =, not just ≡
definition repr_mul (a b : ) : repr (mul a b) = pmul (repr a) (repr b) :=
int.cases_on a
(take m,
int.cases_on b
(take n,
(calc
pmul (repr m) (repr n) = (m * n + 0 * 0, m * 0 + 0 * n) : rfl
... = (m * n + 0 * 0, m * 0 + 0) : zero_mul)⁻¹)
(take n',
(calc
pmul (repr m) (repr (neg_succ_of_nat n')) =
(m * 0 + 0 * succ n', m * succ n' + 0 * 0) : rfl
... = (m * 0 + 0, m * succ n' + 0 * 0) : zero_mul
... = repr (mul m (neg_succ_of_nat n')) : repr_neg_of_nat)⁻¹))
(take m',
int.cases_on b
(take n,
(calc
pmul (repr (neg_succ_of_nat m')) (repr n) =
(0 * n + succ m' * 0, 0 * 0 + succ m' * n) : rfl
... = (0 + succ m' * 0, 0 * 0 + succ m' * n) : zero_mul
... = (0 + succ m' * 0, succ m' * n) : {!nat.zero_add}
... = repr (mul (neg_succ_of_nat m') n) : repr_neg_of_nat)⁻¹)
(take n',
(calc
pmul (repr (neg_succ_of_nat m')) (repr (neg_succ_of_nat n')) =
(0 + succ m' * succ n', 0 * succ n') : rfl
... = (succ m' * succ n', 0 * succ n') : nat.zero_add
... = (succ m' * succ n', 0) : zero_mul
... = repr (mul (neg_succ_of_nat m') (neg_succ_of_nat n')) : rfl)⁻¹))
definition equiv_mul_prep {xa ya xb yb xn yn xm ym : }
(H1 : xa + yb = ya + xb) (H2 : xn + ym = yn + xm)
: xa * xn + ya * yn + (xb * ym + yb * xm) = xa * yn + ya * xn + (xb * xm + yb * ym) :=
have H3 : xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
= xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn)), from
calc
xa * xn + ya * yn + (xb * ym + yb * xm) + (yb * xn + xb * yn + (xb * xn + yb * yn))
= xa * xn + yb * xn + (ya * yn + xb * yn) + (xb * xn + xb * ym + (yb * yn + yb * xm))
: by exact sorry
... = (xa + yb) * xn + (ya + xb) * yn + (xb * (xn + ym) + yb * (yn + xm)) : by exact sorry
... = (ya + xb) * xn + (xa + yb) * yn + (xb * (yn + xm) + yb * (xn + ym)) : by exact sorry
... = ya * xn + xb * xn + (xa * yn + yb * yn) + (xb * yn + xb * xm + (yb*xn + yb*ym))
: by exact sorry
... = xa * yn + ya * xn + (xb * xm + yb * ym) + (yb * xn + xb * yn + (xb * xn + yb * yn))
: by exact sorry,
nat.add.cancel_right H3
definition pmul_congr {p p' q q' : × } (H1 : p ≡ p') (H2 : q ≡ q') : pmul p q ≡ pmul p' q' :=
equiv_mul_prep H1 H2
definition pmul_comm (p q : × ) : pmul p q = pmul q p :=
calc
(pr1 p * pr1 q + pr2 p * pr2 q, pr1 p * pr2 q + pr2 p * pr1 q) =
(pr1 q * pr1 p + pr2 p * pr2 q, pr1 p * pr2 q + pr2 p * pr1 q) : mul.comm
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 p * pr2 q + pr2 p * pr1 q) : mul.comm
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr2 p * pr1 q) : mul.comm
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr2 q * pr1 p + pr1 q * pr2 p) : mul.comm
... = (pr1 q * pr1 p + pr2 q * pr2 p, pr1 q * pr2 p + pr2 q * pr1 p) : nat.add.comm
definition mul.comm (a b : ) : a * b = b * a :=
eq_of_repr_equiv_repr
((calc
repr (a * b) = pmul (repr a) (repr b) : repr_mul
... = pmul (repr b) (repr a) : pmul_comm
... = repr (b * a) : repr_mul) ▸ !equiv.refl)
definition pmul_assoc (p q r: × ) : pmul (pmul p q) r = pmul p (pmul q r) :=
by exact sorry
definition mul.assoc (a b c : ) : (a * b) * c = a * (b * c) :=
eq_of_repr_equiv_repr
((calc
repr (a * b * c) = pmul (repr (a * b)) (repr c) : repr_mul
... = pmul (pmul (repr a) (repr b)) (repr c) : repr_mul
... = pmul (repr a) (pmul (repr b) (repr c)) : pmul_assoc
... = pmul (repr a) (repr (b * c)) : repr_mul
... = repr (a * (b * c)) : repr_mul) ▸ !equiv.refl)
definition mul_one (a : ) : a * 1 = a :=
eq_of_repr_equiv_repr (equiv_of_eq
((calc
repr (a * 1) = pmul (repr a) (repr 1) : repr_mul
... = (pr1 (repr a), pr2 (repr a)) : by exact sorry
... = repr a : prod.eta)))
definition one_mul (a : ) : 1 * a = a :=
mul.comm a 1 ▸ mul_one a
definition mul.right_distrib (a b c : ) : (a + b) * c = a * c + b * c :=
eq_of_repr_equiv_repr
(calc
repr ((a + b) * c) = pmul (repr (a + b)) (repr c) : repr_mul
... ≡ pmul (padd (repr a) (repr b)) (repr c) : pmul_congr !repr_add equiv.refl
... = padd (pmul (repr a) (repr c)) (pmul (repr b) (repr c)) : by exact sorry
... = padd (repr (a * c)) (pmul (repr b) (repr c)) : {(repr_mul a c)⁻¹}
... = padd (repr (a * c)) (repr (b * c)) : repr_mul
... ≡ repr (a * c + b * c) : equiv.symm !repr_add)
definition mul.left_distrib (a b c : ) : a * (b + c) = a * b + a * c :=
calc
a * (b + c) = (b + c) * a : mul.comm a (b + c)
... = b * a + c * a : mul.right_distrib b c a
... = a * b + c * a : {mul.comm b a}
... = a * b + a * c : {mul.comm c a}
definition zero_ne_one : (typeof 0 : int) ≠ 1 :=
assume H : 0 = 1,
show empty, from succ_ne_zero 0 ((of_nat.inj H)⁻¹)
definition eq_zero_or_eq_zero_of_mul_eq_zero {a b : } (H : a * b = 0) : a = 0 ⊎ b = 0 :=
have H2 : (nat_abs a) * (nat_abs b) = nat.zero, from
calc
(nat_abs a) * (nat_abs b) = (nat_abs (a * b)) : (mul_nat_abs a b)⁻¹
... = (nat_abs 0) : {H}
... = nat.zero : nat_abs_of_nat nat.zero,
have H3 : (nat_abs a) = nat.zero ⊎ (nat_abs b) = nat.zero,
from eq_zero_or_eq_zero_of_mul_eq_zero H2,
sum_of_sum_of_imp_of_imp H3
(assume H : (nat_abs a) = nat.zero, nat_abs_eq_zero H)
(assume H : (nat_abs b) = nat.zero, nat_abs_eq_zero H)
section
open [classes] algebra
protected definition integral_domain [instance] [reducible] : algebra.integral_domain int :=
⦃algebra.integral_domain,
add := add,
add_assoc := add.assoc,
zero := zero,
zero_add := zero_add,
add_zero := add_zero,
neg := neg,
add_left_inv := add.left_inv,
add_comm := add.comm,
mul := mul,
mul_assoc := mul.assoc,
one := (of_num 1),
one_mul := one_mul,
mul_one := mul_one,
left_distrib := mul.left_distrib,
right_distrib := mul.right_distrib,
mul_comm := mul.comm,
eq_zero_or_eq_zero_of_mul_eq_zero := @eq_zero_or_eq_zero_of_mul_eq_zero,
is_hset_carrier := is_hset_of_decidable_eq⦄
end
/- instantiate ring theorems to int -/
section port_algebra
open [classes] algebra
definition mul.left_comm : Πa b c : , a * (b * c) = b * (a * c) := algebra.mul.left_comm
definition mul.right_comm : Πa b c : , (a * b) * c = (a * c) * b := algebra.mul.right_comm
definition add.left_comm : Πa b c : , a + (b + c) = b + (a + c) := algebra.add.left_comm
definition add.right_comm : Πa b c : , (a + b) + c = (a + c) + b := algebra.add.right_comm
definition add.left_cancel : Π{a b c : }, a + b = a + c → b = c := @algebra.add.left_cancel _ _
definition add.right_cancel : Π{a b c : }, a + b = c + b → a = c := @algebra.add.right_cancel _ _
definition neg_add_cancel_left : Πa b : , -a + (a + b) = b := algebra.neg_add_cancel_left
definition neg_add_cancel_right : Πa b : , a + -b + b = a := algebra.neg_add_cancel_right
definition neg_eq_of_add_eq_zero : Π{a b : }, a + b = 0 → -a = b :=
@algebra.neg_eq_of_add_eq_zero _ _
definition neg_zero : -0 = 0 := algebra.neg_zero
definition neg_neg : Πa : , -(-a) = a := algebra.neg_neg
definition neg.inj : Π{a b : }, -a = -b → a = b := @algebra.neg.inj _ _
definition neg_eq_neg_iff_eq : Πa b : , -a = -b ↔ a = b := algebra.neg_eq_neg_iff_eq
definition neg_eq_zero_iff_eq_zero : Πa : , -a = 0 ↔ a = 0 := algebra.neg_eq_zero_iff_eq_zero
definition eq_neg_of_eq_neg : Π{a b : }, a = -b → b = -a := @algebra.eq_neg_of_eq_neg _ _
definition eq_neg_iff_eq_neg : Π{a b : }, a = -b ↔ b = -a := @algebra.eq_neg_iff_eq_neg _ _
definition add.right_inv : Πa : , a + -a = 0 := algebra.add.right_inv
definition add_neg_cancel_left : Πa b : , a + (-a + b) = b := algebra.add_neg_cancel_left
definition add_neg_cancel_right : Πa b : , a + b + -b = a := algebra.add_neg_cancel_right
definition neg_add_rev : Πa b : , -(a + b) = -b + -a := algebra.neg_add_rev
definition eq_add_neg_of_add_eq : Π{a b c : }, a + c = b → a = b + -c :=
@algebra.eq_add_neg_of_add_eq _ _
definition eq_neg_add_of_add_eq : Π{a b c : }, b + a = c → a = -b + c :=
@algebra.eq_neg_add_of_add_eq _ _
definition neg_add_eq_of_eq_add : Π{a b c : }, b = a + c → -a + b = c :=
@algebra.neg_add_eq_of_eq_add _ _
definition add_neg_eq_of_eq_add : Π{a b c : }, a = c + b → a + -b = c :=
@algebra.add_neg_eq_of_eq_add _ _
definition eq_add_of_add_neg_eq : Π{a b c : }, a + -c = b → a = b + c :=
@algebra.eq_add_of_add_neg_eq _ _
definition eq_add_of_neg_add_eq : Π{a b c : }, -b + a = c → a = b + c :=
@algebra.eq_add_of_neg_add_eq _ _
definition add_eq_of_eq_neg_add : Π{a b c : }, b = -a + c → a + b = c :=
@algebra.add_eq_of_eq_neg_add _ _
definition add_eq_of_eq_add_neg : Π{a b c : }, a = c + -b → a + b = c :=
@algebra.add_eq_of_eq_add_neg _ _
definition add_eq_iff_eq_neg_add : Πa b c : , a + b = c ↔ b = -a + c :=
@algebra.add_eq_iff_eq_neg_add _ _
definition add_eq_iff_eq_add_neg : Πa b c : , a + b = c ↔ a = c + -b :=
@algebra.add_eq_iff_eq_add_neg _ _
definition sub (a b : ) : := algebra.sub a b
infix - := int.sub
definition sub_eq_add_neg : Πa b : , a - b = a + -b := algebra.sub_eq_add_neg
definition sub_self : Πa : , a - a = 0 := algebra.sub_self
definition sub_add_cancel : Πa b : , a - b + b = a := algebra.sub_add_cancel
definition add_sub_cancel : Πa b : , a + b - b = a := algebra.add_sub_cancel
definition eq_of_sub_eq_zero : Π{a b : }, a - b = 0 → a = b := @algebra.eq_of_sub_eq_zero _ _
definition eq_iff_sub_eq_zero : Πa b : , a = b ↔ a - b = 0 := algebra.eq_iff_sub_eq_zero
definition zero_sub : Πa : , 0 - a = -a := algebra.zero_sub
definition sub_zero : Πa : , a - 0 = a := algebra.sub_zero
definition sub_neg_eq_add : Πa b : , a - (-b) = a + b := algebra.sub_neg_eq_add
definition neg_sub : Πa b : , -(a - b) = b - a := algebra.neg_sub
definition add_sub : Πa b c : , a + (b - c) = a + b - c := algebra.add_sub
definition sub_add_eq_sub_sub_swap : Πa b c : , a - (b + c) = a - c - b :=
algebra.sub_add_eq_sub_sub_swap
definition sub_eq_iff_eq_add : Πa b c : , a - b = c ↔ a = c + b := algebra.sub_eq_iff_eq_add
definition eq_sub_iff_add_eq : Πa b c : , a = b - c ↔ a + c = b := algebra.eq_sub_iff_add_eq
definition eq_iff_eq_of_sub_eq_sub : Π{a b c d : }, a - b = c - d → (a = b ↔ c = d) :=
@algebra.eq_iff_eq_of_sub_eq_sub _ _
definition eq_sub_of_add_eq : Π{a b c : }, a + c = b → a = b - c := @algebra.eq_sub_of_add_eq _ _
definition sub_eq_of_eq_add : Π{a b c : }, a = c + b → a - b = c := @algebra.sub_eq_of_eq_add _ _
definition eq_add_of_sub_eq : Π{a b c : }, a - c = b → a = b + c := @algebra.eq_add_of_sub_eq _ _
definition add_eq_of_eq_sub : Π{a b c : }, a = c - b → a + b = c := @algebra.add_eq_of_eq_sub _ _
definition sub_add_eq_sub_sub : Πa b c : , a - (b + c) = a - b - c := algebra.sub_add_eq_sub_sub
definition neg_add_eq_sub : Πa b : , -a + b = b - a := algebra.neg_add_eq_sub
definition neg_add : Πa b : , -(a + b) = -a + -b := algebra.neg_add
definition sub_add_eq_add_sub : Πa b c : , a - b + c = a + c - b := algebra.sub_add_eq_add_sub
definition sub_sub_ : Πa b c : , a - b - c = a - (b + c) := algebra.sub_sub
definition add_sub_add_left_eq_sub : Πa b c : , (c + a) - (c + b) = a - b :=
algebra.add_sub_add_left_eq_sub
definition eq_sub_of_add_eq' : Π{a b c : }, c + a = b → a = b - c := @algebra.eq_sub_of_add_eq' _ _
definition sub_eq_of_eq_add' : Π{a b c : }, a = b + c → a - b = c := @algebra.sub_eq_of_eq_add' _ _
definition eq_add_of_sub_eq' : Π{a b c : }, a - b = c → a = b + c := @algebra.eq_add_of_sub_eq' _ _
definition add_eq_of_eq_sub' : Π{a b c : }, b = c - a → a + b = c := @algebra.add_eq_of_eq_sub' _ _
definition ne_zero_of_mul_ne_zero_right : Π{a b : }, a * b ≠ 0 → a ≠ 0 :=
@algebra.ne_zero_of_mul_ne_zero_right _ _
definition ne_zero_of_mul_ne_zero_left : Π{a b : }, a * b ≠ 0 → b ≠ 0 :=
@algebra.ne_zero_of_mul_ne_zero_left _ _
definition dvd (a b : ) : Type₀ := algebra.dvd a b
notation a b := dvd a b
definition dvd.intro : Π{a b c : } (H : a * c = b), a b := @algebra.dvd.intro _ _
definition dvd.intro_left : Π{a b c : } (H : c * a = b), a b := @algebra.dvd.intro_left _ _
definition exists_eq_mul_right_of_dvd : Π{a b : } (H : a b), Σc, b = a * c :=
@algebra.exists_eq_mul_right_of_dvd _ _
definition dvd.elim : Π{P : Type} {a b : } (H₁ : a b) (H₂ : Πc, b = a * c → P), P :=
@algebra.dvd.elim _ _
definition exists_eq_mul_left_of_dvd : Π{a b : } (H : a b), Σc, b = c * a :=
@algebra.exists_eq_mul_left_of_dvd _ _
definition dvd.elim_left : Π{P : Type} {a b : } (H₁ : a b) (H₂ : Πc, b = c * a → P), P :=
@algebra.dvd.elim_left _ _
definition dvd.refl : Πa : , (a a) := algebra.dvd.refl
definition dvd.trans : Π{a b c : } (H₁ : a b) (H₂ : b c), a c := @algebra.dvd.trans _ _
definition eq_zero_of_zero_dvd : Π{a : } (H : 0 a), a = 0 := @algebra.eq_zero_of_zero_dvd _ _
definition dvd_zero : Πa : , a 0 := algebra.dvd_zero
definition one_dvd : Πa : , 1 a := algebra.one_dvd
definition dvd_mul_right : Πa b : , a a * b := algebra.dvd_mul_right
definition dvd_mul_left : Πa b : , a b * a := algebra.dvd_mul_left
definition dvd_mul_of_dvd_left : Π{a b : } (H : a b) (c : ), a b * c :=
@algebra.dvd_mul_of_dvd_left _ _
definition dvd_mul_of_dvd_right : Π{a b : } (H : a b) (c : ), a c * b :=
@algebra.dvd_mul_of_dvd_right _ _
definition mul_dvd_mul : Π{a b c d : }, a b → c d → a * c b * d :=
@algebra.mul_dvd_mul _ _
definition dvd_of_mul_right_dvd : Π{a b c : }, a * b c → a c :=
@algebra.dvd_of_mul_right_dvd _ _
definition dvd_of_mul_left_dvd : Π{a b c : }, a * b c → b c :=
@algebra.dvd_of_mul_left_dvd _ _
definition dvd_add : Π{a b c : }, a b → a c → a b + c := @algebra.dvd_add _ _
definition zero_mul : Πa : , 0 * a = 0 := algebra.zero_mul
definition mul_zero : Πa : , a * 0 = 0 := algebra.mul_zero
definition neg_mul_eq_neg_mul : Πa b : , -(a * b) = -a * b := algebra.neg_mul_eq_neg_mul
definition neg_mul_eq_mul_neg : Πa b : , -(a * b) = a * -b := algebra.neg_mul_eq_mul_neg
definition neg_mul_neg : Πa b : , -a * -b = a * b := algebra.neg_mul_neg
definition neg_mul_comm : Πa b : , -a * b = a * -b := algebra.neg_mul_comm
definition neg_eq_neg_one_mul : Πa : , -a = -1 * a := algebra.neg_eq_neg_one_mul
definition mul_sub_left_distrib : Πa b c : , a * (b - c) = a * b - a * c :=
algebra.mul_sub_left_distrib
definition mul_sub_right_distrib : Πa b c : , (a - b) * c = a * c - b * c :=
algebra.mul_sub_right_distrib
definition mul_add_eq_mul_add_iff_sub_mul_add_eq :
Πa b c d e : , a * e + c = b * e + d ↔ (a - b) * e + c = d :=
algebra.mul_add_eq_mul_add_iff_sub_mul_add_eq
definition mul_self_sub_mul_self_eq : Πa b : , a * a - b * b = (a + b) * (a - b) :=
algebra.mul_self_sub_mul_self_eq
definition mul_self_sub_one_eq : Πa : , a * a - 1 = (a + 1) * (a - 1) :=
algebra.mul_self_sub_one_eq
definition dvd_neg_iff_dvd : Πa b : , a -b ↔ a b := algebra.dvd_neg_iff_dvd
definition neg_dvd_iff_dvd : Πa b : , -a b ↔ a b := algebra.neg_dvd_iff_dvd
definition dvd_sub : Πa b c : , a b → a c → a b - c := algebra.dvd_sub
definition mul_ne_zero : Π{a b : }, a ≠ 0 → b ≠ 0 → a * b ≠ 0 := @algebra.mul_ne_zero _ _
definition mul.cancel_right : Π{a b c : }, a ≠ 0 → b * a = c * a → b = c :=
@algebra.mul.cancel_right _ _
definition mul.cancel_left : Π{a b c : }, a ≠ 0 → a * b = a * c → b = c :=
@algebra.mul.cancel_left _ _
definition mul_self_eq_mul_self_iff : Πa b : , a * a = b * b ↔ a = b ⊎ a = -b :=
algebra.mul_self_eq_mul_self_iff
definition mul_self_eq_one_iff : Πa : , a * a = 1 ↔ a = 1 ⊎ a = -1 :=
algebra.mul_self_eq_one_iff
definition dvd_of_mul_dvd_mul_left : Π{a b c : }, a ≠ 0 → a*b a*c → b c :=
@algebra.dvd_of_mul_dvd_mul_left _ _
definition dvd_of_mul_dvd_mul_right : Π{a b c : }, a ≠ 0 → b*a c*a → b c :=
@algebra.dvd_of_mul_dvd_mul_right _ _
end port_algebra
/- additional properties -/
definition of_nat_sub_of_nat {m n : } (H : #nat m ≥ n) : of_nat m - of_nat n = of_nat (#nat m - n) :=
have H1 : m = (#nat m - n + n), from (nat.sub_add_cancel H)⁻¹,
have H2 : m = (#nat m - n) + n, from ap of_nat H1,
sub_eq_of_eq_add H2
definition neg_succ_of_nat_eq' (m : ) : -[m +1] = -m - 1 :=
by rewrite [neg_succ_of_nat_eq, -of_nat_add_of_nat, neg_add]
end int

View file

@ -3,13 +3,13 @@ Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.nat.basic
(Ported from standard library file data.nat.basic on May 02, 2015)
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
Basic operations on the natural numbers.
-/
import algebra.binary
open eq sum sigma prod binary
import algebra.ring
open core prod binary
namespace nat
@ -19,7 +19,7 @@ definition addl (x y : ) : :=
nat.rec y (λ n r, succ r) x
infix `⊕`:65 := addl
theorem addl_succ_right (n m : ) : n ⊕ succ m = succ (n ⊕ m) :=
definition addl_succ_right (n m : ) : n ⊕ succ m = succ (n ⊕ m) :=
nat.rec_on n
rfl
(λ n₁ ih, calc
@ -27,7 +27,7 @@ nat.rec_on n
... = succ (succ (n₁ ⊕ m)) : ih
... = succ (succ n₁ ⊕ m) : rfl)
theorem add_eq_addl (x : ) : ∀y, x + y = x ⊕ y :=
definition add_eq_addl (x : ) : ∀y, x + y = x ⊕ y :=
nat.rec_on x
(λ y, nat.rec_on y
rfl
@ -47,52 +47,52 @@ nat.rec_on x
/- successor and predecessor -/
theorem succ_ne_zero (n : ) : succ n ≠ 0 :=
definition succ_ne_zero (n : ) : succ n ≠ 0 :=
by contradiction
-- add_rewrite succ_ne_zero
theorem pred_zero : pred 0 = 0 :=
definition pred_zero : pred 0 = 0 :=
rfl
theorem pred_succ (n : ) : pred (succ n) = n :=
definition pred_succ (n : ) : pred (succ n) = n :=
rfl
theorem eq_zero_or_eq_succ_pred (n : ) : n = 0 ⊎ n = succ (pred n) :=
definition eq_zero_or_eq_succ_pred (n : ) : n = 0 ⊎ n = succ (pred n) :=
nat.rec_on n
(sum.inl rfl)
(take m IH, sum.inr
(show succ m = succ (pred (succ m)), from ap succ !pred_succ⁻¹))
theorem exists_eq_succ_of_ne_zero {n : } (H : n ≠ 0) : Σk : , n = succ k :=
⟨_, sum.rec_on (eq_zero_or_eq_succ_pred n) (λH2, absurd H2 H) function.id⟩
definition exists_eq_succ_of_ne_zero {n : } (H : n ≠ 0) : Σk : , n = succ k :=
sigma.mk _ (sum_resolve_right !eq_zero_or_eq_succ_pred H)
theorem succ_inj {n m : } (H : succ n = succ m) : n = m :=
definition succ_inj {n m : } (H : succ n = succ m) : n = m :=
lift.down (nat.no_confusion H (λe, e))
theorem succ_ne_self {n : } : succ n ≠ n :=
definition succ_ne_self {n : } : succ n ≠ n :=
nat.rec_on n
(take H : 1 = 0,
have ne : 1 ≠ 0, from !succ_ne_zero,
absurd H ne)
(take k IH H, IH (succ_inj H))
theorem discriminate {B : Type} {n : } (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
definition discriminate {B : Type} {n : } (H1: n = 0 → B) (H2 : ∀m, n = succ m → B) : B :=
have H : n = n → B, from nat.cases_on n H1 H2,
H rfl
theorem two_step_induction_on {P : → Type} (a : ) (H1 : P 0) (H2 : P 1)
definition two_step_induction_on {P : → Type} (a : ) (H1 : P 0) (H2 : P 1)
(H3 : ∀ (n : ) (IH1 : P n) (IH2 : P (succ n)), P (succ (succ n))) : P a :=
have stronger : P a × P (succ a), from
nat.rec_on a
(H1, H2)
(pair H1 H2)
(take k IH,
have IH1 : P k, from pr1 IH,
have IH2 : P (succ k), from pr2 IH,
(IH2, (H3 k IH1 IH2))),
pair IH2 (H3 k IH1 IH2)),
pr1 stronger
theorem sub_induction {P : → Type} (n m : ) (H1 : ∀m, P 0 m)
definition sub_induction {P : → Type} (n m : ) (H1 : ∀m, P 0 m)
(H2 : ∀n, P (succ n) 0) (H3 : ∀n m, P n m → P (succ n) (succ m)) : P n m :=
have general : ∀m, P n m, from nat.rec_on n
(take m : , H1 m)
@ -104,13 +104,13 @@ general m
/- addition -/
theorem add_zero (n : ) : n + 0 = n :=
definition add_zero (n : ) : n + 0 = n :=
rfl
theorem add_succ (n m : ) : n + succ m = succ (n + m) :=
definition add_succ (n m : ) : n + succ m = succ (n + m) :=
rfl
theorem zero_add (n : ) : 0 + n = n :=
definition zero_add (n : ) : 0 + n = n :=
nat.rec_on n
!add_zero
(take m IH, show 0 + succ m = succ m, from
@ -118,7 +118,7 @@ nat.rec_on n
0 + succ m = succ (0 + m) : add_succ
... = succ m : IH)
theorem succ_add (n m : ) : (succ n) + m = succ (n + m) :=
definition succ_add (n m : ) : (succ n) + m = succ (n + m) :=
nat.rec_on m
(!add_zero ▸ !add_zero)
(take k IH, calc
@ -126,7 +126,7 @@ nat.rec_on m
... = succ (succ (n + k)) : IH
... = succ (n + succ k) : add_succ)
theorem add.comm (n m : ) : n + m = m + n :=
definition add.comm (n m : ) : n + m = m + n :=
nat.rec_on m
(!add_zero ⬝ !zero_add⁻¹)
(take k IH, calc
@ -134,10 +134,10 @@ nat.rec_on m
... = succ (k + n) : IH
... = succ k + n : succ_add)
theorem succ_add_eq_succ_add (n m : ) : succ n + m = n + succ m :=
definition succ_add_eq_succ_add (n m : ) : succ n + m = n + succ m :=
!succ_add ⬝ !add_succ⁻¹
theorem add.assoc (n m k : ) : (n + m) + k = n + (m + k) :=
definition add.assoc (n m k : ) : (n + m) + k = n + (m + k) :=
nat.rec_on k
(!add_zero ▸ !add_zero)
(take l IH,
@ -147,13 +147,13 @@ nat.rec_on k
... = n + succ (m + l) : add_succ
... = n + (m + succ l) : add_succ)
theorem add.left_comm (n m k : ) : n + (m + k) = m + (n + k) :=
definition add.left_comm (n m k : ) : n + (m + k) = m + (n + k) :=
left_comm add.comm add.assoc n m k
theorem add.right_comm (n m k : ) : n + m + k = n + k + m :=
definition add.right_comm (n m k : ) : n + m + k = n + k + m :=
right_comm add.comm add.assoc n m k
theorem add.cancel_left {n m k : } : n + m = n + k → m = k :=
definition add.cancel_left {n m k : } : n + m = n + k → m = k :=
nat.rec_on n
(take H : 0 + m = 0 + k,
!zero_add⁻¹ ⬝ H ⬝ !zero_add)
@ -166,11 +166,11 @@ nat.rec_on n
have H3 : n + m = n + k, from succ_inj H2,
IH H3)
theorem add.cancel_right {n m k : } (H : n + m = k + m) : n = k :=
definition add.cancel_right {n m k : } (H : n + m = k + m) : n = k :=
have H2 : m + n = m + k, from !add.comm ⬝ H ⬝ !add.comm,
add.cancel_left H2
theorem eq_zero_of_add_eq_zero_right {n m : } : n + m = 0 → n = 0 :=
definition eq_zero_of_add_eq_zero_right {n m : } : n + m = 0 → n = 0 :=
nat.rec_on n
(take (H : 0 + m = 0), rfl)
(take k IH,
@ -181,34 +181,34 @@ nat.rec_on n
... = 0 : H)
!succ_ne_zero)
theorem eq_zero_of_add_eq_zero_left {n m : } (H : n + m = 0) : m = 0 :=
definition eq_zero_of_add_eq_zero_left {n m : } (H : n + m = 0) : m = 0 :=
eq_zero_of_add_eq_zero_right (!add.comm ⬝ H)
theorem eq_zero_and_eq_zero_of_add_eq_zero {n m : } (H : n + m = 0) : n = 0 × m = 0 :=
(eq_zero_of_add_eq_zero_right H, eq_zero_of_add_eq_zero_left H)
definition eq_zero_and_eq_zero_of_add_eq_zero {n m : } (H : n + m = 0) : n = 0 × m = 0 :=
pair (eq_zero_of_add_eq_zero_right H) (eq_zero_of_add_eq_zero_left H)
theorem add_one (n : ) : n + 1 = succ n :=
definition add_one (n : ) : n + 1 = succ n :=
!add_zero ▸ !add_succ
theorem one_add (n : ) : 1 + n = succ n :=
definition one_add (n : ) : 1 + n = succ n :=
!zero_add ▸ !succ_add
/- multiplication -/
theorem mul_zero (n : ) : n * 0 = 0 :=
definition mul_zero (n : ) : n * 0 = 0 :=
rfl
theorem mul_succ (n m : ) : n * succ m = n * m + n :=
definition mul_succ (n m : ) : n * succ m = n * m + n :=
rfl
-- commutativity, distributivity, associativity, identity
theorem zero_mul (n : ) : 0 * n = 0 :=
definition zero_mul (n : ) : 0 * n = 0 :=
nat.rec_on n
!mul_zero
(take m IH, !mul_succ ⬝ !add_zero ⬝ IH)
theorem succ_mul (n m : ) : (succ n) * m = (n * m) + m :=
definition succ_mul (n m : ) : (succ n) * m = (n * m) + m :=
nat.rec_on m
(!mul_zero ⬝ !mul_zero⁻¹ ⬝ !add_zero⁻¹)
(take k IH, calc
@ -220,7 +220,7 @@ nat.rec_on m
... = n * k + n + succ k : add.assoc
... = n * succ k + succ k : mul_succ)
theorem mul.comm (n m : ) : n * m = m * n :=
definition mul.comm (n m : ) : n * m = m * n :=
nat.rec_on m
(!mul_zero ⬝ !zero_mul⁻¹)
(take k IH, calc
@ -228,7 +228,7 @@ nat.rec_on m
... = k * n + n : IH
... = (succ k) * n : succ_mul)
theorem mul.right_distrib (n m k : ) : (n + m) * k = n * k + m * k :=
definition mul.right_distrib (n m k : ) : (n + m) * k = n * k + m * k :=
nat.rec_on k
(calc
(n + m) * 0 = 0 : mul_zero
@ -244,14 +244,14 @@ nat.rec_on k
... = n * succ l + (m * l + m) : mul_succ
... = n * succ l + m * succ l : mul_succ)
theorem mul.left_distrib (n m k : ) : n * (m + k) = n * m + n * k :=
definition mul.left_distrib (n m k : ) : n * (m + k) = n * m + n * k :=
calc
n * (m + k) = (m + k) * n : mul.comm
... = m * n + k * n : mul.right_distrib
... = n * m + k * n : mul.comm
... = n * m + n * k : mul.comm
theorem mul.assoc (n m k : ) : (n * m) * k = n * (m * k) :=
definition mul.assoc (n m k : ) : (n * m) * k = n * (m * k) :=
nat.rec_on k
(calc
(n * m) * 0 = n * (m * 0) : mul_zero)
@ -262,18 +262,18 @@ nat.rec_on k
... = n * (m * l + m) : mul.left_distrib
... = n * (m * succ l) : mul_succ)
theorem mul_one (n : ) : n * 1 = n :=
definition mul_one (n : ) : n * 1 = n :=
calc
n * 1 = n * 0 + n : mul_succ
... = 0 + n : mul_zero
... = n : zero_add
theorem one_mul (n : ) : 1 * n = n :=
definition one_mul (n : ) : 1 * n = n :=
calc
1 * n = n * 1 : mul.comm
... = n : mul_one
theorem eq_zero_or_eq_zero_of_mul_eq_zero {n m : } : n * m = 0 → n = 0 ⊎ m = 0 :=
definition eq_zero_or_eq_zero_of_mul_eq_zero {n m : } : n * m = 0 → n = 0 ⊎ m = 0 :=
nat.cases_on n
(assume H, sum.inl rfl)
(take n',
@ -288,4 +288,66 @@ nat.cases_on n
... = succ (succ n' * m' + n') : add_succ)⁻¹)
!succ_ne_zero))
section
open [classes] algebra
protected definition comm_semiring [instance] [reducible] : algebra.comm_semiring nat :=
⦃algebra.comm_semiring,
add := add,
add_assoc := add.assoc,
zero := zero,
zero_add := zero_add,
add_zero := add_zero,
add_comm := add.comm,
mul := mul,
mul_assoc := mul.assoc,
one := succ zero,
one_mul := one_mul,
mul_one := mul_one,
left_distrib := mul.left_distrib,
right_distrib := mul.right_distrib,
zero_mul := zero_mul,
mul_zero := mul_zero,
mul_comm := mul.comm,
is_hset_carrier := is_hset_of_decidable_eq⦄
end
section port_algebra
open [classes] algebra
definition mul.left_comm : ∀a b c : , a * (b * c) = b * (a * c) := algebra.mul.left_comm
definition mul.right_comm : ∀a b c : , (a * b) * c = (a * c) * b := algebra.mul.right_comm
definition dvd (a b : ) : Type₀ := algebra.dvd a b
notation a b := dvd a b
definition dvd.intro : ∀{a b c : } (H : a * c = b), a b := @algebra.dvd.intro _ _
definition dvd.intro_left : ∀{a b c : } (H : c * a = b), a b := @algebra.dvd.intro_left _ _
definition exists_eq_mul_right_of_dvd : ∀{a b : } (H : a b), Σc, b = a * c :=
@algebra.exists_eq_mul_right_of_dvd _ _
definition dvd.elim : ∀{P : Type} {a b : } (H₁ : a b) (H₂ : ∀c, b = a * c → P), P :=
@algebra.dvd.elim _ _
definition exists_eq_mul_left_of_dvd : ∀{a b : } (H : a b), Σc, b = c * a :=
@algebra.exists_eq_mul_left_of_dvd _ _
definition dvd.elim_left : ∀{P : Type} {a b : } (H₁ : a b) (H₂ : ∀c, b = c * a → P), P :=
@algebra.dvd.elim_left _ _
definition dvd.refl : ∀a : , a a := algebra.dvd.refl
definition dvd.trans : ∀{a b c : }, a b → b c → a c := @algebra.dvd.trans _ _
definition eq_zero_of_zero_dvd : ∀{a : }, 0 a → a = 0 := @algebra.eq_zero_of_zero_dvd _ _
definition dvd_zero : ∀a : , a 0 := algebra.dvd_zero
definition one_dvd : ∀a : , 1 a := algebra.one_dvd
definition dvd_mul_right : ∀a b : , a a * b := algebra.dvd_mul_right
definition dvd_mul_left : ∀a b : , a b * a := algebra.dvd_mul_left
definition dvd_mul_of_dvd_left : ∀{a b : } (H : a b) (c : ), a b * c :=
@algebra.dvd_mul_of_dvd_left _ _
definition dvd_mul_of_dvd_right : ∀{a b : } (H : a b) (c : ), a c * b :=
@algebra.dvd_mul_of_dvd_right _ _
definition mul_dvd_mul : ∀{a b c d : }, a b → c d → a * c b * d :=
@algebra.mul_dvd_mul _ _
definition dvd_of_mul_right_dvd : ∀{a b c : }, a * b c → a c :=
@algebra.dvd_of_mul_right_dvd _ _
definition dvd_of_mul_left_dvd : ∀{a b c : }, a * b c → b c :=
@algebra.dvd_of_mul_left_dvd _ _
definition dvd_add : ∀{a b c : }, a b → a c → a b + c := @algebra.dvd_add _ _
end port_algebra
end nat

View file

@ -0,0 +1,9 @@
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.nat.default
Authors: Floris van Doorn
-/
import .basic .order .sub

425
hott/types/nat/order.hlean Normal file
View file

@ -0,0 +1,425 @@
/-
Copyright (c) 2014 Floris van Doorn. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Module: types.nat.order
Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
The order relation on the natural numbers.
Ported from standard library
-/
import .basic algebra.ordered_ring
open core prod decidable
namespace nat
/- lt and le -/
definition le_of_lt_or_eq {m n : } (H : m < n ⊎ m = n) : m ≤ n :=
sum.rec_on H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
definition lt.by_cases {a b : } {P : Type}
(H1 : a < b → P) (H2 : a = b → P) (H3 : b < a → P) : P :=
sum.rec_on !lt.trichotomy
(assume H, H1 H)
(assume H, sum.rec_on H (assume H', H2 H') (assume H', H3 H'))
definition lt_or_eq_of_le {m n : } (H : m ≤ n) : m < n ⊎ m = n :=
lt.by_cases
(assume H1 : m < n, sum.inl H1)
(assume H1 : m = n, sum.inr H1)
(assume H1 : m > n, absurd (lt_of_le_of_lt H H1) !lt.irrefl)
definition le_iff_lt_or_eq (m n : ) : m ≤ n ↔ m < n ⊎ m = n :=
iff.intro lt_or_eq_of_le le_of_lt_or_eq
definition lt_of_le_and_ne {m n : } (H1 : m ≤ n) (H2 : m ≠ n) : m < n :=
sum.rec_on (lt_or_eq_of_le H1)
(take H3 : m < n, H3)
(take H3 : m = n, absurd H3 H2)
definition lt_iff_le_and_ne (m n : ) : m < n ↔ m ≤ n × m ≠ n :=
iff.intro
(take H, pair (le_of_lt H) (take H1, lt.irrefl _ (H1 ▸ H)))
(take H, lt_of_le_and_ne (pr1 H) (pr2 H))
definition le_add_right (n k : ) : n ≤ n + k :=
nat.rec_on k
(calc n ≤ n : le.refl n
... = n + zero : add_zero)
(λ k (ih : n ≤ n + k), calc
n ≤ succ (n + k) : le_succ_of_le ih
... = n + succ k : add_succ)
definition le_add_left (n m : ): n ≤ m + n :=
!add.comm ▸ !le_add_right
definition le.intro {n m k : } (h : n + k = m) : n ≤ m :=
h ▸ le_add_right n k
definition le.elim {n m : } (h : n ≤ m) : Σk, n + k = m :=
le.rec_on h
(sigma.mk 0 rfl)
(λ m (h : n < m), lt.rec_on h
(sigma.mk 1 rfl)
(λ b hlt (ih : Σ (k : ), n + k = b),
sigma.rec_on ih (λ(k : ) (h : n + k = b),
sigma.mk (succ k) (calc
n + succ k = succ (n + k) : add_succ
... = succ b : h))))
definition le.total {m n : } : m ≤ n ⊎ n ≤ m :=
lt.by_cases
(assume H : m < n, sum.inl (le_of_lt H))
(assume H : m = n, sum.inl (H ▸ !le.refl))
(assume H : m > n, sum.inr (le_of_lt H))
/- addition -/
definition add_le_add_left {n m : } (H : n ≤ m) (k : ) : k + n ≤ k + m :=
sigma.rec_on (le.elim H) (λ(l : ) (Hl : n + l = m),
le.intro
(calc
k + n + l = k + (n + l) : !add.assoc
... = k + m : {Hl}))
definition add_le_add_right {n m : } (H : n ≤ m) (k : ) : n + k ≤ m + k :=
!add.comm ▸ !add.comm ▸ add_le_add_left H k
definition le_of_add_le_add_left {k n m : } (H : k + n ≤ k + m) : n ≤ m :=
sigma.rec_on (le.elim H) (λ(l : ) (Hl : k + n + l = k + m),
le.intro (add.cancel_left
(calc
k + (n + l) = k + n + l : (!add.assoc)⁻¹
... = k + m : Hl)))
definition add_lt_add_left {n m : } (H : n < m) (k : ) : k + n < k + m :=
lt_of_succ_le (!add_succ ▸ add_le_add_left (succ_le_of_lt H) k)
definition add_lt_add_right {n m : } (H : n < m) (k : ) : n + k < m + k :=
!add.comm ▸ !add.comm ▸ add_lt_add_left H k
definition lt_add_of_pos_right {n k : } (H : k > 0) : n < n + k :=
!add_zero ▸ add_lt_add_left H n
/- multiplication -/
definition mul_le_mul_left {n m : } (H : n ≤ m) (k : ) : k * n ≤ k * m :=
sigma.rec_on (le.elim H) (λ(l : ) (Hl : n + l = m),
have H2 : k * n + k * l = k * m, by rewrite [-mul.left_distrib, Hl],
le.intro H2)
definition mul_le_mul_right {n m : } (H : n ≤ m) (k : ) : n * k ≤ m * k :=
!mul.comm ▸ !mul.comm ▸ (mul_le_mul_left H k)
definition mul_le_mul {n m k l : } (H1 : n ≤ k) (H2 : m ≤ l) : n * m ≤ k * l :=
le.trans (mul_le_mul_right H1 m) (mul_le_mul_left H2 k)
definition mul_lt_mul_of_pos_left {n m k : } (H : n < m) (Hk : k > 0) : k * n < k * m :=
have H2 : k * n < k * n + k, from lt_add_of_pos_right Hk,
have H3 : k * n + k ≤ k * m, from !mul_succ ▸ mul_le_mul_left (succ_le_of_lt H) k,
lt_of_lt_of_le H2 H3
definition mul_lt_mul_of_pos_right {n m k : } (H : n < m) (Hk : k > 0) : n * k < m * k :=
!mul.comm ▸ !mul.comm ▸ mul_lt_mul_of_pos_left H Hk
definition le.antisymm {n m : } (H1 : n ≤ m) (H2 : m ≤ n) : n = m :=
sigma.rec_on (le.elim H1) (λ(k : ) (Hk : n + k = m),
sigma.rec_on (le.elim H2) (λ(l : ) (Hl : m + l = n),
have L1 : k + l = 0, from
add.cancel_left
(calc
n + (k + l) = n + k + l : (!add.assoc)⁻¹
... = m + l : {Hk}
... = n : Hl
... = n + 0 : (!add_zero)⁻¹),
have L2 : k = 0, from eq_zero_of_add_eq_zero_right L1,
calc
n = n + 0 : (!add_zero)⁻¹
... = n + k : {L2⁻¹}
... = m : Hk))
definition zero_le (n : ) : 0 ≤ n :=
le.intro !zero_add
/- nat is an instance of a linearly ordered semiring -/
section
open [classes] algebra
protected definition linear_ordered_semiring [instance] [reducible] :
algebra.linear_ordered_semiring nat :=
⦃ algebra.linear_ordered_semiring, nat.comm_semiring,
add_left_cancel := @add.cancel_left,
add_right_cancel := @add.cancel_right,
lt := lt,
le := le,
le_refl := le.refl,
le_trans := @le.trans,
le_antisymm := @le.antisymm,
le_total := @le.total,
le_iff_lt_or_eq := @le_iff_lt_or_eq,
lt_iff_le_and_ne := lt_iff_le_and_ne,
add_le_add_left := @add_le_add_left,
le_of_add_le_add_left := @le_of_add_le_add_left,
zero_ne_one := ne.symm (succ_ne_zero zero),
mul_le_mul_of_nonneg_left := (take a b c H1 H2, mul_le_mul_left H1 c),
mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right H1 c),
mul_lt_mul_of_pos_left := @mul_lt_mul_of_pos_left,
mul_lt_mul_of_pos_right := @mul_lt_mul_of_pos_right ⦄
migrate from algebra with nat
replacing has_le.ge → ge, has_lt.gt → gt
hiding pos_of_mul_pos_left, pos_of_mul_pos_right, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right
end
section port_algebra
open [classes] algebra
definition add_pos_left : Π{a : }, 0 < a → Πb : , 0 < a + b :=
take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
definition add_pos_right : Π{a : }, 0 < a → Πb : , 0 < b + a :=
take a H b, !add.comm ▸ add_pos_left H b
definition add_eq_zero_iff_eq_zero_and_eq_zero : Π{a b : },
a + b = 0 ↔ a = 0 × b = 0 :=
take a b : ,
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
definition le_add_of_le_left : Π{a b c : }, b ≤ c → b ≤ a + c :=
take a b c H, @algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
definition le_add_of_le_right : Π{a b c : }, b ≤ c → b ≤ c + a :=
take a b c H, @algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
definition lt_add_of_lt_left : Π{b c : }, b < c → Πa, b < a + c :=
take b c H a, @algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
definition lt_add_of_lt_right : Π{b c : }, b < c → Πa, b < c + a :=
take b c H a, @algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
definition lt_of_mul_lt_mul_left : Π{a b c : }, c * a < c * b → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
definition lt_of_mul_lt_mul_right : Π{a b c : }, a * c < b * c → a < b :=
take a b c H, @algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
definition pos_of_mul_pos_left : Π{a b : }, 0 < a * b → 0 < b :=
take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
definition pos_of_mul_pos_right : Π{a b : }, 0 < a * b → 0 < a :=
take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le
end port_algebra
definition zero_le_one : 0 ≤ 1 := dec_trivial
definition zero_lt_one : 0 < 1 := dec_trivial
/- properties specific to nat -/
definition lt_intro {n m k : } (H : succ n + k = m) : n < m :=
lt_of_succ_le (le.intro H)
definition lt_elim {n m : } (H : n < m) : Σk, succ n + k = m :=
le.elim (succ_le_of_lt H)
definition lt_add_succ (n m : ) : n < n + succ m :=
lt_intro !succ_add_eq_succ_add
definition eq_zero_of_le_zero {n : } (H : n ≤ 0) : n = 0 :=
obtain (k : ) (Hk : n + k = 0), from le.elim H,
eq_zero_of_add_eq_zero_right Hk
/- succ and pred -/
definition lt_iff_succ_le (m n : nat) : m < n ↔ succ m ≤ n :=
iff.intro succ_le_of_lt lt_of_succ_le
definition not_succ_le_zero (n : ) : ¬ succ n ≤ 0 :=
(assume H : succ n ≤ 0,
have H2 : succ n = 0, from eq_zero_of_le_zero H,
absurd H2 !succ_ne_zero)
definition succ_le_succ {n m : } (H : n ≤ m) : succ n ≤ succ m :=
!add_one ▸ !add_one ▸ add_le_add_right H 1
definition le_of_succ_le_succ {n m : } (H : succ n ≤ succ m) : n ≤ m :=
le_of_add_le_add_right ((!add_one)⁻¹ ▸ (!add_one)⁻¹ ▸ H)
definition self_le_succ (n : ) : n ≤ succ n :=
le.intro !add_one
definition succ_le_or_eq_of_le {n m : } (H : n ≤ m) : succ n ≤ m ⊎ n = m :=
sum.rec_on (lt_or_eq_of_le H)
(assume H1 : n < m, sum.inl (succ_le_of_lt H1))
(assume H1 : n = m, sum.inr H1)
definition le_succ_of_pred_le {n m : } : pred n ≤ m → n ≤ succ m :=
nat.cases_on n
(assume H : pred 0 ≤ m, !zero_le)
(take n',
assume H : pred (succ n') ≤ m,
have H1 : n' ≤ m, from pred_succ n' ▸ H,
succ_le_succ H1)
definition pred_le_of_le_succ {n m : } : n ≤ succ m → pred n ≤ m :=
nat.cases_on n
(assume H, !pred_zero⁻¹ ▸ zero_le m)
(take n',
assume H : succ n' ≤ succ m,
have H1 : n' ≤ m, from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
definition succ_le_of_le_pred {n m : } : succ n ≤ m → n ≤ pred m :=
nat.cases_on m
(assume H, absurd H !not_succ_le_zero)
(take m',
assume H : succ n ≤ succ m',
have H1 : n ≤ m', from le_of_succ_le_succ H,
!pred_succ⁻¹ ▸ H1)
definition pred_le_pred_of_le {n m : } : n ≤ m → pred n ≤ pred m :=
nat.cases_on n
(assume H, pred_zero⁻¹ ▸ zero_le (pred m))
(take n',
assume H : succ n' ≤ m,
!pred_succ⁻¹ ▸ succ_le_of_le_pred H)
definition lt_of_pred_lt_pred {n m : } (H : pred n < pred m) : n < m :=
lt_of_not_le
(take H1 : m ≤ n,
not_lt_of_le (pred_le_pred_of_le H1) H)
definition le_or_eq_succ_of_le_succ {n m : } (H : n ≤ succ m) : n ≤ m ⊎ n = succ m :=
sum_of_sum_of_imp_left (succ_le_or_eq_of_le H)
(take H2 : succ n ≤ succ m, show n ≤ m, from le_of_succ_le_succ H2)
definition le_pred_self (n : ) : pred n ≤ n :=
nat.cases_on n
(pred_zero⁻¹ ▸ !le.refl)
(take k : , (!pred_succ)⁻¹ ▸ !self_le_succ)
definition succ_pos (n : ) : 0 < succ n :=
!zero_lt_succ
definition succ_pred_of_pos {n : } (H : n > 0) : succ (pred n) = n :=
(sum_resolve_right (eq_zero_or_eq_succ_pred n) (ne.symm (ne_of_lt H)))⁻¹
definition exists_eq_succ_of_lt {n m : } (H : n < m) : Σk, m = succ k :=
discriminate
(take (Hm : m = 0), absurd (Hm ▸ H) !not_lt_zero)
(take (l : ) (Hm : m = succ l), sigma.mk l Hm)
definition lt_succ_self (n : ) : n < succ n :=
lt.base n
definition le_of_lt_succ {n m : } (H : n < succ m) : n ≤ m :=
le_of_succ_le_succ (succ_le_of_lt H)
/- other forms of rec -/
protected definition strong_induction_on {P : nat → Type} (n : ) (H : Πn, (Πm, m < n → P m) → P n) :
P n :=
have H1 : Π {n m : nat}, m < n → P m, from
take n,
nat.rec_on n
(show Πm, m < 0 → P m, from take m H, absurd H !not_lt_zero)
(take n',
assume IH : Π {m : nat}, m < n' → P m,
have H2: P n', from H n' @IH,
show Πm, m < succ n' → P m, from
take m,
assume H3 : m < succ n',
sum.rec_on (lt_or_eq_of_le (le_of_lt_succ H3))
(assume H4: m < n', IH H4)
(assume H4: m = n', H4⁻¹ ▸ H2)),
H1 !lt_succ_self
protected definition case_strong_induction_on {P : nat → Type} (a : nat) (H0 : P 0)
(Hind : Π(n : nat), (Πm, m ≤ n → P m) → P (succ n)) : P a :=
strong_induction_on a (
take n,
show (Πm, m < n → P m) → P n, from
nat.cases_on n
(assume H : (Πm, m < 0 → P m), show P 0, from H0)
(take n,
assume H : (Πm, m < succ n → P m),
show P (succ n), from
Hind n (take m, assume H1 : m ≤ n, H _ (lt_succ_of_le H1))))
/- pos -/
definition by_cases_zero_pos {P : → Type} (y : ) (H0 : P 0) (H1 : Π {y : nat}, y > 0 → P y) : P y :=
nat.cases_on y H0 (take y, H1 !succ_pos)
definition eq_zero_or_pos (n : ) : n = 0 ⊎ n > 0 :=
sum_of_sum_of_imp_left
(sum.swap (lt_or_eq_of_le !zero_le))
(take H : 0 = n, H⁻¹)
definition pos_of_ne_zero {n : } (H : n ≠ 0) : n > 0 :=
sum.rec_on !eq_zero_or_pos (take H2 : n = 0, absurd H2 H) (take H2 : n > 0, H2)
definition ne_zero_of_pos {n : } (H : n > 0) : n ≠ 0 :=
ne.symm (ne_of_lt H)
definition exists_eq_succ_of_pos {n : } (H : n > 0) : Σl, n = succ l :=
exists_eq_succ_of_lt H
definition pos_of_dvd_of_pos {m n : } (H1 : m n) (H2 : n > 0) : m > 0 :=
pos_of_ne_zero
(assume H3 : m = 0,
have H4 : n = 0, from eq_zero_of_zero_dvd (H3 ▸ H1),
ne_of_lt H2 H4⁻¹)
/- multiplication -/
definition mul_lt_mul_of_le_of_lt {n m k l : } (Hk : k > 0) (H1 : n ≤ k) (H2 : m < l) :
n * m < k * l :=
lt_of_le_of_lt (mul_le_mul_right H1 m) (mul_lt_mul_of_pos_left H2 Hk)
definition mul_lt_mul_of_lt_of_le {n m k l : } (Hl : l > 0) (H1 : n < k) (H2 : m ≤ l) :
n * m < k * l :=
lt_of_le_of_lt (mul_le_mul_left H2 n) (mul_lt_mul_of_pos_right H1 Hl)
definition mul_lt_mul_of_le_of_le {n m k l : } (H1 : n < k) (H2 : m < l) : n * m < k * l :=
have H3 : n * m ≤ k * m, from mul_le_mul_right (le_of_lt H1) m,
have H4 : k * m < k * l, from mul_lt_mul_of_pos_left H2 (lt_of_le_of_lt !zero_le H1),
lt_of_le_of_lt H3 H4
definition eq_of_mul_eq_mul_left {m k n : } (Hn : n > 0) (H : n * m = n * k) : m = k :=
have H2 : n * m ≤ n * k, from H ▸ !le.refl,
have H3 : n * k ≤ n * m, from H ▸ !le.refl,
have H4 : m ≤ k, from le_of_mul_le_mul_left H2 Hn,
have H5 : k ≤ m, from le_of_mul_le_mul_left H3 Hn,
le.antisymm H4 H5
definition eq_of_mul_eq_mul_right {n m k : } (Hm : m > 0) (H : n * m = k * m) : n = k :=
eq_of_mul_eq_mul_left Hm (!mul.comm ▸ !mul.comm ▸ H)
definition eq_zero_or_eq_of_mul_eq_mul_left {n m k : } (H : n * m = n * k) : n = 0 ⊎ m = k :=
sum_of_sum_of_imp_right !eq_zero_or_pos
(assume Hn : n > 0, eq_of_mul_eq_mul_left Hn H)
definition eq_zero_or_eq_of_mul_eq_mul_right {n m k : } (H : n * m = k * m) : m = 0 ⊎ n = k :=
eq_zero_or_eq_of_mul_eq_mul_left (!mul.comm ▸ !mul.comm ▸ H)
definition eq_one_of_mul_eq_one_right {n m : } (H : n * m = 1) : n = 1 :=
have H2 : n * m > 0, from H⁻¹ ▸ !succ_pos,
have H3 : n > 0, from pos_of_mul_pos_right H2,
have H4 : m > 0, from pos_of_mul_pos_left H2,
sum.rec_on (le_or_gt n 1)
(assume H5 : n ≤ 1,
show n = 1, from le.antisymm H5 (succ_le_of_lt H3))
(assume H5 : n > 1,
have H6 : n * m ≥ 2 * 1, from mul_le_mul (succ_le_of_lt H5) (succ_le_of_lt H4),
have H7 : 1 ≥ 2, from !mul_one ▸ H ▸ H6,
absurd !lt_succ_self (not_lt_of_le H7))
definition eq_one_of_mul_eq_one_left {n m : } (H : n * m = 1) : m = 1 :=
eq_one_of_mul_eq_one_right (!mul.comm ▸ H)
definition eq_one_of_mul_eq_self_left {n m : } (Hpos : n > 0) (H : m * n = n) : m = 1 :=
eq_of_mul_eq_mul_right Hpos (H ⬝ !one_mul⁻¹)
definition eq_one_of_mul_eq_self_right {n m : } (Hpos : m > 0) (H : m * n = m) : n = 1 :=
eq_one_of_mul_eq_self_left Hpos (!mul.comm ▸ H)
definition eq_one_of_dvd_one {n : } (H : n 1) : n = 1 :=
dvd.elim H
(take m,
assume H1 : 1 = n * m,
eq_one_of_mul_eq_one_right H1⁻¹)
end nat

465
hott/types/nat/sub.hlean Normal file
View file

@ -0,0 +1,465 @@
/-
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
Module: data.nat.sub
Subtraction on the natural numbers, as well as min, max, and distance.
Ported from standard library
-/
import .order
open core
namespace nat
/- subtraction -/
definition sub_zero (n : ) : n - 0 = n :=
rfl
definition sub_succ (n m : ) : n - succ m = pred (n - m) :=
rfl
definition zero_sub (n : ) : 0 - n = 0 :=
nat.rec_on n !sub_zero
(take k : nat,
assume IH : 0 - k = 0,
calc
0 - succ k = pred (0 - k) : sub_succ
... = pred 0 : IH
... = 0 : pred_zero)
definition succ_sub_succ (n m : ) : succ n - succ m = n - m :=
succ_sub_succ_eq_sub n m
definition sub_self (n : ) : n - n = 0 :=
nat.rec_on n !sub_zero (take k IH, !succ_sub_succ ⬝ IH)
definition add_sub_add_right (n k m : ) : (n + k) - (m + k) = n - m :=
nat.rec_on k
(calc
(n + 0) - (m + 0) = n - (m + 0) : {!add_zero}
... = n - m : {!add_zero})
(take l : nat,
assume IH : (n + l) - (m + l) = n - m,
calc
(n + succ l) - (m + succ l) = succ (n + l) - (m + succ l) : {!add_succ}
... = succ (n + l) - succ (m + l) : {!add_succ}
... = (n + l) - (m + l) : !succ_sub_succ
... = n - m : IH)
definition add_sub_add_left (k n m : ) : (k + n) - (k + m) = n - m :=
!add.comm ▸ !add.comm ▸ !add_sub_add_right
definition add_sub_cancel (n m : ) : n + m - m = n :=
nat.rec_on m
(!add_zero⁻¹ ▸ !sub_zero)
(take k : ,
assume IH : n + k - k = n,
calc
n + succ k - succ k = succ (n + k) - succ k : add_succ
... = n + k - k : succ_sub_succ
... = n : IH)
definition add_sub_cancel_left (n m : ) : n + m - n = m :=
!add.comm ▸ !add_sub_cancel
definition sub_sub (n m k : ) : n - m - k = n - (m + k) :=
nat.rec_on k
(calc
n - m - 0 = n - m : sub_zero
... = n - (m + 0) : add_zero)
(take l : nat,
assume IH : n - m - l = n - (m + l),
calc
n - m - succ l = pred (n - m - l) : !sub_succ
... = pred (n - (m + l)) : IH
... = n - succ (m + l) : sub_succ
... = n - (m + succ l) : {!add_succ⁻¹})
definition succ_sub_sub_succ (n m k : ) : succ n - m - succ k = n - m - k :=
calc
succ n - m - succ k = succ n - (m + succ k) : sub_sub
... = succ n - succ (m + k) : add_succ
... = n - (m + k) : succ_sub_succ
... = n - m - k : sub_sub
definition sub_self_add (n m : ) : n - (n + m) = 0 :=
calc
n - (n + m) = n - n - m : sub_sub
... = 0 - m : sub_self
... = 0 : zero_sub
definition sub.right_comm (m n k : ) : m - n - k = m - k - n :=
calc
m - n - k = m - (n + k) : !sub_sub
... = m - (k + n) : {!add.comm}
... = m - k - n : !sub_sub⁻¹
definition sub_one (n : ) : n - 1 = pred n :=
rfl
definition succ_sub_one (n : ) : succ n - 1 = n :=
rfl
/- interaction with multiplication -/
definition mul_pred_left (n m : ) : pred n * m = n * m - m :=
nat.rec_on n
(calc
pred 0 * m = 0 * m : pred_zero
... = 0 : zero_mul
... = 0 - m : zero_sub
... = 0 * m - m : zero_mul)
(take k : nat,
assume IH : pred k * m = k * m - m,
calc
pred (succ k) * m = k * m : pred_succ
... = k * m + m - m : add_sub_cancel
... = succ k * m - m : succ_mul)
definition mul_pred_right (n m : ) : n * pred m = n * m - n :=
calc
n * pred m = pred m * n : mul.comm
... = m * n - n : mul_pred_left
... = n * m - n : mul.comm
definition mul_sub_right_distrib (n m k : ) : (n - m) * k = n * k - m * k :=
nat.rec_on m
(calc
(n - 0) * k = n * k : sub_zero
... = n * k - 0 : sub_zero
... = n * k - 0 * k : zero_mul)
(take l : nat,
assume IH : (n - l) * k = n * k - l * k,
calc
(n - succ l) * k = pred (n - l) * k : sub_succ
... = (n - l) * k - k : mul_pred_left
... = n * k - l * k - k : IH
... = n * k - (l * k + k) : sub_sub
... = n * k - (succ l * k) : succ_mul)
definition mul_sub_left_distrib (n m k : ) : n * (m - k) = n * m - n * k :=
calc
n * (m - k) = (m - k) * n : !mul.comm
... = m * n - k * n : !mul_sub_right_distrib
... = n * m - k * n : {!mul.comm}
... = n * m - n * k : {!mul.comm}
definition mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
by rewrite [mul_sub_left_distrib, *mul.right_distrib, mul.comm b a, add.comm (a*a) (a*b), add_sub_add_left]
definition succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
calc succ a * succ a = (a+1)*(a+1) : by rewrite [add_one]
... = a*a + a + a + 1 : by rewrite [mul.right_distrib, mul.left_distrib, one_mul, mul_one]
/- interaction with inequalities -/
definition succ_sub {m n : } : m ≥ n → succ m - n = succ (m - n) :=
sub_induction n m
(take k, assume H : 0 ≤ k, rfl)
(take k,
assume H : succ k ≤ 0,
absurd H !not_succ_le_zero)
(take k l,
assume IH : k ≤ l → succ l - k = succ (l - k),
take H : succ k ≤ succ l,
calc
succ (succ l) - succ k = succ l - k : succ_sub_succ
... = succ (l - k) : IH (le_of_succ_le_succ H)
... = succ (succ l - succ k) : succ_sub_succ)
definition sub_eq_zero_of_le {n m : } (H : n ≤ m) : n - m = 0 :=
obtain (k : ) (Hk : n + k = m), from le.elim H, Hk ▸ !sub_self_add
definition add_sub_of_le {n m : } : n ≤ m → n + (m - n) = m :=
sub_induction n m
(take k,
assume H : 0 ≤ k,
calc
0 + (k - 0) = k - 0 : zero_add
... = k : sub_zero)
(take k, assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
(take k l,
assume IH : k ≤ l → k + (l - k) = l,
take H : succ k ≤ succ l,
calc
succ k + (succ l - succ k) = succ k + (l - k) : succ_sub_succ
... = succ (k + (l - k)) : succ_add
... = succ l : IH (le_of_succ_le_succ H))
definition add_sub_of_ge {n m : } (H : n ≥ m) : n + (m - n) = n :=
calc
n + (m - n) = n + 0 : sub_eq_zero_of_le H
... = n : add_zero
definition sub_add_cancel {n m : } : n ≥ m → n - m + m = n :=
!add.comm ▸ !add_sub_of_le
definition sub_add_of_le {n m : } : n ≤ m → n - m + m = m :=
!add.comm ▸ add_sub_of_ge
definition sub.cases {P : → Type} {n m : } (H1 : n ≤ m → P 0) (H2 : Πk, m + k = n -> P k)
: P (n - m) :=
sum.rec_on !le.total
(assume H3 : n ≤ m, (sub_eq_zero_of_le H3)⁻¹ ▸ (H1 H3))
(assume H3 : m ≤ n, H2 (n - m) (add_sub_of_le H3))
definition exists_sub_eq_of_le {n m : } (H : n ≤ m) : Σk, m - k = n :=
obtain (k : ) (Hk : n + k = m), from le.elim H,
sigma.mk k
(calc
m - k = n + k - k : Hk
... = n : add_sub_cancel)
definition add_sub_assoc {m k : } (H : k ≤ m) (n : ) : n + m - k = n + (m - k) :=
have l1 : k ≤ m → n + m - k = n + (m - k), from
sub_induction k m
(take m : ,
assume H : 0 ≤ m,
calc
n + m - 0 = n + m : sub_zero
... = n + (m - 0) : sub_zero)
(take k : , assume H : succ k ≤ 0, absurd H !not_succ_le_zero)
(take k m,
assume IH : k ≤ m → n + m - k = n + (m - k),
take H : succ k ≤ succ m,
calc
n + succ m - succ k = succ (n + m) - succ k : add_succ
... = n + m - k : succ_sub_succ
... = n + (m - k) : IH (le_of_succ_le_succ H)
... = n + (succ m - succ k) : succ_sub_succ),
l1 H
definition le_of_sub_eq_zero {n m : } : n - m = 0 → n ≤ m :=
sub.cases
(assume H1 : n ≤ m, assume H2 : 0 = 0, H1)
(take k : ,
assume H1 : m + k = n,
assume H2 : k = 0,
have H3 : n = m, from !add_zero ▸ H2 ▸ H1⁻¹,
H3 ▸ !le.refl)
definition sub_sub.cases {P : → Type} {n m : } (H1 : Πk, n = m + k -> P k 0)
(H2 : Πk, m = n + k → P 0 k) : P (n - m) (m - n) :=
sum.rec_on !le.total
(assume H3 : n ≤ m,
(sub_eq_zero_of_le H3)⁻¹ ▸ (H2 (m - n) (add_sub_of_le H3)⁻¹))
(assume H3 : m ≤ n,
(sub_eq_zero_of_le H3)⁻¹ ▸ (H1 (n - m) (add_sub_of_le H3)⁻¹))
definition sub_eq_of_add_eq {n m k : } (H : n + m = k) : k - n = m :=
have H2 : k - n + n = m + n, from
calc
k - n + n = k : sub_add_cancel (le.intro H)
... = n + m : H⁻¹
... = m + n : !add.comm,
add.cancel_right H2
definition sub_le_sub_right {n m : } (H : n ≤ m) (k : ) : n - k ≤ m - k :=
obtain (l : ) (Hl : n + l = m), from le.elim H,
sum.rec_on !le.total
(assume H2 : n ≤ k, (sub_eq_zero_of_le H2)⁻¹ ▸ !zero_le)
(assume H2 : k ≤ n,
have H3 : n - k + l = m - k, from
calc
n - k + l = l + (n - k) : add.comm
... = l + n - k : add_sub_assoc H2 l
... = n + l - k : add.comm
... = m - k : Hl,
le.intro H3)
definition sub_le_sub_left {n m : } (H : n ≤ m) (k : ) : k - m ≤ k - n :=
obtain (l : ) (Hl : n + l = m), from le.elim H,
sub.cases
(assume H2 : k ≤ m, !zero_le)
(take m' : ,
assume Hm : m + m' = k,
have H3 : n ≤ k, from le.trans H (le.intro Hm),
have H4 : m' + l + n = k - n + n, from
calc
m' + l + n = n + (m' + l) : add.comm
... = n + (l + m') : add.comm
... = n + l + m' : add.assoc
... = m + m' : Hl
... = k : Hm
... = k - n + n : sub_add_cancel H3,
le.intro (add.cancel_right H4))
definition sub_pos_of_lt {m n : } (H : m < n) : n - m > 0 :=
have H1 : n = n - m + m, from (sub_add_cancel (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, from (zero_add m)⁻¹ ▸ H1 ▸ H,
!lt_of_add_lt_add_right H2
definition lt_of_sub_pos {m n : } (H : n - m > 0) : m < n :=
lt_of_not_le
(take H1 : m ≥ n,
have H2 : n - m = 0, from sub_eq_zero_of_le H1,
!lt.irrefl (H2 ▸ H))
definition lt_of_sub_lt_sub_right {n m k : } (H : n - k < m - k) : n < m :=
lt_of_not_le
(assume H1 : m ≤ n,
have H2 : m - k ≤ n - k, from sub_le_sub_right H1 _,
not_le_of_lt H H2)
definition lt_of_sub_lt_sub_left {n m k : } (H : n - m < n - k) : k < m :=
lt_of_not_le
(assume H1 : m ≤ k,
have H2 : n - k ≤ n - m, from sub_le_sub_left H1 _,
not_le_of_lt H H2)
definition sub_lt_sub_add_sub (n m k : ) : n - k ≤ (n - m) + (m - k) :=
sub.cases
(assume H : n ≤ m, !zero_add⁻¹ ▸ sub_le_sub_right H k)
(take mn : ,
assume Hmn : m + mn = n,
sub.cases
(assume H : m ≤ k,
have H2 : n - k ≤ n - m, from sub_le_sub_left H n,
have H3 : n - k ≤ mn, from sub_eq_of_add_eq Hmn ▸ H2,
show n - k ≤ mn + 0, from !add_zero⁻¹ ▸ H3)
(take km : ,
assume Hkm : k + km = m,
have H : k + (mn + km) = n, from
calc
k + (mn + km) = k + (km + mn): add.comm
... = k + km + mn : add.assoc
... = m + mn : Hkm
... = n : Hmn,
have H2 : n - k = mn + km, from sub_eq_of_add_eq H,
H2 ▸ !le.refl))
definition sub_lt_self {m n : } (H1 : m > 0) (H2 : n > 0) : m - n < m :=
calc
m - n = succ (pred m) - n : succ_pred_of_pos H1
... = succ (pred m) - succ (pred n) : succ_pred_of_pos H2
... = pred m - pred n : succ_sub_succ
... ≤ pred m : sub_le
... < succ (pred m) : lt_succ_self
... = m : succ_pred_of_pos H1
definition le_sub_of_add_le {m n k : } (H : m + k ≤ n) : m ≤ n - k :=
calc
m = m + k - k : add_sub_cancel
... ≤ n - k : sub_le_sub_right H k
definition lt_sub_of_add_lt {m n k : } (H : m + k < n) (H2 : k ≤ n) : m < n - k :=
lt_of_succ_le (le_sub_of_add_le (calc
succ m + k = succ (m + k) : succ_add_eq_succ_add
... ≤ n : succ_le_of_lt H))
/- distance -/
definition dist [reducible] (n m : ) := (n - m) + (m - n)
definition dist.comm (n m : ) : dist n m = dist m n :=
!add.comm
definition dist_self (n : ) : dist n n = 0 :=
calc
(n - n) + (n - n) = 0 + (n - n) : sub_self
... = 0 + 0 : sub_self
... = 0 : rfl
definition eq_of_dist_eq_zero {n m : } (H : dist n m = 0) : n = m :=
have H2 : n - m = 0, from eq_zero_of_add_eq_zero_right H,
have H3 : n ≤ m, from le_of_sub_eq_zero H2,
have H4 : m - n = 0, from eq_zero_of_add_eq_zero_left H,
have H5 : m ≤ n, from le_of_sub_eq_zero H4,
le.antisymm H3 H5
definition dist_eq_sub_of_le {n m : } (H : n ≤ m) : dist n m = m - n :=
calc
dist n m = 0 + (m - n) : {sub_eq_zero_of_le H}
... = m - n : zero_add
definition dist_eq_sub_of_ge {n m : } (H : n ≥ m) : dist n m = n - m :=
!dist.comm ▸ dist_eq_sub_of_le H
definition dist_zero_right (n : ) : dist n 0 = n :=
dist_eq_sub_of_ge !zero_le ⬝ !sub_zero
definition dist_zero_left (n : ) : dist 0 n = n :=
dist_eq_sub_of_le !zero_le ⬝ !sub_zero
definition dist.intro {n m k : } (H : n + m = k) : dist k n = m :=
calc
dist k n = k - n : dist_eq_sub_of_ge (le.intro H)
... = m : sub_eq_of_add_eq H
definition dist_add_add_right (n k m : ) : dist (n + k) (m + k) = dist n m :=
calc
dist (n + k) (m + k) = ((n+k) - (m+k)) + ((m+k)-(n+k)) : rfl
... = (n - m) + ((m + k) - (n + k)) : add_sub_add_right
... = (n - m) + (m - n) : add_sub_add_right
definition dist_add_add_left (k n m : ) : dist (k + n) (k + m) = dist n m :=
!add.comm ▸ !add.comm ▸ !dist_add_add_right
definition dist_add_eq_of_ge {n m : } (H : n ≥ m) : dist n m + m = n :=
calc
dist n m + m = n - m + m : {dist_eq_sub_of_ge H}
... = n : sub_add_cancel H
definition dist_eq_intro {n m k l : } (H : n + m = k + l) : dist n k = dist l m :=
calc
dist n k = dist (n + m) (k + m) : dist_add_add_right
... = dist (k + l) (k + m) : H
... = dist l m : dist_add_add_left
definition dist_sub_eq_dist_add_left {n m : } (H : n ≥ m) (k : ) :
dist (n - m) k = dist n (k + m) :=
have H2 : n - m + (k + m) = k + n, from
calc
n - m + (k + m) = n - m + (m + k) : add.comm
... = n - m + m + k : add.assoc
... = n + k : sub_add_cancel H
... = k + n : add.comm,
dist_eq_intro H2
definition dist_sub_eq_dist_add_right {k m : } (H : k ≥ m) (n : ) :
dist n (k - m) = dist (n + m) k :=
(dist_sub_eq_dist_add_left H n ▸ !dist.comm) ▸ !dist.comm
definition dist.triangle_inequality (n m k : ) : dist n k ≤ dist n m + dist m k :=
have H : (n - m) + (m - k) + ((k - m) + (m - n)) = (n - m) + (m - n) + ((m - k) + (k - m)),
by exact sorry,
H ▸ add_le_add !sub_lt_sub_add_sub !sub_lt_sub_add_sub
definition dist_add_add_le_add_dist_dist (n m k l : ) : dist (n + m) (k + l) ≤ dist n k + dist m l :=
have H : dist (n + m) (k + m) + dist (k + m) (k + l) = dist n k + dist m l, from
!dist_add_add_left ▸ !dist_add_add_right ▸ rfl,
H ▸ !dist.triangle_inequality
definition dist_mul_left (k n m : ) : dist (k * n) (k * m) = k * dist n m :=
have H : Πn m, dist n m = n - m + (m - n), from take n m, rfl,
by exact sorry
definition dist_mul_right (n k m : ) : dist (n * k) (m * k) = dist n m * k :=
have H : Πn m, dist n m = n - m + (m - n), from take n m, rfl,
by exact sorry
definition dist_mul_dist (n m k l : ) : dist n m * dist k l = dist (n * k + m * l) (n * l + m * k) :=
have aux : Πk l, k ≥ l → dist n m * dist k l = dist (n * k + m * l) (n * l + m * k), from
take k l : ,
assume H : k ≥ l,
have H2 : m * k ≥ m * l, from mul_le_mul_left H m,
have H3 : n * l + m * k ≥ m * l, from le.trans H2 !le_add_left,
calc
dist n m * dist k l = dist n m * (k - l) : dist_eq_sub_of_ge H
... = dist (n * (k - l)) (m * (k - l)) : dist_mul_right
... = dist (n * k - n * l) (m * k - m * l) : by exact sorry
... = dist (n * k) (m * k - m * l + n * l) : dist_sub_eq_dist_add_left (mul_le_mul_left H n)
... = dist (n * k) (n * l + (m * k - m * l)) : add.comm
... = dist (n * k) (n * l + m * k - m * l) : add_sub_assoc H2 (n * l)
... = dist (n * k + m * l) (n * l + m * k) : dist_sub_eq_dist_add_right H3 _,
sum.rec_on !le.total
(assume H : k ≤ l, !dist.comm ▸ !dist.comm ▸ aux l k H)
(assume H : l ≤ k, aux k l H)
end nat

View file

@ -152,7 +152,7 @@ int.cases_on a
protected definition equiv (p q : × ) : Prop := pr1 p + pr2 q = pr2 p + pr1 q
local notation p `≡` q := equiv p q
local infix `≡` := int.equiv
protected theorem equiv.refl [refl] {p : × } : p ≡ p := !add.comm

View file

@ -84,8 +84,7 @@ sub rename_in_file {
while (<>) {
foreach my $lkey (keys %literalrenamings2) {
# replace all instances of lkey
if (/$lkey/) {print STDOUT "renamed ", $lkey, "\n"; }
# else {print STDOUT "WARNING: didn't rename ", $lkey, " to ", $literalrenamings2{$lkey}, "\n";}
# if (/$lkey/) {print STDOUT "renamed ", $lkey, "\n"; }
s/$lkey/$literalrenamings2{$lkey}/g
}
foreach my $key (keys %renamings) {
@ -103,6 +102,7 @@ sub rename_in_file {
my $oldfile = shift;
my $newfile = shift;
if (-e $newfile) {move($newfile,$newfile.".orig") or die "Move failed: $!"; }
print "copying ", $oldfile, " to ",$newfile, ".\n";
copy($oldfile,$newfile) or die "Copy failed: $!";
get_renamings;

View file

@ -20,7 +20,8 @@
# have to be escaped
now=$(date +"%B %d, %Y")
./port.pl ../library/data/nat/basic.lean ../hott/types/nat/basic.hlean "Module: data.nat.basic" "Module: types.nat.basic
(Ported from standard library file data.nat.basic on $now)" "import logic.connectives data.num algebra.binary algebra.ring" "import algebra.binary" "open binary eq.ops" "open core prod binary" "nat.no_confusion H \(λe, e\)" "lift.down (nat.no_confusion H (λe, e))"
./port.pl ../library/data/nat/basic.lean ../hott/types/nat/basic2.hlean "Module: data.nat.basic" "Module: types.nat.basic
(Ported from standard library file data.nat.basic on $now)" "import logic.connectives data.num algebra.binary algebra.ring" "import algebra.ring" "open binary eq.ops" "open core prod binary" "nat.no_confusion H \(λe, e\)" "lift.down (nat.no_confusion H (λe, e))"
# ./port.pl ../library/logic/connectives.lean ../hott/logic.hlean
/port.pl ../library/algebra/ring.lean ../hott/algebra/ring.hlean "import logic.eq logic.connectives data.unit data.sigma data.prod" "import algebra.group" "import algebra.function algebra.binary algebra.group" "" "open eq eq.ops" "open core"

View file

@ -1,21 +1,44 @@
Prop:Type
theorem:definition
by simp;by exact sorry
true:unit
trivial:star
is_true:is_unit
false:empty
is_false:is_empty
induction:rec
induction_on:rec_on
;⊎
or.elim:sum.rec_on
or.inl:sum.inl
or.inr:sum.inr
or.intro_left _;sum.inl
or.intro_right _;sum.inr
or_resolve_right:sum_resolve_right
or_resolve_left:sum_resolve_left
or.swap:sum.swap
or.rec_on:sum.rec_on
or_of_or_of_imp_of_imp:sum_of_sum_of_imp_of_imp
or_of_or_of_imp_left:sum_of_sum_of_imp_left
or_of_or_of_imp_right:sum_of_sum_of_imp_right
∧;×
and.intro:pair
and.left:
and.elim_left:pr1
and.elim_right:pr2
and.elim_left:prod.pr1
and.left:prod.pr1
and.elim_right:prod.pr2
and.right:prod.pr2
∀;Π
∃;Σ
exists.intro:sigma.mk
exists.elim:sigma.rec_on
eq.symm:inverse
congr_arg:ap
or_resolve_right:sum_resolve_right
or_resolve_left:sum_resolve_left
true:unit
trivial:star
false:empty