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

refactor(library): remove algebra namespace

Browse source
This commit is contained in:
Leonardo de Moura 2015-12-05 23:27:46 -08:00
parent 61b3c7c655
commit b94e31a72c
81 changed files with 363 additions and 1131 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/algebra/bundled.lean
View file

@ -7,7 +7,6 @@ Bundled structures
-/
import algebra.group
namespace algebra
structure Semigroup :=
(carrier : Type) (struct : semigroup carrier)
@ -79,4 +78,3 @@ structure AddCommGroup :=
attribute AddCommGroup.carrier [coercion]
attribute AddCommGroup.struct [instance]
end algebra

2
library/algebra/complete_lattice.lean
View file

@ -10,7 +10,6 @@ TODO: define dual complete lattice and simplify proof of dual theorems.
import algebra.lattice data.set.basic
open set
namespace algebra
variable {A : Type}
structure complete_lattice [class] (A : Type) extends lattice A :=
@ -271,4 +270,3 @@ have le₂ : ⨅ univ ≤ ⨆ (∅ : set A), from
le.antisymm le₁ le₂
end complete_lattice
end algebra

8
library/algebra/field.lean
View file

@ -10,8 +10,6 @@ import logic.eq logic.connectives data.unit data.sigma data.prod
import algebra.binary algebra.group algebra.ring
open eq eq.ops
namespace algebra
variable {A : Type}
structure division_ring [class] (A : Type) extends ring A, has_inv A, zero_ne_one_class A :=
@ -22,7 +20,7 @@ section division_ring
variables [s : division_ring A] {a b c : A}
include s
protected definition div (a b : A) : A := a * b⁻¹
protected definition algebra.div (a b : A) : A := a * b⁻¹
definition division_ring_has_div [reducible] [instance] : has_div A :=
has_div.mk algebra.div
@ -469,11 +467,7 @@ section discrete_field
end discrete_field
end algebra
namespace norm_num
open algebra
variable {A : Type}
theorem div_add_helper [s : field A] (n d b c val : A) (Hd : d ≠ 0) (H : n + b * d = val)
(H2 : c * d = val) : n / d + b = c :=

16
library/algebra/group.lean
View file

@ -12,8 +12,6 @@ import algebra.binary algebra.priority
open eq eq.ops -- note: ⁻¹ will be overloaded
open binary
namespace algebra
variable {A : Type}
/- semigroup -/
@ -453,7 +451,7 @@ section add_group
/- sub -/
-- TODO: derive corresponding facts for div in a field
definition sub [reducible] (a b : A) : A := a + -b
protected definition algebra.sub [reducible] (a b : A) : A := a + -b
definition add_group_has_sub [reducible] [instance] : has_sub A :=
has_sub.mk algebra.sub
@ -579,12 +577,8 @@ definition group_of_add_group (A : Type) [G : add_group A] : group A :=
inv := has_neg.neg,
mul_left_inv := add.left_inv⦄
end algebra
namespace norm_num
open algebra
reveal add.assoc
variable {A : Type}
definition add1 [s : has_add A] [s' : has_one A] (a : A) : A := add a one
@ -691,14 +685,14 @@ theorem neg_zero_helper [s : add_group A] (a : A) (H : a = 0) : - a = 0 :=
end norm_num
attribute [simp]
algebra.zero_add algebra.add_zero algebra.one_mul algebra.mul_one
zero_add add_zero one_mul mul_one
at simplifier.unit
attribute [simp]
algebra.neg_neg algebra.sub_eq_add_neg
neg_neg sub_eq_add_neg
at simplifier.neg
attribute [simp]
algebra.add.assoc algebra.add.comm algebra.add.left_comm
algebra.mul.left_comm algebra.mul.comm algebra.mul.assoc
add.assoc add.comm add.left_comm
mul.left_comm mul.comm mul.assoc
at simplifier.ac

9
library/algebra/group_bigops.lean
View file

@ -12,9 +12,8 @@ Bigops based on finsets go in the namespace algebra.finset. There are also versi
defined in group_set_bigops.lean.
-/
import .group .group_power data.list.basic data.list.perm data.finset.basic
open algebra function binary quot subtype list finset
open function binary quot subtype list finset
namespace algebra
variables {A B : Type}
variable [deceqA : decidable_eq A]
@ -80,7 +79,7 @@ section monoid
open nat
lemma Prodl_eq_pow_of_const {f : A → B} :
∀ {l : list A} b, (∀ a, a ∈ l → f a = b) → Prodl l f = b ^ length l
| nil := take b, assume Pconst, by rewrite [length_nil, {b^0}algebra.pow_zero]
| nil := take b, assume Pconst, by rewrite [length_nil, {b^0}pow_zero]
| (a::l) := take b, assume Pconst,
assert Pconstl : ∀ a', a' ∈ l → f a' = b,
from take a' Pa'in, Pconst a' (mem_cons_of_mem a Pa'in),
@ -119,7 +118,7 @@ namespace finset
(λ l₁ l₂ p, Prodl_eq_Prodl_of_perm f p)
-- ∏ x ∈ s, f x
notation `∏` binders `∈` s, r:(scoped f, prod s f) := r
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → B) : Prod ∅ f = 1 :=
Prodl_nil f
@ -232,5 +231,3 @@ namespace finset
theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = (0:B) := Prod_one s
end finset
end algebra

3
library/algebra/group_power.lean
View file

@ -29,7 +29,6 @@ structure has_pow_int [class] (A : Type) :=
definition pow_int {A : Type} [s : has_pow_int A] : A → int → A :=
has_pow_int.pow_int
namespace algebra
/- monoid -/
section monoid
open nat
@ -262,5 +261,3 @@ theorem add_imul (i j : ℤ) (a : A) : imul (i + j) a = imul i a + imul j a :=
theorem imul_comm (i j : ℤ) (a : A) : imul i a + imul j a = imul j a + imul i a := gpow_comm a i j
end add_group
end algebra

6
library/algebra/group_set_bigops.lean
View file

@ -8,7 +8,6 @@ Set-based version of group_bigops.
import .group_bigops data.set.finite
open set classical
namespace algebra
namespace set
variables {A B : Type}
@ -19,7 +18,7 @@ section Prod
variable [cmB : comm_monoid B]
include cmB
noncomputable definition Prod (s : set A) (f : A → B) : B := algebra.finset.Prod (to_finset s) f
noncomputable definition Prod (s : set A) (f : A → B) : B := finset.Prod (to_finset s) f
-- ∏ x ∈ s, f x
notation `∏` binders `∈` s, r:(scoped f, prod s f) := r
@ -101,6 +100,3 @@ section Sum
end Sum
end set
end algebra

4
library/algebra/lattice.lean
View file

@ -5,8 +5,6 @@ Author: Jeremy Avigad
-/
import .order
namespace algebra
variable {A : Type}
/- lattices (we could split this to upper- and lower-semilattices, if needed) -/
@ -108,5 +106,3 @@ section
theorem sup_eq_right {a b : A} (H : a ≤ b) : a ⊔ b = b :=
eq.subst !sup.comm (sup_eq_left H)
end
end algebra

4
library/algebra/order.lean
View file

@ -8,8 +8,6 @@ Weak orders "≤", strict orders "<", and structures that include both.
import logic.eq logic.connectives algebra.binary algebra.priority
open eq eq.ops
namespace algebra
variable {A : Type}
/- weak orders -/
@ -431,5 +429,3 @@ section
(assume H : a ≤ b, by rewrite (max_eq_right H); apply H₂)
(assume H : a > b, by rewrite (max_eq_left_of_lt H); apply H₁)
end
end algebra

3
library/algebra/ordered_field.lean
View file

@ -6,8 +6,6 @@ Authors: Robert Lewis
import algebra.ordered_ring algebra.field
open eq eq.ops
namespace algebra
structure linear_ordered_field [class] (A : Type) extends linear_ordered_ring A, field A
section linear_ordered_field
@ -516,4 +514,3 @@ section discrete_linear_ordered_field
!eq_div_of_mul_eq this !eq_sign_mul_abs⁻¹)
end discrete_linear_ordered_field
end algebra

6
library/algebra/ordered_group.lean
View file

@ -10,8 +10,6 @@ import logic.eq data.unit data.sigma data.prod
import algebra.binary algebra.group algebra.order
open eq eq.ops -- note: ⁻¹ will be overloaded
namespace algebra
variable {A : Type}
/- partially ordered monoids, such as the natural numbers -/
@ -790,7 +788,7 @@ section
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
le_of_add_le_add_right H1
theorem abs_sub_le (a b c : A) : abs (a - c) ≤ abs (a - b) + abs (b - c) :=
calc
@ -823,5 +821,3 @@ section
end
end
end algebra

6
library/algebra/ordered_ring.lean
View file

@ -11,8 +11,6 @@ of "linear_ordered_comm_ring". This development is modeled after Isabelle's libr
import algebra.ordered_group algebra.ring
open eq eq.ops
namespace algebra
variable {A : Type}
private definition absurd_a_lt_a {B : Type} {a : A} [s : strict_order A] (H : a < a) : B :=
@ -714,11 +712,7 @@ end
/- TODO: Multiplication and one, starting with mult_right_le_one_le. -/
end algebra
namespace norm_num
open algebra
variable {A : Type}
theorem pos_bit0_helper [s : linear_ordered_semiring A] (a : A) (H : a > 0) : bit0 a > 0 :=
by rewrite ↑bit0; apply add_pos H H

4
library/algebra/priority.lean
View file

@ -3,6 +3,4 @@ Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
namespace algebra
protected definition prio := num.sub std.priority.default 100
end algebra
protected definition algebra.prio := num.sub std.priority.default 100

18
library/algebra/ring.lean
View file

@ -11,8 +11,6 @@ import logic.eq logic.connectives data.unit data.sigma data.prod
import algebra.binary algebra.group
open eq eq.ops
namespace algebra
variable {A : Type}
/- auxiliary classes -/
@ -75,7 +73,7 @@ section comm_semiring
variables [s : comm_semiring A] (a b c : A)
include s
protected definition dvd (a b : A) : Prop := ∃c, b = a * c
protected definition algebra.dvd (a b : A) : Prop := ∃c, b = a * c
definition comm_semiring_has_dvd [reducible] [instance] [priority algebra.prio] : has_dvd A :=
has_dvd.mk algebra.dvd
@ -195,8 +193,8 @@ section
rewrite [-left_distrib, add.right_inv, mul_zero]
end
theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul
theorem mul_neg_eq_neg_mul_symm : a * - b = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg
theorem neg_mul_eq_neg_mul_symm : - a * b = - (a * b) := eq.symm !neg_mul_eq_neg_mul
theorem mul_neg_eq_neg_mul_symm : a * - b = - (a * b) := eq.symm !neg_mul_eq_mul_neg
theorem neg_mul_neg : -a * -b = a * b :=
calc
@ -404,11 +402,7 @@ section
dvd.intro this)
end
end algebra
namespace norm_num
open algebra
variables {A : Type}
theorem mul_zero [s : mul_zero_class A] (a : A) : a * zero = zero :=
by rewrite [↑zero, mul_zero]
@ -491,13 +485,13 @@ theorem pos_mul_neg_helper [s : ring A] (a b c : A) (H : a * b = c) : a * (-b) =
end norm_num
attribute [simp]
algebra.zero_mul algebra.mul_zero
zero_mul mul_zero
at simplifier.unit
attribute [simp]
algebra.neg_mul_eq_neg_mul_symm algebra.mul_neg_eq_neg_mul_symm
neg_mul_eq_neg_mul_symm mul_neg_eq_neg_mul_symm
at simplifier.neg
attribute [simp]
algebra.left_distrib algebra.right_distrib
left_distrib right_distrib
at simplifier.distrib

4
library/algebra/ring_power.lean
View file

@ -10,8 +10,6 @@ Properties of the power operation in an ordered ring or field.
import .group_power .ordered_field
open nat
namespace algebra
variable {A : Type}
section semiring
@ -172,5 +170,3 @@ begin
end
end discrete_field
end algebra

1
library/data/bag.lean
View file

@ -8,7 +8,6 @@ Finite bags.
import data.nat data.list.perm algebra.binary
open nat quot list subtype binary function eq.ops
open [declarations] perm
open algebra
variable {A : Type}

1
library/data/bv.lean
View file

@ -11,7 +11,6 @@ import data.list
import data.tuple
namespace bv
open algebra
open bool
open eq.ops
open list

6
library/data/complex.lean
View file

@ -6,7 +6,7 @@ Authors: Jacob Gross, Jeremy Avigad
The complex numbers.
-/
import data.real
open real eq.ops algebra
open real eq.ops
record complex : Type :=
(re : ℝ) (im : ℝ)
@ -156,9 +156,9 @@ iff.intro eq_of_of_real_eq_of_real !congr_arg
/- make complex an instance of ring -/
protected definition comm_ring [reducible] : algebra.comm_ring complex :=
protected definition comm_ring [reducible] : comm_ring complex :=
begin
fapply algebra.comm_ring.mk,
fapply comm_ring.mk,
exact complex.add,
exact complex.add_assoc,
exact 0,

2
library/data/encodable.lean
View file

@ -8,7 +8,7 @@ Note that every encodable type is countable.
-/
import data.fintype data.list data.list.sort data.sum data.nat.div data.countable data.equiv
import data.finset
open option list nat function algebra
open option list nat function
structure encodable [class] (A : Type) :=
(encode : A → nat) (decode : nat → option A) (encodek : ∀ a, decode (encode a) = some a)

2
library/data/examples/vector.lean
View file

@ -7,7 +7,7 @@ This file demonstrates how to encode vectors using indexed inductive families.
In standard library we do not use this approach.
-/
import data.nat data.list data.fin
open nat prod fin algebra
open nat prod fin
inductive vector (A : Type) : nat → Type :=
| nil {} : vector A zero

5
library/data/fin.lean
View file

@ -7,7 +7,6 @@ Finite ordinal types.
-/
import data.list.basic data.finset.basic data.fintype.card algebra.group data.equiv
open eq.ops nat function list finset fintype
open algebra
structure fin (n : nat) := (val : nat) (is_lt : val < n)
@ -259,8 +258,6 @@ lemma madd_left_inv : ∀ i : fin (succ n), madd (minv i) i = fin.zero n
| (mk iv ilt) := eq_of_veq (by
rewrite [val_madd, ↑minv, ↑fin.zero, mod_add_mod, nat.sub_add_cancel (le_of_lt ilt), mod_self])
open algebra
definition madd_is_comm_group [instance] : add_comm_group (fin (succ n)) :=
add_comm_group.mk madd madd_assoc (fin.zero n) zero_madd madd_zero minv madd_left_inv madd_comm
@ -411,7 +408,7 @@ definition fin_sum_equiv (n m : nat) : (fin n + fin m) ≃ fin (n+m) :=
assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
take v, suppose v < m, calc
v + n < m + n : add_lt_add_of_lt_of_le this !le.refl
... = n + m : algebra.add.comm,
... = n + m : add.comm,
⦃ equiv,
to_fun := λ s : sum (fin n) (fin m),
match s with

39
library/data/finset/bigops.lean
View file

@ -19,8 +19,8 @@ variables {A B : Type} [deceqA : decidable_eq A] [deceqB : decidable_eq B]
section union
definition to_comm_monoid_Union (B : Type) [deceqB : decidable_eq B] :
algebra.comm_monoid (finset B) :=
⦃ algebra.comm_monoid,
comm_monoid (finset B) :=
⦃ comm_monoid,
mul := union,
mul_assoc := union.assoc,
one := empty,
@ -29,48 +29,47 @@ definition to_comm_monoid_Union (B : Type) [deceqB : decidable_eq B] :
mul_comm := union.comm
⦄
open [classes] algebra
local attribute finset.to_comm_monoid_Union [instance]
include deceqB
definition Unionl (l : list A) (f : A → finset B) : finset B := algebra.Prodl l f
definition Unionl (l : list A) (f : A → finset B) : finset B := Prodl l f
notation `⋃` binders `←` l, r:(scoped f, Unionl l f) := r
definition Union (s : finset A) (f : A → finset B) : finset B := algebra.finset.Prod s f
definition Union (s : finset A) (f : A → finset B) : finset B := finset.Prod s f
notation `⋃` binders `∈` s, r:(scoped f, finset.Union s f) := r
theorem Unionl_nil (f : A → finset B) : Unionl [] f = ∅ := algebra.Prodl_nil f
theorem Unionl_nil (f : A → finset B) : Unionl [] f = ∅ := Prodl_nil f
theorem Unionl_cons (f : A → finset B) (a : A) (l : list A) :
Unionl (a::l) f = f a ∪ Unionl l f := algebra.Prodl_cons f a l
Unionl (a::l) f = f a ∪ Unionl l f := Prodl_cons f a l
theorem Unionl_append (l₁ l₂ : list A) (f : A → finset B) :
Unionl (l₁++l₂) f = Unionl l₁ f ∪ Unionl l₂ f := algebra.Prodl_append l₁ l₂ f
Unionl (l₁++l₂) f = Unionl l₁ f ∪ Unionl l₂ f := Prodl_append l₁ l₂ f
theorem Unionl_mul (l : list A) (f g : A → finset B) :
Unionl l (λx, f x ∪ g x) = Unionl l f ∪ Unionl l g := algebra.Prodl_mul l f g
Unionl l (λx, f x ∪ g x) = Unionl l f ∪ Unionl l g := Prodl_mul l f g
section deceqA
include deceqA
theorem Unionl_insert_of_mem (f : A → finset B) {a : A} {l : list A} (H : a ∈ l) :
Unionl (list.insert a l) f = Unionl l f := algebra.Prodl_insert_of_mem f H
Unionl (list.insert a l) f = Unionl l f := Prodl_insert_of_mem f H
theorem Unionl_insert_of_not_mem (f : A → finset B) {a : A} {l : list A} (H : a ∉ l) :
Unionl (list.insert a l) f = f a ∪ Unionl l f := algebra.Prodl_insert_of_not_mem f H
Unionl (list.insert a l) f = f a ∪ Unionl l f := Prodl_insert_of_not_mem f H
theorem Unionl_union {l₁ l₂ : list A} (f : A → finset B) (d : list.disjoint l₁ l₂) :
Unionl (list.union l₁ l₂) f = Unionl l₁ f ∪ Unionl l₂ f := algebra.Prodl_union f d
theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = (∅ : finset B) := algebra.Prodl_one l
Unionl (list.union l₁ l₂) f = Unionl l₁ f ∪ Unionl l₂ f := Prodl_union f d
theorem Unionl_empty (l : list A) : Unionl l (λ x, ∅) = (∅ : finset B) := Prodl_one l
end deceqA
theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := algebra.finset.Prod_empty f
theorem Union_empty (f : A → finset B) : Union ∅ f = ∅ := finset.Prod_empty f
theorem Union_mul (s : finset A) (f g : A → finset B) :
Union s (λx, f x ∪ g x) = Union s f ∪ Union s g := algebra.finset.Prod_mul s f g
Union s (λx, f x ∪ g x) = Union s f ∪ Union s g := finset.Prod_mul s f g
section deceqA
include deceqA
theorem Union_insert_of_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∈ s) :
Union (insert a s) f = Union s f := algebra.finset.Prod_insert_of_mem f H
Union (insert a s) f = Union s f := finset.Prod_insert_of_mem f H
private theorem Union_insert_of_not_mem (f : A → finset B) {a : A} {s : finset A} (H : a ∉ s) :
Union (insert a s) f = f a ∪ Union s f := algebra.finset.Prod_insert_of_not_mem f H
Union (insert a s) f = f a ∪ Union s f := finset.Prod_insert_of_not_mem f H
theorem Union_union (f : A → finset B) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := algebra.finset.Prod_union f disj
Union (s₁ ∪ s₂) f = Union s₁ f ∪ Union s₂ f := finset.Prod_union f disj
theorem Union_ext {s : finset A} {f g : A → finset B} (H : ∀x, x ∈ s → f x = g x) :
Union s f = Union s g := algebra.finset.Prod_ext H
theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := algebra.finset.Prod_one s
Union s f = Union s g := finset.Prod_ext H
theorem Union_empty' (s : finset A) : Union s (λ x, ∅) = (∅ : finset B) := finset.Prod_one s
-- this will eventually be an instance of something more general
theorem inter_Union (s : finset B) (t : finset A) (f : A → finset B) :

5
library/data/finset/card.lean
View file

@ -5,9 +5,8 @@ Author: Jeremy Avigad
Cardinality calculations for finite sets.
-/
import .to_set .bigops data.set.function data.nat.power data.nat.bigops
open nat nat.finset eq.ops
open algebra
import .to_set .bigops data.set.function data.nat.power
open nat eq.ops
namespace finset

5
library/data/finset/equiv.lean
View file

@ -4,14 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import data.finset.card
open nat nat.finset decidable
open algebra
open nat decidable
namespace finset
variable {A : Type}
protected definition to_nat (s : finset nat) : nat :=
nat.finset.Sum s (λ n, 2^n)
finset.Sum s (λ n, 2^n)
open finset (to_nat)

9
library/data/finset/partition.lean
View file

@ -43,15 +43,15 @@ begin
intro Pxg1, rewrite [Pxg1, and.right Pg1, and.right Pg2],
intro Pe, exact absurd Pe Pne
end
open nat
theorem class_equation (f : @partition A _) :
card (partition.set f) = nat.finset.Sum (equiv_classes f) card :=
card (partition.set f) = finset.Sum (equiv_classes f) card :=
let s := (partition.set f), p := (partition.part f), img := image p s in
calc
card s = card (Union s p) : partition.complete f
... = card (Union img id) : image_eq_Union_index_image s p
... = card (Union (equiv_classes f) id) : rfl
... = nat.finset.Sum (equiv_classes f) card : card_Union_of_disjoint _ id (equiv_class_disjoint f)
... = finset.Sum (equiv_classes f) card : card_Union_of_disjoint _ id (equiv_class_disjoint f)
lemma equiv_class_refl {f : A → finset A} (Pequiv : is_partition f) : ∀ a, a ∈ f a :=
take a, by rewrite [Pequiv a a]
@ -113,9 +113,8 @@ begin rewrite [binary_union P at {1}], apply Union_union, exact binary_inter_emp
end
open nat nat.finset
open nat
section
open algebra algebra.finset
variables {B : Type} [acmB : add_comm_monoid B]
include acmB

1
library/data/fintype/function.lean
View file

@ -7,7 +7,6 @@ Author : Haitao Zhang
import data
open nat function eq.ops
open algebra
namespace list
-- this is in preparation for counting the number of finite functions

2
library/data/hf.lean
View file

@ -10,7 +10,7 @@ we implement this module using a bijection from (finset nat) to nat, and
this bijection is implemeted using the Ackermann coding.
-/
import data.nat data.finset.equiv data.list
open nat binary algebra
open nat binary
open - [notations] finset
definition hf := nat

23
library/data/int/basic.lean
View file

@ -30,7 +30,6 @@ import algebra.relation algebra.binary algebra.ordered_ring
open eq.ops
open prod relation nat
open decidable binary
open algebra
/- the type of integers -/
@ -386,12 +385,12 @@ show pr1 p + pr2 p + 0 = pr2 p + pr1 p + 0, from !nat.add_comm ▸ rfl
theorem padd_padd_pneg (p q : ℕ × ℕ) : padd (padd p q) (pneg q) ≡ p :=
calc pr1 p + pr1 q + pr2 q + pr2 p
= pr1 p + (pr1 q + pr2 q) + pr2 p : algebra.add.assoc
... = pr1 p + (pr1 q + pr2 q + pr2 p) : algebra.add.assoc
... = pr1 p + (pr2 q + pr1 q + pr2 p) : algebra.add.comm
... = pr1 p + (pr2 q + pr2 p + pr1 q) : algebra.add.right_comm
... = pr1 p + (pr2 p + pr2 q + pr1 q) : algebra.add.comm
... = pr2 p + pr2 q + pr1 q + pr1 p : algebra.add.comm
= pr1 p + (pr1 q + pr2 q) + pr2 p : add.assoc
... = pr1 p + (pr1 q + pr2 q + pr2 p) : add.assoc
... = pr1 p + (pr2 q + pr1 q + pr2 p) : add.comm
... = pr1 p + (pr2 q + pr2 p + pr1 q) : add.right_comm
... = pr1 p + (pr2 p + pr2 q + pr1 q) : add.comm
... = pr2 p + pr2 q + pr1 q + pr1 p : add.comm
protected theorem add_left_inv (a : ℤ) : -a + a = 0 :=
have H : repr (-a + a) ≡ repr 0, from
@ -482,7 +481,7 @@ show (_,_) = (_,_),
begin
congruence,
{ congruence, repeat rewrite mul.comm },
{ rewrite algebra.add.comm, congruence, repeat rewrite mul.comm }
{ rewrite add.comm, congruence, repeat rewrite mul.comm }
end
protected theorem mul_comm (a b : ℤ) : a * b = b * a :=
@ -496,7 +495,7 @@ private theorem pmul_assoc_prep {p1 p2 q1 q2 r1 r2 : ℕ} :
((p1*q1+p2*q2)*r1+(p1*q2+p2*q1)*r2, (p1*q1+p2*q2)*r2+(p1*q2+p2*q1)*r1) =
(p1*(q1*r1+q2*r2)+p2*(q1*r2+q2*r1), p1*(q1*r2+q2*r1)+p2*(q1*r1+q2*r2)) :=
begin
rewrite[+left_distrib,+right_distrib,*algebra.mul.assoc],
rewrite[+left_distrib,+right_distrib,*mul.assoc],
exact (congr_arg2 pair (!add.comm4 ⬝ (!congr_arg !nat.add_comm))
(!add.comm4 ⬝ (!congr_arg !nat.add_comm)))
end
@ -552,8 +551,8 @@ protected theorem eq_zero_or_eq_zero_of_mul_eq_zero {a b : ℤ} (H : a * b = 0)
or.imp eq_zero_of_nat_abs_eq_zero eq_zero_of_nat_abs_eq_zero
(eq_zero_or_eq_zero_of_mul_eq_zero (by rewrite [-nat_abs_mul, H]))
protected definition integral_domain [reducible] [trans_instance] : algebra.integral_domain int :=
⦃algebra.integral_domain,
protected definition integral_domain [reducible] [trans_instance] : integral_domain int :=
⦃integral_domain,
add := int.add,
add_assoc := int.add_assoc,
zero := 0,
@ -584,7 +583,7 @@ theorem of_nat_sub {m n : ℕ} (H : m ≥ n) : of_nat (m - n) = of_nat m - of_na
assert m - n + n = m, from nat.sub_add_cancel H,
begin
symmetry,
apply algebra.sub_eq_of_eq_add,
apply sub_eq_of_eq_add,
rewrite [-of_nat_add, this]
end

165
library/data/int/bigops.lean
View file

@ -1,165 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Finite products and sums on the integers.
-/
import data.int.order algebra.group_bigops algebra.group_set_bigops
open list
namespace int
open [classes] algebra
local attribute int.decidable_linear_ordered_comm_ring [instance]
variables {A : Type} [deceqA : decidable_eq A]
/- Prodl -/
definition Prodl (l : list A) (f : A → int) : int := algebra.Prodl l f
notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r
theorem Prodl_nil (f : A → int) : Prodl [] f = 1 := algebra.Prodl_nil f
theorem Prodl_cons (f : A → int) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f :=
algebra.Prodl_cons f a l
theorem Prodl_append (l₁ l₂ : list A) (f : A → int) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f :=
algebra.Prodl_append l₁ l₂ f
theorem Prodl_mul (l : list A) (f g : A → int) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
section deceqA
include deceqA
theorem Prodl_insert_of_mem (f : A → int) {a : A} {l : list A} (H : a ∈ l) :
Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H
theorem Prodl_insert_of_not_mem (f : A → int) {a : A} {l : list A} (H : a ∉ l) :
Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H
theorem Prodl_union {l₁ l₂ : list A} (f : A → int) (d : disjoint l₁ l₂) :
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l
end deceqA
/- Prod over finset -/
namespace finset
open finset
definition Prod (s : finset A) (f : A → int) : int := algebra.finset.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → int) : Prod ∅ f = 1 := algebra.finset.Prod_empty f
theorem Prod_mul (s : finset A) (f g : A → int) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.finset.Prod_mul s f g
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → int) {a : A} {s : finset A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → int) {a : A} {s : finset A} (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → int) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj
theorem Prod_ext {s : finset A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.finset.Prod_ext H
theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s
end deceqA
end finset
/- Prod over set -/
namespace set
open set
noncomputable definition Prod (s : set A) (f : A → int) : int := algebra.set.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → int) : Prod ∅ f = 1 := algebra.set.Prod_empty f
theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → int) : Prod s f = 1 :=
algebra.set.Prod_of_not_finite nfins f
theorem Prod_mul (s : set A) (f g : A → int) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.set.Prod_mul s f g
theorem Prod_insert_of_mem (f : A → int) {a : A} {s : set A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → int) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → int) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj
theorem Prod_ext {s : set A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.set.Prod_ext H
theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s
end set
/- Suml -/
definition Suml (l : list A) (f : A → int) : int := algebra.Suml l f
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
theorem Suml_nil (f : A → int) : Suml [] f = 0 := algebra.Suml_nil f
theorem Suml_cons (f : A → int) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
algebra.Suml_cons f a l
theorem Suml_append (l₁ l₂ : list A) (f : A → int) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
algebra.Suml_append l₁ l₂ f
theorem Suml_add (l : list A) (f g : A → int) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
section deceqA
include deceqA
theorem Suml_insert_of_mem (f : A → int) {a : A} {l : list A} (H : a ∈ l) :
Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H
theorem Suml_insert_of_not_mem (f : A → int) {a : A} {l : list A} (H : a ∉ l) :
Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H
theorem Suml_union {l₁ l₂ : list A} (f : A → int) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l
end deceqA
/- Sum over a finset -/
namespace finset
open finset
definition Sum (s : finset A) (f : A → int) : int := algebra.finset.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → int) : Sum ∅ f = 0 := algebra.finset.Sum_empty f
theorem Sum_add (s : finset A) (f g : A → int) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.finset.Sum_add s f g
section deceqA
include deceqA
theorem Sum_insert_of_mem (f : A → int) {a : A} {s : finset A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → int) {a : A} {s : finset A} (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → int) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj
theorem Sum_ext {s : finset A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.finset.Sum_ext H
theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s
end deceqA
end finset
/- Sum over a set -/
namespace set
open set
noncomputable definition Sum (s : set A) (f : A → int) : int := algebra.set.Sum s f
notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → int) : Sum ∅ f = 0 := algebra.set.Sum_empty f
theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → int) : Sum s f = 0 :=
algebra.set.Sum_of_not_finite nfins f
theorem Sum_add (s : set A) (f g : A → int) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.set.Sum_add s f g
theorem Sum_insert_of_mem (f : A → int) {a : A} {s : set A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → int) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → int) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj
theorem Sum_ext {s : set A} {f g : A → int} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.set.Sum_ext H
theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s
end set
end int

2
library/data/int/default.lean
View file

@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
-/
import .basic .order .div .power .gcd .bigops
import .basic .order .div .power .gcd

3
library/data/int/div.lean
View file

@ -10,7 +10,6 @@ Following SSReflect and the SMTlib standard, we define a % b so that 0 ≤ a % b
import data.int.order data.nat.div
open [coercions] [reduce_hints] nat
open [declarations] [classes] nat (succ)
open algebra
open eq.ops
namespace int
@ -162,7 +161,7 @@ or.elim (nat.lt_or_ge m (n * k))
have (-[1+m] + n * k) / k = -[1+m] / k + n, from calc
(-[1+m] + n * k) / k
= of_nat ((k * n - (m + 1)) / k) :
by rewrite [add.comm, neg_succ_of_nat_eq, of_nat_div, algebra.mul.comm k n,
by rewrite [add.comm, neg_succ_of_nat_eq, of_nat_div, mul.comm k n,
of_nat_sub H3]
... = of_nat (n - m / k - 1) :
nat.mul_sub_div_of_lt (!nat.mul_comm ▸ m_lt_nk)

1
library/data/int/gcd.lean
View file

@ -7,7 +7,6 @@ Definitions and properties of gcd, lcm, and coprime.
-/
import .div data.nat.gcd
open eq.ops
open algebra
namespace int

21
library/data/int/order.lean
View file

@ -8,7 +8,6 @@ and transfer the results.
-/
import .basic algebra.ordered_ring
open nat
open algebra
open decidable
open int eq.ops
@ -234,8 +233,8 @@ protected theorem lt_of_le_of_lt {a b c : ℤ} (Hab : a ≤ b) (Hbc : b < c) :
(assume Heq, int.not_le_of_gt (Heq⁻¹ ▸ Hbc) Hab))
protected definition linear_ordered_comm_ring [reducible] [trans_instance] :
algebra.linear_ordered_comm_ring int :=
⦃algebra.linear_ordered_comm_ring, int.integral_domain,
linear_ordered_comm_ring int :=
⦃linear_ordered_comm_ring, int.integral_domain,
le := int.le,
le_refl := int.le_refl,
le_trans := @int.le_trans,
@ -255,8 +254,8 @@ protected definition linear_ordered_comm_ring [reducible] [trans_instance] :
add_lt_add_left := @int.add_lt_add_left⦄
protected definition decidable_linear_ordered_comm_ring [reducible] [instance] :
algebra.decidable_linear_ordered_comm_ring int :=
⦃algebra.decidable_linear_ordered_comm_ring,
decidable_linear_ordered_comm_ring int :=
⦃decidable_linear_ordered_comm_ring,
int.linear_ordered_comm_ring,
decidable_lt := decidable_lt⦄
@ -315,13 +314,13 @@ have H1 : a + 1 ≤ b + 1, from add_one_le_of_lt H,
le_of_add_le_add_right H1
theorem sub_one_le_of_lt {a b : ℤ} (H : a ≤ b) : a - 1 < b :=
lt_of_add_one_le (begin rewrite algebra.sub_add_cancel, exact H end)
lt_of_add_one_le (begin rewrite sub_add_cancel, exact H end)
theorem lt_of_sub_one_le {a b : ℤ} (H : a - 1 < b) : a ≤ b :=
!sub_add_cancel ▸ add_one_le_of_lt H
theorem le_sub_one_of_lt {a b : ℤ} (H : a < b) : a ≤ b - 1 :=
le_of_lt_add_one begin rewrite algebra.sub_add_cancel, exact H end
le_of_lt_add_one begin rewrite sub_add_cancel, exact H end
theorem lt_of_le_sub_one {a b : ℤ} (H : a ≤ b - 1) : a < b :=
!sub_add_cancel ▸ (lt_add_one_of_le H)
@ -376,7 +375,7 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
end,
have H' : P (b + of_nat (nat_abs (elt - b))), begin
rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt (iff.mpr !sub_pos_iff_lt Heltb)),
add.comm, algebra.sub_add_cancel],
add.comm, sub_add_cancel],
apply Helt
end,
apply and.intro,
@ -387,13 +386,13 @@ theorem exists_least_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
let Hzb' := lt_of_not_ge Hzb,
let Hpos := iff.mpr !sub_pos_iff_lt Hzb',
have Hzbk : z = b + of_nat (nat_abs (z - b)),
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, algebra.sub_add_cancel],
by rewrite [of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos), int.add_comm, sub_add_cancel],
have Hk : nat_abs (z - b) < least (λ n, P (b + of_nat n)) (nat.succ (nat_abs (elt - b))), begin
let Hz' := iff.mp !lt_add_iff_sub_lt_left Hz,
rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
apply lt_of_of_nat_lt_of_nat Hz'
end,
let Hk' := algebra.not_le_of_gt Hk,
let Hk' := not_le_of_gt Hk,
rewrite Hzbk,
apply λ p, mt (ge_least_of_lt _ p) Hk',
apply nat.lt_trans Hk,
@ -431,7 +430,7 @@ theorem exists_greatest_of_bdd {P : ℤ → Prop} [HP : decidable_pred P]
rewrite [-of_nat_nat_abs_of_nonneg (int.le_of_lt Hpos) at Hz'],
apply lt_of_of_nat_lt_of_nat Hz'
end,
let Hk' := algebra.not_le_of_gt Hk,
let Hk' := not_le_of_gt Hk,
rewrite Hzbk,
apply λ p, mt (ge_least_of_lt _ p) Hk',
apply nat.lt_trans Hk,

1
library/data/int/power.lean
View file

@ -8,7 +8,6 @@ The power function on the integers.
import data.int.basic data.int.order data.int.div algebra.group_power data.nat.power
namespace int
open algebra
definition int_has_pow_nat [reducible] [instance] [priority int.prio] : has_pow_nat int :=
has_pow_nat.mk has_pow_nat.pow_nat

1
library/data/list/basic.lean
View file

@ -7,7 +7,6 @@ Basic properties of lists.
-/
import logic tools.helper_tactics data.nat.order data.nat.sub
open eq.ops helper_tactics nat prod function option
open algebra
inductive list (T : Type) : Type :=
| nil {} : list T

2
library/data/list/comb.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn
List combinators.
-/
import data.list.basic data.equiv
open nat prod decidable function helper_tactics algebra
open nat prod decidable function helper_tactics
namespace list
variables {A B C : Type}

1
library/data/list/sort.lean
View file

@ -176,7 +176,6 @@ have p : sort R l₁ ~ sort R l₂, from calc
eq_of_sorted_of_perm tr asy p s₁ s₂
section
open algebra
omit decR
lemma strongly_sorted_sort [ord : decidable_linear_order A] (l : list A) : strongly_sorted le (sort le l) :=
strongly_sorted_sort_core le.total (@le.trans A _) le.refl l

18
library/data/matrix.lean
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
Matrices
-/
import algebra.ring data.fin data.fintype
open algebra fin nat
open fin nat
definition matrix [reducible] (A : Type) (m n : nat) := fin m → fin n → A
@ -83,17 +83,17 @@ has_mul.mk matrix.mul
infix ` × ` := mul
infix `⬝` := smul
lemma add_zero (M : matrix A m n) : M + 0 = M :=
matrix.ext (λ i j, !algebra.add_zero)
protected lemma add_zero (M : matrix A m n) : M + 0 = M :=
matrix.ext (λ i j, !add_zero)
lemma zero_add (M : matrix A m n) : 0 + M = M :=
matrix.ext (λ i j, !algebra.zero_add)
protected lemma zero_add (M : matrix A m n) : 0 + M = M :=
matrix.ext (λ i j, !zero_add)
lemma add.comm (M : matrix A m n) (N : matrix A m n) : M + N = N + M :=
matrix.ext (λ i j, !algebra.add.comm)
protected lemma add.comm (M : matrix A m n) (N : matrix A m n) : M + N = N + M :=
matrix.ext (λ i j, !add.comm)
lemma add.assoc (M : matrix A m n) (N : matrix A m n) (P : matrix A m n) : (M + N) + P = M + (N + P) :=
matrix.ext (λ i j, !algebra.add.assoc)
protected lemma add.assoc (M : matrix A m n) (N : matrix A m n) (P : matrix A m n) : (M + N) + P = M + (N + P) :=
matrix.ext (λ i j, !add.assoc)
definition is_diagonal (M : matrix A n n) :=
∀ i j, i = j ∨ M[i, j] = 0

5
library/data/nat/basic.lean
View file

@ -285,9 +285,8 @@ nat.cases_on n
... = succ (succ n' * m' + n') : add_succ)⁻¹
!succ_ne_zero))
open algebra
protected definition comm_semiring [reducible] [trans_instance] : algebra.comm_semiring nat :=
⦃algebra.comm_semiring,
protected definition comm_semiring [reducible] [trans_instance] : comm_semiring nat :=
⦃comm_semiring,
add := nat.add,
add_assoc := nat.add_assoc,
zero := nat.zero,

165
library/data/nat/bigops.lean
View file

@ -1,165 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Finite products and sums on the natural numbers.
-/
import data.nat.basic data.nat.order algebra.group_bigops algebra.group_set_bigops
open list
namespace nat
open [classes] algebra
local attribute nat.comm_semiring [instance]
variables {A : Type} [deceqA : decidable_eq A]
/- Prodl -/
definition Prodl (l : list A) (f : A → nat) : nat := algebra.Prodl l f
notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r
theorem Prodl_nil (f : A → nat) : Prodl [] f = 1 := algebra.Prodl_nil f
theorem Prodl_cons (f : A → nat) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f :=
algebra.Prodl_cons f a l
theorem Prodl_append (l₁ l₂ : list A) (f : A → nat) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f :=
algebra.Prodl_append l₁ l₂ f
theorem Prodl_mul (l : list A) (f g : A → nat) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
section deceqA
include deceqA
theorem Prodl_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) :
Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H
theorem Prodl_insert_of_not_mem (f : A → nat) {a : A} {l : list A} (H : a ∉ l) :
Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H
theorem Prodl_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) :
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
theorem Prodl_one (l : list A) : Prodl l (λ x, nat.succ 0) = 1 := algebra.Prodl_one l
end deceqA
/- Prod over finset -/
namespace finset
open finset
definition Prod (s : finset A) (f : A → nat) : nat := algebra.finset.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.finset.Prod_empty f
theorem Prod_mul (s : finset A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.finset.Prod_mul s f g
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj
theorem Prod_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.finset.Prod_ext H
theorem Prod_one (s : finset A) : Prod s (λ x, nat.succ 0) = 1 := algebra.finset.Prod_one s
end deceqA
end finset
/- Prod over set -/
namespace set
open set
noncomputable definition Prod (s : set A) (f : A → nat) : nat := algebra.set.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → nat) : Prod ∅ f = 1 := algebra.set.Prod_empty f
theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Prod s f = 1 :=
algebra.set.Prod_of_not_finite nfins f
theorem Prod_mul (s : set A) (f g : A → nat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.set.Prod_mul s f g
theorem Prod_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj
theorem Prod_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.set.Prod_ext H
theorem Prod_one (s : set A) : Prod s (λ x, nat.succ 0) = 1 := algebra.set.Prod_one s
end set
/- Suml -/
definition Suml (l : list A) (f : A → nat) : nat := algebra.Suml l f
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
theorem Suml_nil (f : A → nat) : Suml [] f = 0 := algebra.Suml_nil f
theorem Suml_cons (f : A → nat) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
algebra.Suml_cons f a l
theorem Suml_append (l₁ l₂ : list A) (f : A → nat) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
algebra.Suml_append l₁ l₂ f
theorem Suml_add (l : list A) (f g : A → nat) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
section deceqA
include deceqA
theorem Suml_insert_of_mem (f : A → nat) {a : A} {l : list A} (H : a ∈ l) :
Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H
theorem Suml_insert_of_not_mem (f : A → nat) {a : A} {l : list A} (H : a ∉ l) :
Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H
theorem Suml_union {l₁ l₂ : list A} (f : A → nat) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
theorem Suml_zero (l : list A) : Suml l (λ x, zero) = 0 := algebra.Suml_zero l
end deceqA
/- Sum over a finset -/
namespace finset
open finset
definition Sum (s : finset A) (f : A → nat) : nat := algebra.finset.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.finset.Sum_empty f
theorem Sum_add (s : finset A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.finset.Sum_add s f g
section deceqA
include deceqA
theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : finset A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : finset A} (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → nat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj
theorem Sum_ext {s : finset A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.finset.Sum_ext H
theorem Sum_zero (s : finset A) : Sum s (λ x, zero) = 0 := algebra.finset.Sum_zero s
end deceqA
end finset
/- Sum over a set -/
namespace set
open set
noncomputable definition Sum (s : set A) (f : A → nat) : nat := algebra.set.Sum s f
notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → nat) : Sum ∅ f = 0 := algebra.set.Sum_empty f
theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → nat) : Sum s f = 0 :=
algebra.set.Sum_of_not_finite nfins f
theorem Sum_add (s : set A) (f g : A → nat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.set.Sum_add s f g
theorem Sum_insert_of_mem (f : A → nat) {a : A} {s : set A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → nat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → nat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj
theorem Sum_ext {s : set A} {f g : A → nat} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.set.Sum_ext H
theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s
end set
end nat

1
library/data/nat/div.lean
View file

@ -7,7 +7,6 @@ Definitions and properties of div and mod. Much of the development follows Isabe
-/
import data.nat.sub
open eq.ops well_founded decidable prod
open algebra
namespace nat

2
library/data/nat/examples/fib2.lean
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
Show that tail recursive fib is equal to standard one.
-/
import data.nat
open nat algebra
open nat
definition fib : nat → nat
| 0 := 1

2
library/data/nat/examples/partial_sum.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import data.nat
open nat algebra
open nat
definition partial_sum : nat → nat
| 0 := 0

1
library/data/nat/fact.lean
View file

@ -6,7 +6,6 @@ Authors: Leonardo de Moura
Factorial
-/
import data.nat.div
open algebra
namespace nat
definition fact : nat → nat

2
library/data/nat/find.lean
View file

@ -11,7 +11,7 @@ choose {p : nat → Prop} [d : decidable_pred p] : (∃ x, p x) → nat
choose_spec {p : nat → Prop} [d : decidable_pred p] (ex : ∃ x, p x) : p (choose ex)
-/
import data.nat.basic data.nat.order
open nat subtype decidable well_founded algebra
open nat subtype decidable well_founded
namespace nat
section find_x

1
library/data/nat/gcd.lean
View file

@ -7,7 +7,6 @@ Definitions and properties of gcd, lcm, and coprime.
-/
import .div
open eq.ops well_founded decidable prod
open algebra
namespace nat

28
library/data/nat/order.lean
View file

@ -6,7 +6,7 @@ Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
The order relation on the natural numbers.
-/
import data.nat.basic algebra.ordered_ring
open eq.ops algebra
open eq.ops
namespace nat
@ -90,11 +90,9 @@ protected theorem mul_lt_mul_of_pos_right {n m k : ℕ} (H : n < m) (Hk : k > 0)
/- nat is an instance of a linearly ordered semiring and a lattice -/
open algebra
protected definition decidable_linear_ordered_semiring [reducible] [trans_instance] :
algebra.decidable_linear_ordered_semiring nat :=
⦃ algebra.decidable_linear_ordered_semiring, nat.comm_semiring,
decidable_linear_ordered_semiring nat :=
⦃ decidable_linear_ordered_semiring, nat.comm_semiring,
add_left_cancel := @nat.add_left_cancel,
add_right_cancel := @nat.add_right_cancel,
lt := nat.lt,
@ -123,38 +121,38 @@ definition nat_has_dvd [reducible] [instance] [priority nat.prio] : has_dvd nat
has_dvd.mk has_dvd.dvd
theorem add_pos_left {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < a + b :=
@algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
@add_pos_of_pos_of_nonneg _ _ a b H !zero_le
theorem add_pos_right {a : ℕ} (H : 0 < a) (b : ℕ) : 0 < b + a :=
by rewrite add.comm; apply add_pos_left H b
theorem add_eq_zero_iff_eq_zero_and_eq_zero {a b : ℕ} :
a + b = 0 ↔ a = 0 ∧ b = 0 :=
@algebra.add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
@add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg _ _ a b !zero_le !zero_le
theorem le_add_of_le_left {a b c : ℕ} (H : b ≤ c) : b ≤ a + c :=
@algebra.le_add_of_nonneg_of_le _ _ a b c !zero_le H
@le_add_of_nonneg_of_le _ _ a b c !zero_le H
theorem le_add_of_le_right {a b c : ℕ} (H : b ≤ c) : b ≤ c + a :=
@algebra.le_add_of_le_of_nonneg _ _ a b c H !zero_le
@le_add_of_le_of_nonneg _ _ a b c H !zero_le
theorem lt_add_of_lt_left {b c : ℕ} (H : b < c) (a : ℕ) : b < a + c :=
@algebra.lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
@lt_add_of_nonneg_of_lt _ _ a b c !zero_le H
theorem lt_add_of_lt_right {b c : ℕ} (H : b < c) (a : ℕ) : b < c + a :=
@algebra.lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
@lt_add_of_lt_of_nonneg _ _ a b c H !zero_le
theorem lt_of_mul_lt_mul_left {a b c : ℕ} (H : c * a < c * b) : a < b :=
@algebra.lt_of_mul_lt_mul_left _ _ a b c H !zero_le
@lt_of_mul_lt_mul_left _ _ a b c H !zero_le
theorem lt_of_mul_lt_mul_right {a b c : ℕ} (H : a * c < b * c) : a < b :=
@algebra.lt_of_mul_lt_mul_right _ _ a b c H !zero_le
@lt_of_mul_lt_mul_right _ _ a b c H !zero_le
theorem pos_of_mul_pos_left {a b : ℕ} (H : 0 < a * b) : 0 < b :=
@algebra.pos_of_mul_pos_left _ _ a b H !zero_le
@pos_of_mul_pos_left _ _ a b H !zero_le
theorem pos_of_mul_pos_right {a b : ℕ} (H : 0 < a * b) : 0 < a :=
@algebra.pos_of_mul_pos_right _ _ a b H !zero_le
@pos_of_mul_pos_right _ _ a b H !zero_le
theorem zero_le_one : (0:nat) ≤ 1 :=
dec_trivial

5
library/data/nat/pairing.lean
View file

@ -7,7 +7,6 @@ Elegant pairing function.
-/
import data.nat.sqrt data.nat.div
open prod decidable
open algebra
namespace nat
definition mkpair (a b : nat) : nat :=
@ -30,7 +29,7 @@ by_cases
(suppose h₁ : ¬ n - s*s < s,
have s ≤ n - s*s, from le_of_not_gt h₁,
assert s + s*s ≤ n - s*s + s*s, from add_le_add_right this (s*s),
assert s*s + s ≤ n, by rewrite [nat.sub_add_cancel (sqrt_lower n) at this,
assert s*s + s ≤ n, by rewrite [nat.sub_add_cancel (sqrt_lower n) at this,
add.comm at this]; assumption,
have n ≤ s*s + s + s, from sqrt_upper n,
have n - s*s ≤ s + s, from calc
@ -69,7 +68,7 @@ by_cases
esimp [mkpair],
rewrite [if_neg `¬ a < b`],
esimp [unpair],
rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *nat.add_sub_cancel_left,
rewrite [add.assoc (a * a) a b, sqrt_offset_eq `a + b ≤ a + a`, *nat.add_sub_cancel_left,
if_neg `¬ a + b < a`]
end)

1
library/data/nat/parity.lean
View file

@ -9,7 +9,6 @@ import data.nat.power logic.identities
namespace nat
open decidable
open algebra
definition even (n : nat) := n % 2 = 0

3
library/data/nat/power.lean
View file

@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Jeremy Avigad
The power function on the natural numbers.
-/
import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_power
open algebra
namespace nat
@ -14,7 +13,7 @@ definition nat_has_pow_nat [instance] [reducible] [priority nat.prio] : has_pow_
has_pow_nat.mk has_pow_nat.pow_nat
theorem pow_le_pow_of_le {x y : ℕ} (i : ℕ) (H : x ≤ y) : x^i ≤ y^i :=
algebra.pow_le_pow_of_le i !zero_le H
pow_le_pow_of_le i !zero_le H
theorem eq_zero_of_pow_eq_zero {a m : ℕ} (H : a^m = 0) : a = 0 :=
or.elim (eq_zero_or_pos m)

1
library/data/nat/sqrt.lean
View file

@ -10,7 +10,6 @@ import data.nat.order data.nat.sub
namespace nat
open decidable
open algebra
-- This is the simplest possible function that just performs a linear search
definition sqrt_aux : nat → nat → nat

8
library/data/nat/sub.lean
View file

@ -6,7 +6,7 @@ Authors: Floris van Doorn, Jeremy Avigad
Subtraction on the natural numbers, as well as min, max, and distance.
-/
import .order
open eq.ops algebra
open eq.ops
namespace nat
@ -144,7 +144,7 @@ calc
... = n * m - n * k : {!mul.comm}
protected theorem mul_self_sub_mul_self_eq (a b : nat) : a * a - b * b = (a + b) * (a - b) :=
by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b),
by rewrite [nat.mul_sub_left_distrib, *right_distrib, mul.comm b a, add.comm (a*a) (a*b),
nat.add_sub_add_left]
theorem succ_mul_succ_eq (a : nat) : succ a * succ a = a*a + a + a + 1 :=
@ -290,8 +290,6 @@ sub.cases
... = k - n + n : nat.sub_add_cancel H3,
le.intro (add.right_cancel H4))
open algebra
protected theorem sub_pos_of_lt {m n : ℕ} (H : m < n) : n - m > 0 :=
assert H1 : n = n - m + m, from (nat.sub_add_cancel (le_of_lt H))⁻¹,
have H2 : 0 + m < n - m + m, begin rewrite [zero_add, -H1], exact H end,
@ -484,7 +482,7 @@ or.elim !le.total
lemma dist_eq_max_sub_min {i j : nat} : dist i j = (max i j) - min i j :=
or.elim (lt_or_ge i j)
(suppose i < j,
(suppose i < j,
by rewrite [max_eq_right_of_lt this, min_eq_left_of_lt this, dist_eq_sub_of_lt this])
(suppose i ≥ j,
by rewrite [max_eq_left this , min_eq_right this, dist_eq_sub_of_ge this])

37
library/data/pnat.lean
View file

@ -10,7 +10,6 @@ are those needed for that construction.
-/
import data.rat.order data.nat
open nat rat subtype eq.ops
open algebra
namespace pnat
@ -150,7 +149,7 @@ begin
unfold inv,
change 1 / rat_of_pnat n ≤ 1 / 1,
apply one_div_le_one_div_of_le,
apply algebra.zero_lt_one,
apply zero_lt_one,
apply rat_of_pnat_ge_one
end
@ -159,7 +158,7 @@ begin
unfold inv,
change 1 / rat_of_pnat n < 1 / 1,
apply one_div_lt_one_div_of_lt,
apply algebra.zero_lt_one,
apply zero_lt_one,
rewrite pnat.to_rat_of_nat,
apply (of_nat_lt_of_nat_of_lt H)
end
@ -177,7 +176,7 @@ protected theorem one_mul (n : ℕ+) : pone * n = n :=
begin
apply pnat.eq,
unfold pone,
rewrite [pnat.mul_def, ↑nat_of_pnat, algebra.one_mul]
rewrite [pnat.mul_def, ↑nat_of_pnat, one_mul]
end
theorem pone_le (n : ℕ+) : pone ≤ n :=
@ -220,9 +219,9 @@ pnat_le_of_rat_of_pnat_le (le_of_one_div_le_one_div !rat_of_pnat_is_pos H)
theorem two_mul (p : ℕ+) : rat_of_pnat (2 * p) = (1 + 1) * rat_of_pnat p :=
by rewrite pnat_to_rat_mul
theorem add_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ :=
protected theorem add_halves (p : ℕ+) : (2 * p)⁻¹ + (2 * p)⁻¹ = p⁻¹ :=
begin
rewrite [↑inv, -(add_halves (1 / (rat_of_pnat p))), algebra.div_div_eq_div_mul],
rewrite [↑inv, -(add_halves (1 / (rat_of_pnat p))), div_div_eq_div_mul],
have H : rat_of_pnat (2 * p) = rat_of_pnat p * (1 + 1), by rewrite [rat.mul_comm, two_mul],
rewrite *H
end
@ -231,15 +230,15 @@ theorem add_halves_double (m n : ℕ+) :
m⁻¹ + n⁻¹ = ((2 * m)⁻¹ + (2 * n)⁻¹) + ((2 * m)⁻¹ + (2 * n)⁻¹) :=
have hsimp [visible] : ∀ a b : ℚ, (a + a) + (b + b) = (a + b) + (a + b),
by intros; rewrite [rat.add_assoc, -(rat.add_assoc a b b), {_+b}rat.add_comm, -*rat.add_assoc],
by rewrite [-add_halves m, -add_halves n, hsimp]
by rewrite [-pnat.add_halves m, -pnat.add_halves n, hsimp]
protected theorem inv_mul_eq_mul_inv {p q : ℕ+} : (p * q)⁻¹ = p⁻¹ * q⁻¹ :=
begin rewrite [↑inv, pnat_to_rat_mul, algebra.one_div_mul_one_div] end
begin rewrite [↑inv, pnat_to_rat_mul, one_div_mul_one_div] end
protected theorem inv_mul_le_inv (p q : ℕ+) : (p * q)⁻¹ ≤ q⁻¹ :=
begin
rewrite [pnat.inv_mul_eq_mul_inv, -{q⁻¹}rat.one_mul at {2}],
apply algebra.mul_le_mul,
apply mul_le_mul,
apply inv_le_one,
apply le.refl,
apply le_of_lt,
@ -251,7 +250,7 @@ theorem pnat_mul_le_mul_left' (a b c : ℕ+) : a ≤ b → c * a ≤ c * b :=
begin
rewrite +pnat.le_def, intro H,
apply mul_le_mul_of_nonneg_left H,
apply algebra.le_of_lt,
apply le_of_lt,
apply pnat_pos
end
@ -298,8 +297,8 @@ by apply inv_gt_of_lt; apply lt_add_left
theorem div_le_pnat (q : ℚ) (n : ℕ+) (H : q ≥ n⁻¹) : 1 / q ≤ rat_of_pnat n :=
begin
apply algebra.div_le_of_le_mul,
apply algebra.lt_of_lt_of_le,
apply div_le_of_le_mul,
apply lt_of_lt_of_le,
apply pnat.inv_pos,
rotate 1,
apply H,
@ -320,7 +319,7 @@ by rewrite [rat.mul_comm, *pnat.inv_mul_eq_mul_inv, hsimp, *pnat.inv_cancel_left
definition pceil (a : ℚ) : ℕ+ := tag (ubound a) !ubound_pos
theorem pceil_helper {a : ℚ} {n : ℕ+} (H : pceil a ≤ n) (Ha : a > 0) : n⁻¹ ≤ 1 / a :=
algebra.le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a))
le.trans (inv_ge_of_le H) (one_div_le_one_div_of_le Ha (ubound_ge a))
theorem inv_pceil_div (a b : ℚ) (Ha : a > 0) (Hb : b > 0) : (pceil (a / b))⁻¹ ≤ b / a :=
assert (pceil (a / b))⁻¹ ≤ 1 / (1 / (b / a)),
@ -331,7 +330,7 @@ assert (pceil (a / b))⁻¹ ≤ 1 / (1 / (b / a)),
show 1 / (b / a) ≤ rat_of_pnat (pceil (a / b)),
begin
rewrite div_div_eq_mul_div,
rewrite algebra.one_mul,
rewrite one_mul,
apply ubound_ge
end
end,
@ -347,14 +346,14 @@ begin
apply exists.elim (exists_add_lt_and_pos_of_lt H),
intro c Hc,
existsi (pceil ((1 + 1 + 1) / c)),
apply algebra.lt.trans,
apply lt.trans,
rotate 1,
apply and.left Hc,
rewrite rat.add_assoc,
apply rat.add_lt_add_left,
rewrite -(algebra.add_halves c) at {3},
rewrite -(add_halves c) at {3},
apply add_lt_add,
repeat (apply algebra.lt_of_le_of_lt;
repeat (apply lt_of_le_of_lt;
apply inv_pceil_div;
apply dec_trivial;
apply and.right Hc;
@ -367,10 +366,10 @@ end
theorem nonneg_of_ge_neg_invs (a : ℚ) : (∀ n : ℕ+, -n⁻¹ ≤ a) → 0 ≤ a :=
begin
intro H,
apply algebra.le_of_not_gt,
apply le_of_not_gt,
suppose a < 0,
have H2 : 0 < -a, from neg_pos_of_neg this,
(algebra.not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc
(not_lt_of_ge !H) (iff.mp !lt_neg_iff_lt_neg (calc
(pceil (of_num 2 / -a))⁻¹ ≤ -a / of_num 2
: !inv_pceil_div dec_trivial H2
... < -a / 1

41
library/data/rat/basic.lean
View file

@ -7,7 +7,6 @@ The rational numbers as a field generated by the integers, defined as the usual
-/
import data.int algebra.field
open int quot eq.ops
open algebra
record prerat : Type :=
(num : ℤ) (denom : ℤ) (denom_pos : denom > 0)
@ -211,29 +210,29 @@ by esimp[equiv, smul]; rewrite[mul.assoc, mul.left_comm]
/- properties -/
theorem add.comm (a b : prerat) : add a b ≡ add b a :=
protected theorem add.comm (a b : prerat) : add a b ≡ add b a :=
by rewrite [↑add, ↑equiv, ▸*, add.comm, mul.comm (denom a)]
theorem add.assoc (a b c : prerat) : add (add a b) c ≡ add a (add b c) :=
protected theorem add.assoc (a b c : prerat) : add (add a b) c ≡ add a (add b c) :=
by rewrite [↑add, ↑equiv, ▸*, *(mul.comm (num c)), *(λy, mul.comm y (denom a)), *left_distrib,
*right_distrib, *mul.assoc, *add.assoc]
theorem add_zero (a : prerat) : add a zero ≡ a :=
protected theorem add_zero (a : prerat) : add a zero ≡ a :=
by rewrite [↑add, ↑equiv, ↑zero, ↑of_int, ▸*, *mul_one, zero_mul, add_zero]
theorem add.left_inv (a : prerat) : add (neg a) a ≡ zero :=
protected theorem add_left_inv (a : prerat) : add (neg a) a ≡ zero :=
by rewrite [↑add, ↑equiv, ↑neg, ↑zero, ↑of_int, ▸*, -neg_mul_eq_neg_mul, add.left_inv, *zero_mul]
theorem mul.comm (a b : prerat) : mul a b ≡ mul b a :=
protected theorem mul_comm (a b : prerat) : mul a b ≡ mul b a :=
by rewrite [↑mul, ↑equiv, mul.comm (num a), mul.comm (denom a)]
theorem mul.assoc (a b c : prerat) : mul (mul a b) c ≡ mul a (mul b c) :=
protected theorem mul_assoc (a b c : prerat) : mul (mul a b) c ≡ mul a (mul b c) :=
by rewrite [↑mul, ↑equiv, *mul.assoc]
theorem mul_one (a : prerat) : mul a one ≡ a :=
protected theorem mul_one (a : prerat) : mul a one ≡ a :=
by rewrite [↑mul, ↑one, ↑of_int, ↑equiv, ▸*, *mul_one]
theorem mul.left_distrib (a b c : prerat) : mul a (add b c) ≡ add (mul a b) (mul a c) :=
protected theorem mul_left_distrib (a b c : prerat) : mul a (add b c) ≡ add (mul a b) (mul a c) :=
have H : smul (denom a) (mul a (add b c)) (denom_pos a) =
add (mul a b) (mul a c), from begin
rewrite[↑smul, ↑mul, ↑add],
@ -258,7 +257,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on
mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_neg an_neg adp)
... ≡ one : begin
esimp [equiv, num, denom, one, mul, of_int],
rewrite [*int.mul_one, *int.one_mul, algebra.mul.comm,
rewrite [*int.mul_one, *int.one_mul, mul.comm,
neg_mul_comm]
end)
(assume an_zero : an = 0, absurd (equiv_zero_of_num_eq_zero an_zero) H)
@ -268,7 +267,7 @@ theorem mul_inv_cancel : ∀{a : prerat}, ¬ a ≡ zero → mul a (inv a) ≡ on
mul a (inv a) ≡ mul a ia : mul_equiv_mul !equiv.refl (inv_of_pos an_pos adp)
... ≡ one : begin
esimp [equiv, num, denom, one, mul, of_int],
rewrite [*int.mul_one, *int.one_mul, algebra.mul.comm]
rewrite [*int.mul_one, *int.one_mul, mul.comm]
end)
theorem zero_not_equiv_one : ¬ zero ≡ one :=
@ -306,8 +305,8 @@ theorem reduce_equiv : ∀ a : prerat, reduce a ≡ a
(assume anz : an = 0,
begin rewrite [↑reduce, if_pos anz, ↑equiv, anz], krewrite zero_mul end)
(assume annz : an ≠ 0,
by rewrite [↑reduce, if_neg annz, ↑equiv, algebra.mul.comm, -!int.mul_div_assoc
!gcd_dvd_left, -!int.mul_div_assoc !gcd_dvd_right, algebra.mul.comm])
by rewrite [↑reduce, if_neg annz, ↑equiv, mul.comm, -!int.mul_div_assoc
!gcd_dvd_left, -!int.mul_div_assoc !gcd_dvd_right, mul.comm])
theorem reduce_eq_reduce : ∀ {a b : prerat}, a ≡ b → reduce a = reduce b
| (mk an ad adpos) (mk bn bd bdpos) :=
@ -331,7 +330,7 @@ theorem reduce_eq_reduce : ∀ {a b : prerat}, a ≡ b → reduce a = reduce b
{apply div_gcd_eq_div_gcd H adpos bdpos},
{esimp, rewrite [gcd.comm, gcd.comm bn],
apply div_gcd_eq_div_gcd_of_nonneg,
rewrite [algebra.mul.comm, -H, algebra.mul.comm],
rewrite [mul.comm, -H, mul.comm],
apply annz,
apply bnnz,
apply le_of_lt adpos,
@ -486,13 +485,13 @@ quot.induction_on a (take u, quot.sound !prerat.add_zero)
protected theorem zero_add (a : ℚ) : 0 + a = a := !rat.add_comm ▸ !rat.add_zero
protected theorem add_left_inv (a : ℚ) : -a + a = 0 :=
quot.induction_on a (take u, quot.sound !prerat.add.left_inv)
quot.induction_on a (take u, quot.sound !prerat.add_left_inv)
protected theorem mul_comm (a b : ℚ) : a * b = b * a :=
quot.induction_on₂ a b (take u v, quot.sound !prerat.mul.comm)
quot.induction_on₂ a b (take u v, quot.sound !prerat.mul_comm)
protected theorem mul_assoc (a b c : ℚ) : a * b * c = a * (b * c) :=
quot.induction_on₃ a b c (take u v w, quot.sound !prerat.mul.assoc)
quot.induction_on₃ a b c (take u v w, quot.sound !prerat.mul_assoc)
protected theorem mul_one (a : ℚ) : a * 1 = a :=
quot.induction_on a (take u, quot.sound !prerat.mul_one)
@ -500,7 +499,7 @@ quot.induction_on a (take u, quot.sound !prerat.mul_one)
protected theorem one_mul (a : ℚ) : 1 * a = a := !rat.mul_comm ▸ !rat.mul_one
protected theorem left_distrib (a b c : ℚ) : a * (b + c) = a * b + a * c :=
quot.induction_on₃ a b c (take u v w, quot.sound !prerat.mul.left_distrib)
quot.induction_on₃ a b c (take u v w, quot.sound !prerat.mul_left_distrib)
protected theorem right_distrib (a b c : ℚ) : (a + b) * c = a * c + b * c :=
by rewrite [rat.mul_comm, rat.left_distrib, *rat.mul_comm c]
@ -551,8 +550,8 @@ decidable.by_cases
end))
protected definition discrete_field [reducible] [trans_instance] : algebra.discrete_field rat :=
⦃algebra.discrete_field,
protected definition discrete_field [reducible] [trans_instance] : discrete_field rat :=
⦃discrete_field,
add := rat.add,
add_assoc := rat.add_assoc,
zero := 0,
@ -588,7 +587,7 @@ iff.mpr (!eq_div_iff_mul_eq H) (mul_denom a)
theorem of_int_div {a b : ℤ} (H : b ∣ a) : of_int (a / b) = of_int a / of_int b :=
decidable.by_cases
(assume bz : b = 0,
by rewrite [bz, int.div_zero, of_int_zero, algebra.div_zero])
by rewrite [bz, int.div_zero, of_int_zero, div_zero])
(assume bnz : b ≠ 0,
have bnz' : of_int b ≠ 0, from assume oibz, bnz (of_int.inj oibz),
have H' : of_int (a / b) * of_int b = of_int a, from

165
library/data/rat/bigops.lean
View file

@ -1,165 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Finite products and sums on the rationals.
-/
import data.rat.order algebra.group_bigops algebra.group_set_bigops
open list
namespace rat
open [classes] algebra
local attribute rat.discrete_linear_ordered_field [instance]
variables {A : Type} [deceqA : decidable_eq A]
/- Prodl -/
definition Prodl (l : list A) (f : A → rat) : rat := algebra.Prodl l f
notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r
theorem Prodl_nil (f : A → rat) : Prodl [] f = 1 := algebra.Prodl_nil f
theorem Prodl_cons (f : A → rat) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f :=
algebra.Prodl_cons f a l
theorem Prodl_append (l₁ l₂ : list A) (f : A → rat) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f :=
algebra.Prodl_append l₁ l₂ f
theorem Prodl_mul (l : list A) (f g : A → rat) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
section deceqA
include deceqA
theorem Prodl_insert_of_mem (f : A → rat) {a : A} {l : list A} (H : a ∈ l) :
Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H
theorem Prodl_insert_of_not_mem (f : A → rat) {a : A} {l : list A} (H : a ∉ l) :
Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H
theorem Prodl_union {l₁ l₂ : list A} (f : A → rat) (d : disjoint l₁ l₂) :
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l
end deceqA
/- Prod over finset -/
namespace finset
open finset
definition Prod (s : finset A) (f : A → rat) : rat := algebra.finset.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → rat) : Prod ∅ f = 1 := algebra.finset.Prod_empty f
theorem Prod_mul (s : finset A) (f g : A → rat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.finset.Prod_mul s f g
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → rat) {a : A} {s : finset A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → rat) {a : A} {s : finset A} (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → rat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj
theorem Prod_ext {s : finset A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.finset.Prod_ext H
theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s
end deceqA
end finset
/- Prod over set -/
namespace set
open set
noncomputable definition Prod (s : set A) (f : A → rat) : rat := algebra.set.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → rat) : Prod ∅ f = 1 := algebra.set.Prod_empty f
theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → rat) : Prod s f = 1 :=
algebra.set.Prod_of_not_finite nfins f
theorem Prod_mul (s : set A) (f g : A → rat) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.set.Prod_mul s f g
theorem Prod_insert_of_mem (f : A → rat) {a : A} {s : set A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → rat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → rat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj
theorem Prod_ext {s : set A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.set.Prod_ext H
theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s
end set
/- Suml -/
definition Suml (l : list A) (f : A → rat) : rat := algebra.Suml l f
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
theorem Suml_nil (f : A → rat) : Suml [] f = 0 := algebra.Suml_nil f
theorem Suml_cons (f : A → rat) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
algebra.Suml_cons f a l
theorem Suml_append (l₁ l₂ : list A) (f : A → rat) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
algebra.Suml_append l₁ l₂ f
theorem Suml_add (l : list A) (f g : A → rat) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
section deceqA
include deceqA
theorem Suml_insert_of_mem (f : A → rat) {a : A} {l : list A} (H : a ∈ l) :
Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H
theorem Suml_insert_of_not_mem (f : A → rat) {a : A} {l : list A} (H : a ∉ l) :
Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H
theorem Suml_union {l₁ l₂ : list A} (f : A → rat) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l
end deceqA
/- Sum over a finset -/
namespace finset
open finset
definition Sum (s : finset A) (f : A → rat) : rat := algebra.finset.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → rat) : Sum ∅ f = 0 := algebra.finset.Sum_empty f
theorem Sum_add (s : finset A) (f g : A → rat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.finset.Sum_add s f g
section deceqA
include deceqA
theorem Sum_insert_of_mem (f : A → rat) {a : A} {s : finset A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → rat) {a : A} {s : finset A} (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → rat) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj
theorem Sum_ext {s : finset A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.finset.Sum_ext H
theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s
end deceqA
end finset
/- Sum over a set -/
namespace set
open set
noncomputable definition Sum (s : set A) (f : A → rat) : rat := algebra.set.Sum s f
notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → rat) : Sum ∅ f = 0 := algebra.set.Sum_empty f
theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → rat) : Sum s f = 0 :=
algebra.set.Sum_of_not_finite nfins f
theorem Sum_add (s : set A) (f g : A → rat) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.set.Sum_add s f g
theorem Sum_insert_of_mem (f : A → rat) {a : A} {s : set A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → rat) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → rat) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj
theorem Sum_ext {s : set A} {f g : A → rat} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.set.Sum_ext H
theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s
end set
end rat

2
library/data/rat/default.lean
View file

@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
-/
import .basic .order .bigops
import .basic .order

7
library/data/rat/order.lean
View file

@ -7,7 +7,6 @@ Adds the ordering, and instantiates the rationals as an ordered field.
-/
import data.int algebra.ordered_field algebra.group_power data.rat.basic
open quot eq.ops
open algebra
/- the ordering on representations -/
@ -303,8 +302,8 @@ let H' := rat.le_of_lt H in
!rat.lt_irrefl (Heq' ▸ H)))
protected definition discrete_linear_ordered_field [reducible] [trans_instance] :
algebra.discrete_linear_ordered_field rat :=
⦃algebra.discrete_linear_ordered_field,
discrete_linear_ordered_field rat :=
⦃discrete_linear_ordered_field,
rat.discrete_field,
le_refl := rat.le_refl,
le_trans := @rat.le_trans,
@ -433,7 +432,7 @@ theorem binary_nat_bound (a : ℕ) : of_nat a ≤ 2^a :=
(take n : nat, assume Hn,
calc
of_nat (nat.succ n) = (of_nat n) + 1 : of_nat_add
... ≤ 2^n + 1 : algebra.add_le_add_right Hn
... ≤ 2^n + 1 : add_le_add_right Hn
... ≤ 2^n + (2:rat)^n : add_le_add_left (pow_ge_one_of_ge_one two_ge_one _)
... = 2^(succ n) : pow_two_add)

117
library/data/real/basic.lean
View file

@ -22,7 +22,6 @@ The construction of the reals is arranged in four files.
-/
import data.nat data.rat.order data.pnat
open nat eq pnat
open algebra
open - [coercions] rat
local postfix `⁻¹` := pnat.inv
@ -51,17 +50,17 @@ have of_nat 3 * n⁻¹ < b, from calc
: mul_lt_mul_of_pos_right dec_trivial !pnat.inv_pos
... ≤ of_nat 4 * (b / of_nat 4)
: mul_le_mul_of_nonneg_left (!inv_pceil_div dec_trivial H) !of_nat_nonneg
... = b / of_nat 4 * of_nat 4 : algebra.mul.comm
... = b / of_nat 4 * of_nat 4 : mul.comm
... = b : !div_mul_cancel dec_trivial,
exists.intro n (calc
a + n⁻¹ + n⁻¹ + n⁻¹ = a + (1 + 1 + 1) * n⁻¹ : by rewrite [+right_distrib, +rat.one_mul, -+algebra.add.assoc]
a + n⁻¹ + n⁻¹ + n⁻¹ = a + (1 + 1 + 1) * n⁻¹ : by rewrite [+right_distrib, +rat.one_mul, -+add.assoc]
... = a + of_nat 3 * n⁻¹ : {show 1+1+1=of_nat 3, from dec_trivial}
... < a + b : rat.add_lt_add_left this a)
private theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b :=
begin
apply algebra.le_of_not_gt,
apply le_of_not_gt,
intro Hb,
cases exists_add_lt_and_pos_of_lt Hb with [c, Hc],
cases find_thirds b c (and.right Hc) with [j, Hbj],
@ -70,17 +69,17 @@ begin
end
private theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d :=
by rewrite [algebra.mul_sub_left_distrib, algebra.mul_sub_right_distrib, add_sub, algebra.sub_add_cancel]
by rewrite [mul_sub_left_distrib, mul_sub_right_distrib, add_sub, sub_add_cancel]
private theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) =
(a * b - d * e) + (a * c - f * g) :=
by rewrite [left_distrib, add_sub_comm]
private theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) :=
by rewrite[add_sub, algebra.sub_add_cancel]
by rewrite[add_sub, sub_add_cancel]
private theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) :=
by rewrite[*add_sub, *algebra.sub_add_cancel]
by rewrite[*add_sub, *sub_add_cancel]
private theorem rewrite_helper7 (a b c d x : ℚ) :
a * b * c - d = (b * c) * (a - x) + (x * b * c - d) :=
@ -88,12 +87,12 @@ begin
have ∀ (a b c : ℚ), a * b * c = b * c * a,
begin
intros a b c,
rewrite (algebra.mul.right_comm b c a),
rewrite (algebra.mul.comm b a)
rewrite (mul.right_comm b c a),
rewrite (mul.comm b a)
end,
rewrite[algebra.mul_sub_left_distrib, add_sub],
rewrite [mul_sub_left_distrib, add_sub],
calc
a * b * c - d = a * b * c - x * b * c + x * b * c - d : algebra.sub_add_cancel
a * b * c - d = a * b * c - x * b * c + x * b * c - d : sub_add_cancel
... = b * c * a - b * c * x + x * b * c - d :
begin
rewrite [this a b c, this x b c]
@ -119,14 +118,14 @@ have H2' : b ≤ (2 * k)⁻¹ * (m⁻¹ + n⁻¹),
exact H2
end,
have a + b ≤ k⁻¹ * (m⁻¹ + n⁻¹), from calc
a + b ≤ (2 * k)⁻¹ * (m⁻¹ + n⁻¹) + (2 * k)⁻¹ * (m⁻¹ + n⁻¹) : algebra.add_le_add H' H2'
a + b ≤ (2 * k)⁻¹ * (m⁻¹ + n⁻¹) + (2 * k)⁻¹ * (m⁻¹ + n⁻¹) : add_le_add H' H2'
... = ((2 * k)⁻¹ + (2 * k)⁻¹) * (m⁻¹ + n⁻¹) : by rewrite right_distrib
... = k⁻¹ * (m⁻¹ + n⁻¹) : by rewrite (pnat.add_halves k),
calc (rat_of_pnat k) * a + b * (rat_of_pnat k)
= (rat_of_pnat k) * a + (rat_of_pnat k) * b : by rewrite (algebra.mul.comm b)
... = (rat_of_pnat k) * (a + b) : algebra.left_distrib
= (rat_of_pnat k) * a + (rat_of_pnat k) * b : by rewrite (mul.comm b)
... = (rat_of_pnat k) * (a + b) : left_distrib
... ≤ (rat_of_pnat k) * (k⁻¹ * (m⁻¹ + n⁻¹)) :
iff.mp (!algebra.le_iff_mul_le_mul_left !rat_of_pnat_is_pos) this
iff.mp (!le_iff_mul_le_mul_left !rat_of_pnat_is_pos) this
... = m⁻¹ + n⁻¹ :
by rewrite[-mul.assoc, pnat.inv_cancel_left, one_mul]
@ -135,12 +134,12 @@ private theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e)))
a + b + c - (d + (b + e)) = a + b + c - (d + b + e) : rat.add_assoc
... = a + b - (d + b) + (c - e) : add_sub_comm
... = a + b - b - d + (c - e) : sub_add_eq_sub_sub_swap
... = a - d + (c - e) : algebra.add_sub_cancel)
... = a - d + (c - e) : add_sub_cancel)
private theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) :=
begin
let H := (binary.comm4 add.comm add.assoc a b c d),
rewrite [algebra.add.comm b d at H],
rewrite [add.comm b d at H],
exact H
end
@ -158,7 +157,7 @@ infix `≡` := equiv
theorem equiv.refl (s : seq) : s ≡ s :=
begin
intros,
rewrite [algebra.sub_self, abs_zero],
rewrite [sub_self, abs_zero],
apply add_invs_nonneg
end
@ -173,10 +172,10 @@ theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
∀ j : ℕ+, ∀ n : ℕ+, n ≥ 2 * j → abs (s n - t n) ≤ j⁻¹ :=
begin
intros [j, n, Hn],
apply algebra.le.trans,
apply le.trans,
apply H,
rewrite -(add_halves j),
apply algebra.add_le_add,
rewrite -(pnat.add_halves j),
apply add_le_add,
apply inv_ge_of_le Hn,
apply inv_ge_of_le Hn
end
@ -252,12 +251,12 @@ theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regula
intros,
existsi 2 * (2 * j),
intro n Hn,
rewrite [-sub_add_cancel (s n) (t n), *sub_eq_add_neg, algebra.add.assoc],
rewrite [-sub_add_cancel (s n) (t n), *sub_eq_add_neg, add.assoc],
apply rat.le_trans,
apply abs_add_le_abs_add_abs,
have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn,
have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn,
rewrite -(add_halves j),
rewrite -(pnat.add_halves j),
apply add_le_add,
exact Hst, exact Htu
end
@ -269,16 +268,16 @@ private definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1
private theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
calc
abs (s n) = abs (s n - s pone + s pone) : by rewrite algebra.sub_add_cancel
abs (s n) = abs (s n - s pone + s pone) : by rewrite sub_add_cancel
... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs
... ≤ n⁻¹ + pone⁻¹ + abs (s pone) : algebra.add_le_add_right !Hs
... ≤ n⁻¹ + pone⁻¹ + abs (s pone) : add_le_add_right !Hs
... = n⁻¹ + (1 + abs (s pone)) : by rewrite [pone_inv, rat.add_assoc]
... ≤ 1 + (1 + abs (s pone)) : algebra.add_le_add_right (inv_le_one n)
... ≤ 1 + (1 + abs (s pone)) : add_le_add_right (inv_le_one n)
... = abs (s pone) + (1 + 1) :
by rewrite [add.comm 1 (abs (s pone)), add.comm 1, rat.add_assoc]
... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : algebra.add_le_add_right (!ubound_ge)
... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : add_le_add_right (!ubound_ge)
... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add
... = of_nat (ubound (abs (s pone)) + 1 + 1) : algebra.add.assoc
... = of_nat (ubound (abs (s pone)) + 1 + 1) : add.assoc
... = rat_of_pnat (K s) : by esimp
theorem bdd_of_regular {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : ℕ+, s n ≤ b :=
@ -297,7 +296,7 @@ theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n :
intro n,
apply rat.lt_of_le_of_lt,
apply Hb,
apply algebra.lt_add_of_pos_right,
apply lt_add_of_pos_right,
apply zero_lt_one
end
@ -389,7 +388,7 @@ theorem s_add_comm (s t : seq) : sadd s t ≡ sadd t s :=
begin
esimp [sadd],
intro n,
rewrite [sub_add_eq_sub_sub, algebra.add_sub_cancel, algebra.sub_self, abs_zero],
rewrite [sub_add_eq_sub_sub, add_sub_cancel, sub_self, abs_zero],
apply add_invs_nonneg
end
@ -403,9 +402,9 @@ theorem s_add_assoc (s t u : seq) (Hs : regular s) (Hu : regular u) :
apply abs_add_le_abs_add_abs,
apply rat.le_trans,
rotate 1,
apply algebra.add_le_add_right,
apply add_le_add_right,
apply inv_two_mul_le_inv,
rewrite [-(add_halves (2 * n)), -(add_halves n), factor_lemma_2],
rewrite [-(pnat.add_halves (2 * n)), -(pnat.add_halves n), factor_lemma_2],
apply add_le_add,
apply Hs,
apply Hu
@ -415,7 +414,7 @@ theorem s_mul_comm (s t : seq) : smul s t ≡ smul t s :=
begin
rewrite ↑smul,
intros n,
rewrite [*(K₂_symm s t), rat.mul_comm, algebra.sub_self, abs_zero],
rewrite [*(K₂_symm s t), rat.mul_comm, sub_self, abs_zero],
apply add_invs_nonneg
end
@ -438,7 +437,7 @@ private theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
apply add_le_add,
rewrite 2 abs_mul,
apply le.refl,
rewrite [*rat.mul_assoc, -algebra.mul_sub_left_distrib, -left_distrib, abs_mul],
rewrite [*rat.mul_assoc, -mul_sub_left_distrib, -left_distrib, abs_mul],
apply mul_le_mul_of_nonneg_left,
rewrite rewrite_helper,
apply le.trans,
@ -470,7 +469,7 @@ private theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
(a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) :=
begin
repeat apply algebra.mul_le_mul,
repeat apply mul_le_mul,
apply Kq_bound Ht,
apply Kq_bound Hu,
apply abs_nonneg,
@ -489,17 +488,17 @@ private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular
(Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) :=
begin
apply add_le_add_three,
repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
repeat (assumption | apply mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg),
apply Hs,
apply abs_nonneg,
apply rat.mul_nonneg,
repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
repeat (assumption | apply mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg),
apply Hu,
apply abs_nonneg,
apply rat.mul_nonneg,
repeat (assumption | apply algebra.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
repeat (assumption | apply mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
apply abs_nonneg),
apply Ht,
apply abs_nonneg,
@ -554,7 +553,7 @@ theorem zero_is_reg : regular zero :=
begin
rewrite [↑regular, ↑zero],
intros,
rewrite [algebra.sub_zero, abs_zero],
rewrite [sub_zero, abs_zero],
apply add_invs_nonneg
end
@ -586,7 +585,7 @@ theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero :=
begin
rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv],
intros,
rewrite [neg_add_eq_sub, algebra.sub_self, algebra.sub_zero, abs_zero],
rewrite [neg_add_eq_sub, sub_self, sub_zero, abs_zero],
apply add_invs_nonneg
end
@ -632,7 +631,7 @@ private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (
apply rat.le_trans,
apply mul_le_mul_of_nonneg_right,
apply pceil_helper Hn,
{ repeat (apply algebra.mul_pos | apply algebra.add_pos | apply rat_of_pnat_is_pos |
{ repeat (apply mul_pos | apply add_pos | apply rat_of_pnat_is_pos |
apply pnat.inv_pos) },
apply rat.le_of_lt,
apply add_pos,
@ -654,9 +653,9 @@ private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (
apply rat.le_refl
end,
apply add_le_add,
rewrite [-algebra.mul_sub_left_distrib, abs_mul],
rewrite [-mul_sub_left_distrib, abs_mul],
apply rat.le_trans,
apply algebra.mul_le_mul,
apply mul_le_mul,
apply canon_bound,
apply Hs,
apply Ht,
@ -668,16 +667,16 @@ private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (
apply rat.le_refl,
apply rat.le_of_lt,
apply pnat.inv_pos,
rewrite [-algebra.mul_sub_right_distrib, abs_mul],
rewrite [-mul_sub_right_distrib, abs_mul],
apply rat.le_trans,
apply algebra.mul_le_mul,
apply mul_le_mul,
apply Hs,
apply canon_bound,
apply Ht,
apply abs_nonneg,
apply add_invs_nonneg,
rewrite [*pnat.inv_mul_eq_mul_inv, -right_distrib, mul.comm _ n⁻¹, rat.mul_assoc],
apply algebra.mul_le_mul,
apply mul_le_mul,
repeat apply rat.le_refl,
apply rat.le_of_lt,
apply rat.mul_pos,
@ -706,7 +705,7 @@ theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular
intros N2 HN2,
existsi max N1 N2,
intros n Hn,
rewrite [↑sadd at *, ↑smul, rewrite_helper3, -add_halves j, -*pnat.mul_assoc at *],
rewrite [↑sadd at *, ↑smul, rewrite_helper3, -pnat.add_halves j, -*pnat.mul_assoc at *],
apply rat.le_trans,
apply abs_add_le_abs_add_abs,
apply add_le_add,
@ -732,7 +731,7 @@ theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz :
cases Bd with [N, HN],
existsi N,
intro n Hn,
rewrite [↑equiv at Htz, ↑zero at *, algebra.sub_zero, ↑smul, abs_mul],
rewrite [↑equiv at Htz, ↑zero at *, sub_zero, ↑smul, abs_mul],
apply le.trans,
apply mul_le_mul,
apply Kq_bound Hs,
@ -784,11 +783,11 @@ theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
apply add_le_add_three,
apply Hs,
rewrite [↑sadd at He, ↑sneg at He, ↑zero at He],
let He' := λ a b c, eq.subst !algebra.sub_zero (He a b c),
let He' := λ a b c, eq.subst !sub_zero (He a b c),
apply (He' _ _ Hn),
apply Ht,
rewrite [hsimp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add_assoc],
apply algebra.add_le_add_right,
rewrite [hsimp, pnat.add_halves, -(pnat.add_halves j), -(pnat.add_halves (2 * j)), -*rat.add_assoc],
apply add_le_add_right,
apply add_le_add_three,
repeat (apply rat.le_trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv)
end
@ -797,7 +796,7 @@ theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero :=
begin
rewrite [↑equiv, ↑sadd, ↑sneg, ↑zero],
intros,
rewrite [algebra.sub_zero, algebra.add.right_inv, abs_zero],
rewrite [sub_zero, add.right_inv, abs_zero],
apply add_invs_nonneg
end
@ -880,7 +879,7 @@ theorem one_is_reg : regular one :=
begin
rewrite [↑regular, ↑one],
intros,
rewrite [algebra.sub_self, abs_zero],
rewrite [sub_self, abs_zero],
apply add_invs_nonneg
end
@ -890,7 +889,7 @@ theorem s_one_mul {s : seq} (H : regular s) : smul one s ≡ s :=
rewrite [↑smul, ↑one, rat.one_mul],
apply rat.le_trans,
apply H,
apply algebra.add_le_add_right,
apply add_le_add_right,
apply pnat.inv_mul_le_inv
end
@ -910,7 +909,7 @@ theorem zero_nequiv_one : ¬ zero ≡ one :=
intro Hz,
rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz],
let H := Hz (2 * 2),
rewrite [algebra.zero_sub at H, abs_neg at H, add_halves at H],
rewrite [zero_sub at H, abs_neg at H, pnat.add_halves at H],
have H' : pone⁻¹ ≤ 2⁻¹, from calc
pone⁻¹ = 1 : by rewrite -pone_inv
... = abs 1 : abs_of_pos zero_lt_one
@ -927,7 +926,7 @@ definition const (a : ℚ) : seq := λ n, a
theorem const_reg (a : ℚ) : regular (const a) :=
begin
intros,
rewrite [↑const, algebra.sub_self, abs_zero],
rewrite [↑const, sub_self, abs_zero],
apply add_invs_nonneg
end
@ -953,7 +952,7 @@ section
show abs (a - b) ≤ ε, from calc
abs (a - b) ≤ n⁻¹ + n⁻¹ : H₁ n
... ≤ ε / 2 + ε / 2 : add_le_add Hn Hn
... = ε : algebra.add_halves)
... = ε : add_halves)
end
---------------------------------------------
@ -1146,9 +1145,9 @@ protected theorem zero_ne_one : ¬ (0 : ℝ) = 1 :=
take H : 0 = 1,
absurd (quot.exact H) (r_zero_nequiv_one)
protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
protected definition comm_ring [reducible] : comm_ring ℝ :=
begin
fapply algebra.comm_ring.mk,
fapply comm_ring.mk,
exact add,
exact real.add_assoc,
exact of_num 0,

167
library/data/real/bigops.lean
View file

@ -1,167 +0,0 @@
/-
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
Finite products and sums on the reals.
-/
import data.real.division algebra.group_bigops algebra.group_set_bigops
open list
namespace real
open [classes] algebra
local attribute real.ordered_ring [instance]
local attribute real.comm_ring [instance]
variables {A : Type} [deceqA : decidable_eq A]
/- Prodl -/
definition Prodl (l : list A) (f : A → real) : real := algebra.Prodl l f
notation `∏` binders `←` l, r:(scoped f, Prodl l f) := r
theorem Prodl_nil (f : A → real) : Prodl [] f = 1 := algebra.Prodl_nil f
theorem Prodl_cons (f : A → real) (a : A) (l : list A) : Prodl (a::l) f = f a * Prodl l f :=
algebra.Prodl_cons f a l
theorem Prodl_append (l₁ l₂ : list A) (f : A → real) : Prodl (l₁++l₂) f = Prodl l₁ f * Prodl l₂ f :=
algebra.Prodl_append l₁ l₂ f
theorem Prodl_mul (l : list A) (f g : A → real) :
Prodl l (λx, f x * g x) = Prodl l f * Prodl l g := algebra.Prodl_mul l f g
section deceqA
include deceqA
theorem Prodl_insert_of_mem (f : A → real) {a : A} {l : list A} (H : a ∈ l) :
Prodl (insert a l) f = Prodl l f := algebra.Prodl_insert_of_mem f H
theorem Prodl_insert_of_not_mem (f : A → real) {a : A} {l : list A} (H : a ∉ l) :
Prodl (insert a l) f = f a * Prodl l f := algebra.Prodl_insert_of_not_mem f H
theorem Prodl_union {l₁ l₂ : list A} (f : A → real) (d : disjoint l₁ l₂) :
Prodl (union l₁ l₂) f = Prodl l₁ f * Prodl l₂ f := algebra.Prodl_union f d
theorem Prodl_one (l : list A) : Prodl l (λ x, 1) = 1 := algebra.Prodl_one l
end deceqA
/- Prod over finset -/
namespace finset
open finset
definition Prod (s : finset A) (f : A → real) : real := algebra.finset.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → real) : Prod ∅ f = 1 := algebra.finset.Prod_empty f
theorem Prod_mul (s : finset A) (f g : A → real) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.finset.Prod_mul s f g
section deceqA
include deceqA
theorem Prod_insert_of_mem (f : A → real) {a : A} {s : finset A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.finset.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → real) {a : A} {s : finset A} (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.finset.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → real) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.finset.Prod_union f disj
theorem Prod_ext {s : finset A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.finset.Prod_ext H
theorem Prod_one (s : finset A) : Prod s (λ x, 1) = 1 := algebra.finset.Prod_one s
end deceqA
end finset
/- Prod over set -/
namespace set
open set
noncomputable definition Prod (s : set A) (f : A → real) : real := algebra.set.Prod s f
notation `∏` binders `∈` s, r:(scoped f, Prod s f) := r
theorem Prod_empty (f : A → real) : Prod ∅ f = 1 := algebra.set.Prod_empty f
theorem Prod_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → real) : Prod s f = 1 :=
algebra.set.Prod_of_not_finite nfins f
theorem Prod_mul (s : set A) (f g : A → real) : Prod s (λx, f x * g x) = Prod s f * Prod s g :=
algebra.set.Prod_mul s f g
theorem Prod_insert_of_mem (f : A → real) {a : A} {s : set A} (H : a ∈ s) :
Prod (insert a s) f = Prod s f := algebra.set.Prod_insert_of_mem f H
theorem Prod_insert_of_not_mem (f : A → real) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Prod (insert a s) f = f a * Prod s f := algebra.set.Prod_insert_of_not_mem f H
theorem Prod_union (f : A → real) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Prod (s₁ ∪ s₂) f = Prod s₁ f * Prod s₂ f := algebra.set.Prod_union f disj
theorem Prod_ext {s : set A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) :
Prod s f = Prod s g := algebra.set.Prod_ext H
theorem Prod_one (s : set A) : Prod s (λ x, 1) = 1 := algebra.set.Prod_one s
end set
/- Suml -/
definition Suml (l : list A) (f : A → real) : real := algebra.Suml l f
notation `∑` binders `←` l, r:(scoped f, Suml l f) := r
theorem Suml_nil (f : A → real) : Suml [] f = 0 := algebra.Suml_nil f
theorem Suml_cons (f : A → real) (a : A) (l : list A) : Suml (a::l) f = f a + Suml l f :=
algebra.Suml_cons f a l
theorem Suml_append (l₁ l₂ : list A) (f : A → real) : Suml (l₁++l₂) f = Suml l₁ f + Suml l₂ f :=
algebra.Suml_append l₁ l₂ f
theorem Suml_add (l : list A) (f g : A → real) : Suml l (λx, f x + g x) = Suml l f + Suml l g :=
algebra.Suml_add l f g
section deceqA
include deceqA
theorem Suml_insert_of_mem (f : A → real) {a : A} {l : list A} (H : a ∈ l) :
Suml (insert a l) f = Suml l f := algebra.Suml_insert_of_mem f H
theorem Suml_insert_of_not_mem (f : A → real) {a : A} {l : list A} (H : a ∉ l) :
Suml (insert a l) f = f a + Suml l f := algebra.Suml_insert_of_not_mem f H
theorem Suml_union {l₁ l₂ : list A} (f : A → real) (d : disjoint l₁ l₂) :
Suml (union l₁ l₂) f = Suml l₁ f + Suml l₂ f := algebra.Suml_union f d
theorem Suml_zero (l : list A) : Suml l (λ x, 0) = 0 := algebra.Suml_zero l
end deceqA
/- Sum over a finset -/
namespace finset
open finset
definition Sum (s : finset A) (f : A → real) : real := algebra.finset.Sum s f
notation `∑` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → real) : Sum ∅ f = 0 := algebra.finset.Sum_empty f
theorem Sum_add (s : finset A) (f g : A → real) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.finset.Sum_add s f g
section deceqA
include deceqA
theorem Sum_insert_of_mem (f : A → real) {a : A} {s : finset A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.finset.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → real) {a : A} {s : finset A} (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.finset.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → real) {s₁ s₂ : finset A} (disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.finset.Sum_union f disj
theorem Sum_ext {s : finset A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.finset.Sum_ext H
theorem Sum_zero (s : finset A) : Sum s (λ x, 0) = 0 := algebra.finset.Sum_zero s
end deceqA
end finset
/- Sum over a set -/
namespace set
open set
noncomputable definition Sum (s : set A) (f : A → real) : real := algebra.set.Sum s f
notation `∏` binders `∈` s, r:(scoped f, Sum s f) := r
theorem Sum_empty (f : A → real) : Sum ∅ f = 0 := algebra.set.Sum_empty f
theorem Sum_of_not_finite {s : set A} (nfins : ¬ finite s) (f : A → real) : Sum s f = 0 :=
algebra.set.Sum_of_not_finite nfins f
theorem Sum_add (s : set A) (f g : A → real) : Sum s (λx, f x + g x) = Sum s f + Sum s g :=
algebra.set.Sum_add s f g
theorem Sum_insert_of_mem (f : A → real) {a : A} {s : set A} (H : a ∈ s) :
Sum (insert a s) f = Sum s f := algebra.set.Sum_insert_of_mem f H
theorem Sum_insert_of_not_mem (f : A → real) {a : A} {s : set A} [fins : finite s] (H : a ∉ s) :
Sum (insert a s) f = f a + Sum s f := algebra.set.Sum_insert_of_not_mem f H
theorem Sum_union (f : A → real) {s₁ s₂ : set A} [fins₁ : finite s₁] [fins₂ : finite s₂]
(disj : s₁ ∩ s₂ = ∅) :
Sum (s₁ ∪ s₂) f = Sum s₁ f + Sum s₂ f := algebra.set.Sum_union f disj
theorem Sum_ext {s : set A} {f g : A → real} (H : ∀x, x ∈ s → f x = g x) :
Sum s f = Sum s g := algebra.set.Sum_ext H
theorem Sum_zero (s : set A) : Sum s (λ x, 0) = 0 := algebra.set.Sum_zero s
end set
end real

74
library/data/real/complete.lean
View file

@ -16,7 +16,7 @@ are independent of each other.
-/
import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat
open rat algebra
open rat
local postfix ⁻¹ := pnat.inv
open eq.ops pnat classical
@ -31,8 +31,8 @@ theorem rat_approx {s : seq} (H : regular s) :
intro m Hm,
apply le.trans,
apply H,
rewrite -(add_halves n),
apply algebra.add_le_add_right,
rewrite -(pnat.add_halves n),
apply add_le_add_right,
apply inv_ge_of_le Hm
end
@ -54,13 +54,13 @@ theorem rat_approx_seq {s : seq} (H : regular s) :
apply le.trans,
rotate 1,
rewrite -sub_eq_add_neg,
apply algebra.sub_le_sub_left,
apply sub_le_sub_left,
apply HN,
apply pnat.le_trans,
apply Hp,
rewrite -*pnat.mul_assoc,
apply pnat.mul_le_mul_left,
rewrite [algebra.sub_self, -neg_zero],
rewrite [sub_self, -neg_zero],
apply neg_le_neg,
apply rat.le_of_lt,
apply pnat.inv_pos
@ -79,7 +79,7 @@ theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) :
apply iff.mp !le_add_iff_neg_le_sub_left,
apply le.trans,
apply Hs,
apply algebra.add_le_add_right,
apply add_le_add_right,
rewrite -*pnat.mul_assoc,
apply inv_ge_of_le,
apply pnat.mul_le_mul_left
@ -101,7 +101,7 @@ theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_a
existsi 2 * j,
intro n Hn,
cases em (s n ≥ 0) with [Hpos, Hneg],
rewrite [abs_of_nonneg Hpos, algebra.sub_self, abs_zero],
rewrite [abs_of_nonneg Hpos, sub_self, abs_zero],
apply rat.le_of_lt,
apply pnat.inv_pos,
let Hneg' := lt_of_not_ge Hneg,
@ -148,7 +148,7 @@ theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) :
krewrite pnat.add_halves,
apply le.refl,
let Hneg' := lt_of_not_ge Hneg,
rewrite [abs_of_neg Hneg', ↑sneg, sub_neg_eq_add, neg_add_eq_sub, algebra.sub_self,
rewrite [abs_of_neg Hneg', ↑sneg, sub_neg_eq_add, neg_add_eq_sub, sub_self,
abs_zero],
apply rat.le_of_lt,
apply pnat.inv_pos
@ -166,15 +166,15 @@ namespace real
open [classes] rat_seq
private theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
by rewrite [-sub_add_eq_sub_sub_swap, algebra.sub_add_cancel]
by rewrite [-sub_add_eq_sub_sub_swap, sub_add_cancel]
private theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :=
by rewrite [*add_sub, *algebra.sub_add_cancel]
by rewrite [*add_sub, *sub_add_cancel]
noncomputable definition rep (x : ℝ) : rat_seq.reg_seq := some (quot.exists_rep x)
definition re_abs (x : ℝ) : ℝ :=
quot.lift_on x (λ a, quot.mk (rat_seq.r_abs a))
quot.lift_on x (λ a, quot.mk (rat_seq.r_abs a))
(take a b Hab, quot.sound (rat_seq.r_abs_well_defined Hab))
theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
@ -183,7 +183,7 @@ theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
theorem r_abs_nonpos {x : ℝ} : x ≤ zero → re_abs x = -x :=
quot.induction_on x (λ a Ha, quot.sound (rat_seq.r_equiv_neg_abs_of_le_zero Ha))
private theorem abs_const' (a : ℚ) : of_rat (abs a) = re_abs (of_rat a) :=
private theorem abs_const' (a : ℚ) : of_rat (abs a) = re_abs (of_rat a) :=
quot.sound (rat_seq.r_abs_const a)
private theorem re_abs_is_abs : re_abs = abs := funext
@ -192,7 +192,7 @@ private theorem re_abs_is_abs : re_abs = abs := funext
apply eq.symm,
cases em (zero ≤ x) with [Hor1, Hor2],
rewrite [abs_of_nonneg Hor1, r_abs_nonneg Hor1],
have Hor2' : x ≤ zero, from algebra.le_of_lt (lt_of_not_ge Hor2),
have Hor2' : x ≤ zero, from le_of_lt (lt_of_not_ge Hor2),
rewrite [abs_of_neg (lt_of_not_ge Hor2), r_abs_nonpos Hor2']
end)
@ -227,9 +227,9 @@ theorem cauchy_with_rate_of_converges_to_with_rate {X : r_seq} {a : ℝ} {N :
begin
intro k m n Hm Hn,
rewrite (rewrite_helper9 a),
apply algebra.le.trans,
apply le.trans,
apply abs_add_le_abs_add_abs,
apply algebra.le.trans,
apply le.trans,
apply add_le_add,
apply Hc,
apply Hm,
@ -261,7 +261,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
abs (of_rat (lim_seq m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
(X (Nb M n) - of_rat (lim_seq n)) ≤ of_rat (m⁻¹ + n⁻¹) :=
begin
apply algebra.le.trans,
apply le.trans,
apply add_le_add_three,
apply approx_spec',
rotate 1,
@ -276,7 +276,7 @@ private theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) :
apply Nb_spec_right,
krewrite [-+of_rat_add],
change of_rat ((2 * m)⁻¹ + (2 * n)⁻¹ + (2 * n)⁻¹) ≤ of_rat (m⁻¹ + n⁻¹),
rewrite [algebra.add.assoc],
rewrite [add.assoc],
krewrite pnat.add_halves,
apply of_rat_le_of_rat_of_le,
apply add_le_add_right,
@ -290,7 +290,7 @@ theorem lim_seq_reg : rat_seq.regular lim_seq :=
intro m n,
apply le_of_of_rat_le_of_rat,
rewrite [abs_const, of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
apply algebra.le.trans,
apply le.trans,
apply abs_add_three,
cases em (M (2 * m) ≥ M (2 * n)) with [Hor1, Hor2],
apply lim_seq_reg_helper Hor1,
@ -331,9 +331,9 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
begin
intro k n Hn,
rewrite (rewrite_helper10 (X (Nb M n)) (of_rat (lim_seq n))),
apply algebra.le.trans,
apply le.trans,
apply abs_add_three,
apply algebra.le.trans,
apply le.trans,
apply add_le_add_three,
apply Hc,
apply pnat.le_trans,
@ -357,7 +357,7 @@ theorem converges_to_with_rate_of_cauchy_with_rate : converges_to_with_rate X li
krewrite [-+of_rat_add],
change of_rat ((2 * k)⁻¹ + (2 * n)⁻¹ + n⁻¹) ≤ of_rat k⁻¹,
apply of_rat_le_of_rat_of_le,
apply algebra.le.trans,
apply le.trans,
apply add_le_add_three,
apply rat.le_refl,
apply inv_ge_of_le,
@ -407,7 +407,7 @@ theorem archimedean_upper_strict (x : ℝ) : ∃ z : ℤ, x < of_int z :=
begin
cases archimedean_upper x with [z, Hz],
existsi z + 1,
apply algebra.lt_of_le_of_lt,
apply lt_of_le_of_lt,
apply Hz,
apply of_int_lt_of_int_of_lt,
apply lt_add_of_pos_right,
@ -436,8 +436,8 @@ private definition ex_floor (x : ℝ) :=
existsi some (archimedean_upper_strict x),
let Har := some_spec (archimedean_upper_strict x),
intros z Hz,
apply algebra.not_le_of_gt,
apply algebra.lt_of_lt_of_le,
apply not_le_of_gt,
apply lt_of_lt_of_le,
apply Har,
have H : of_int (some (archimedean_upper_strict x)) ≤ of_int z, begin
apply of_int_le_of_int_of_le,
@ -493,7 +493,7 @@ theorem floor_succ (x : ℝ) : floor (x + 1) = floor x + 1 :=
theorem floor_sub_one_lt_floor (x : ℝ) : floor (x - 1) < floor x :=
begin
apply @algebra.lt_of_add_lt_add_right ℤ _ _ 1,
apply @lt_of_add_lt_add_right ℤ _ _ 1,
rewrite [-floor_succ (x - 1), sub_add_cancel],
apply lt_add_of_pos_right dec_trivial
end
@ -511,9 +511,9 @@ let n := int.nat_abs (ceil (2 / ε)) in
assert int.of_nat n ≥ ceil (2 / ε),
by rewrite of_nat_nat_abs; apply le_abs_self,
have int.of_nat (succ n) ≥ ceil (2 / ε),
begin apply algebra.le.trans, exact this, apply int.of_nat_le_of_nat_of_le, apply le_succ end,
begin apply le.trans, exact this, apply int.of_nat_le_of_nat_of_le, apply le_succ end,
have H₁ : succ n ≥ ceil (2 / ε), from of_int_le_of_int_of_le this,
have H₂ : succ n ≥ 2 / ε, from !algebra.le.trans !le_ceil H₁,
have H₂ : succ n ≥ 2 / ε, from !le.trans !le_ceil H₁,
have H₃ : 2 / ε > 0, from div_pos_of_pos_of_pos two_pos H,
have 1 / succ n < ε, from calc
1 / succ n ≤ 1 / (2 / ε) : one_div_le_one_div_of_le H₃ H₂
@ -564,7 +564,7 @@ private theorem under_spec1 : of_rat under < elt :=
apply of_int_lt_of_int_of_lt,
apply floor_sub_one_lt_floor
end,
algebra.lt_of_lt_of_le H !floor_le
lt_of_lt_of_le H !floor_le
private theorem under_spec : ¬ ub under :=
begin
@ -584,14 +584,14 @@ private theorem over_spec1 : bound < of_rat over :=
apply of_int_lt_of_int_of_lt,
apply ceil_lt_ceil_succ
end,
algebra.lt_of_le_of_lt !le_ceil H
lt_of_le_of_lt !le_ceil H
private theorem over_spec : ub over :=
begin
rewrite ↑ub,
intro y Hy,
apply algebra.le_of_lt,
apply algebra.lt_of_le_of_lt,
apply le_of_lt,
apply lt_of_le_of_lt,
apply bdd,
apply Hy,
apply over_spec1
@ -656,9 +656,9 @@ private theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / ((
... = (over - under) / ((2^a) * 2) : by rewrite div_div_eq_div_mul
... = (over - under) / 2^(a + 1) : by rewrite pow_add,
cases em (ub (avg_seq a)),
rewrite [*if_pos a_1, -add_one, -Hou, ↑avg_seq, ↑avg, sub_eq_add_neg, algebra.add.assoc, -sub_eq_add_neg, div_two_sub_self],
rewrite [*if_pos a_1, -add_one, -Hou, ↑avg_seq, ↑avg, sub_eq_add_neg, add.assoc, -sub_eq_add_neg, div_two_sub_self],
rewrite [*if_neg a_1, -add_one, -Hou, ↑avg_seq, ↑avg, sub_add_eq_sub_sub,
algebra.sub_self_div_two]
sub_self_div_two]
end)
private theorem width_narrows : ∃ n : ℕ, over_seq n - under_seq n ≤ 1 :=
@ -732,7 +732,7 @@ private theorem under_lt_over : under < over :=
cases exists_not_of_not_forall under_spec with [x, Hx],
cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
apply lt_of_of_rat_lt_of_rat,
apply algebra.lt_of_lt_of_le,
apply lt_of_lt_of_le,
apply lt_of_not_ge Hxu,
apply over_spec _ HXx
end
@ -743,7 +743,7 @@ private theorem under_seq_lt_over_seq : ∀ m n : ℕ, under_seq m < over_seq n
cases exists_not_of_not_forall (PA m) with [x, Hx],
cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu],
apply lt_of_of_rat_lt_of_rat,
apply algebra.lt_of_lt_of_le,
apply lt_of_lt_of_le,
apply lt_of_not_ge Hxu,
apply PB,
apply HXx
@ -898,8 +898,8 @@ private theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y :=
intro n,
cases exists_not_of_not_forall (PA _) with [x, Hx],
cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxn],
apply algebra.le.trans,
apply algebra.le_of_lt,
apply le.trans,
apply le_of_lt,
apply lt_of_not_ge Hxn,
apply Hy,
apply HXx

2
library/data/real/default.lean
View file

@ -3,4 +3,4 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Robert Y. Lewis
-/
import .basic .order .division .complete .bigops
import .basic .order .division .complete

36
library/data/real/division.lean
View file

@ -11,7 +11,7 @@ and excluded middle.
import data.real.basic data.real.order data.rat data.nat
open rat
open nat
open eq.ops pnat classical algebra
open eq.ops pnat classical
namespace rat_seq
local postfix ⁻¹ := pnat.inv
@ -24,8 +24,8 @@ definition s_abs (s : seq) : seq := λ n, abs (s n)
theorem abs_reg_of_reg {s : seq} (Hs : regular s) : regular (s_abs s) :=
begin
intros,
apply algebra.le.trans,
apply algebra.abs_abs_sub_abs_le_abs_sub,
apply le.trans,
apply abs_abs_sub_abs_le_abs_sub,
apply Hs
end
@ -191,7 +191,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
cases em (m < ps Hs Hsep) with [Hmlt, Hmlt],
cases em (n < ps Hs Hsep) with [Hnlt, Hnlt],
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt), (s_inv_of_sep_lt_p Hs Hsep Hnlt)],
rewrite [algebra.sub_self, abs_zero],
rewrite [sub_self, abs_zero],
apply add_invs_nonneg,
rewrite [(s_inv_of_sep_lt_p Hs Hsep Hmlt),
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt))],
@ -200,7 +200,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply mul_le_mul,
apply Hs,
rewrite [-(mul_one 1), -(!field.div_mul_div Hsp Hspn), abs_mul],
apply algebra.mul_le_mul,
apply mul_le_mul,
rewrite -(s_inv_of_sep_lt_p Hs Hsep Hmlt),
apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)),
@ -210,7 +210,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply abs_nonneg,
apply add_invs_nonneg,
rewrite [right_distrib, *pnat_cancel', add.comm],
apply algebra.add_le_add_right,
apply add_le_add_right,
apply inv_ge_of_le,
apply pnat.le_of_lt,
apply Hmlt,
@ -219,10 +219,10 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))],
rewrite [(!div_sub_div Hspm Hsp), div_eq_mul_one_div, *abs_mul, *mul_one, *one_mul],
apply le.trans,
apply algebra.mul_le_mul,
apply mul_le_mul,
apply Hs,
rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hsp), abs_mul],
apply algebra.mul_le_mul,
apply mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)),
apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_lt_p Hs Hsep Hnlt),
@ -240,10 +240,10 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt))],
rewrite [(!div_sub_div Hspm Hspn), div_eq_mul_one_div, abs_mul, *one_mul, *mul_one],
apply le.trans,
apply algebra.mul_le_mul,
apply mul_le_mul,
apply Hs,
rewrite [-(mul_one 1), -(!field.div_mul_div Hspm Hspn), abs_mul],
apply algebra.mul_le_mul,
apply mul_le_mul,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hmlt)),
apply le_ps Hs Hsep,
rewrite -(s_inv_of_sep_gt_p Hs Hsep (pnat.le_of_not_gt Hnlt)),
@ -253,7 +253,7 @@ theorem reg_inv_reg {s : seq} (Hs : regular s) (Hsep : sep s zero) : regular (s_
apply abs_nonneg,
apply add_invs_nonneg,
rewrite [right_distrib, *pnat_cancel', add.comm],
apply algebra.le.refl
apply le.refl
end
theorem s_inv_ne_zero {s : seq} (Hs : regular s) (Hsep : sep s zero) (n : ℕ+) : s_inv Hs n ≠ 0 :=
@ -285,7 +285,7 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) :
intro n Hn,
have Hnz : s_inv Hs ((K₂ s (s_inv Hs)) * 2 * n) ≠ 0, from s_inv_ne_zero Hs Hsep _,
rewrite [↑smul, ↑one, mul.comm, -(mul_one_div_cancel Hnz),
-algebra.mul_sub_left_distrib, abs_mul],
-mul_sub_left_distrib, abs_mul],
apply le.trans,
apply mul_le_mul_of_nonneg_right,
apply canon_2_bound_right s,
@ -311,7 +311,7 @@ protected theorem mul_inv {s : seq} (Hs : regular s) (Hsep : sep s zero) :
apply rat_of_pnat_is_pos,
rewrite [left_distrib, pnat.mul_comm ((ps Hs Hsep) * (ps Hs Hsep)), *pnat.mul_assoc,
*(@pnat.inv_mul_eq_mul_inv (K₂ s (s_inv Hs))), -*mul.assoc, *pnat.inv_cancel_left,
*one_mul, -(add_halves j)],
*one_mul, -(pnat.add_halves j)],
apply add_le_add,
apply inv_ge_of_le,
apply pnat_mul_le_mul_left',
@ -432,7 +432,7 @@ theorem s_neg_neg {s : seq} : sneg (sneg s) ≡ s :=
begin
rewrite [↑equiv, ↑sneg],
intro n,
rewrite [neg_neg, algebra.sub_self, abs_zero],
rewrite [neg_neg, sub_self, abs_zero],
apply add_invs_nonneg
end
@ -638,8 +638,8 @@ noncomputable definition dec_lt : decidable_rel real.lt :=
end
protected noncomputable definition discrete_linear_ordered_field [reducible] [trans_instance]:
algebra.discrete_linear_ordered_field ℝ :=
⦃ algebra.discrete_linear_ordered_field, real.comm_ring, real.ordered_ring,
discrete_linear_ordered_field ℝ :=
⦃ discrete_linear_ordered_field, real.comm_ring, real.ordered_ring,
le_total := real.le_total,
mul_inv_cancel := real.mul_inv_cancel,
inv_mul_cancel := real.inv_mul_cancel,
@ -655,7 +655,7 @@ theorem of_rat_one : of_rat (1:rat) = (1:real) := rfl
theorem of_rat_divide (x y : ℚ) : of_rat (x / y) = of_rat x / of_rat y :=
by_cases
(assume yz : y = 0, by krewrite [yz, algebra.div_zero, +of_rat_zero, algebra.div_zero])
(assume yz : y = 0, by krewrite [yz, div_zero, +of_rat_zero, div_zero])
(assume ynz : y ≠ 0,
have ynz' : of_rat y ≠ 0, from assume yz', ynz (of_rat.inj yz'),
!eq_div_of_mul_eq ynz' (by krewrite [-of_rat_mul, !div_mul_cancel ynz]))
@ -684,7 +684,7 @@ have ∀ ε : ℝ, ε > 0 → x < ε, from
take ε, suppose ε > 0,
assert e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
assert ε / 2 < ε, from div_two_lt_of_pos `ε > 0`,
begin apply algebra.lt_of_le_of_lt, apply H _ e2pos, apply this end,
begin apply lt_of_le_of_lt, apply H _ e2pos, apply this end,
eq_zero_of_nonneg_of_forall_lt xnonneg this
theorem eq_zero_of_forall_abs_le {x : ℝ} (H : ∀ ε : ℝ, ε > 0 → abs x ≤ ε) :

84
library/data/real/order.lean
View file

@ -9,7 +9,7 @@ To do:
o Rename things and possibly make theorems private
-/
import data.real.basic data.rat data.nat
open rat nat eq pnat algebra
open rat nat eq pnat
local postfix `⁻¹` := pnat.inv
@ -32,19 +32,19 @@ theorem bdd_away_of_pos {s : seq} (Hs : regular s) (H : pos s) :
have Habs' : s m + abs (s m - s n) ≥ s n, from (iff.mpr (le_add_iff_sub_left_le _ _ _)) Habs,
have HN' : N⁻¹ + N⁻¹ ≤ s n - n⁻¹, begin
rewrite sub_eq_add_neg,
apply iff.mpr (algebra.le_add_iff_sub_right_le _ _ _),
apply iff.mpr (le_add_iff_sub_right_le _ _ _),
rewrite [sub_neg_eq_add, add.comm, -add.assoc],
apply le_of_lt HN
end,
rewrite add.comm at Habs',
have Hin : s m ≥ N⁻¹, from calc
s m ≥ s n - abs (s m - s n) : (iff.mp (le_add_iff_sub_left_le _ _ _)) Habs'
... ≥ s n - (m⁻¹ + n⁻¹) : algebra.sub_le_sub_left !Hs
... ≥ s n - (m⁻¹ + n⁻¹) : sub_le_sub_left !Hs
... = s n - m⁻¹ - n⁻¹ : by rewrite sub_add_eq_sub_sub
... = s n - n⁻¹ - m⁻¹ : by rewrite sub_sub_comm
... ≥ s n - n⁻¹ - N⁻¹ : algebra.sub_le_sub_left (inv_ge_of_le Hm)
... ≥ N⁻¹ + N⁻¹ - N⁻¹ : algebra.sub_le_sub_right HN'
... = N⁻¹ : by rewrite algebra.add_sub_cancel,
... ≥ s n - n⁻¹ - N⁻¹ : sub_le_sub_left (inv_ge_of_le Hm)
... ≥ N⁻¹ + N⁻¹ - N⁻¹ : sub_le_sub_right HN'
... = N⁻¹ : by rewrite add_sub_cancel,
apply Hin
end
@ -104,7 +104,7 @@ theorem nonneg_of_bdd_within {s : seq} (Hs : regular s)
apply add_pos;
repeat apply zero_lt_one;
exact Hε),
rewrite [algebra.add_halves],
rewrite [add_halves],
apply rat.le_refl
end
@ -122,7 +122,7 @@ theorem pos_of_pos_equiv {s t : seq} (Hs : regular s) (Heq : s ≡ t) (Hp : pos
rewrite sub_eq_add_neg,
apply iff.mpr !add_le_add_right_iff,
apply Hs4,
rewrite [*pnat.mul_assoc, pnat.add_halves, -(add_halves N), -sub_eq_add_neg, algebra.add_sub_cancel],
rewrite [*pnat.mul_assoc, pnat.add_halves, -(pnat.add_halves N), -sub_eq_add_neg, add_sub_cancel],
apply inv_two_mul_lt_inv
end
@ -141,7 +141,7 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
apply Heq,
apply le.trans,
rotate 1,
apply algebra.sub_le_sub_right,
apply sub_le_sub_right,
apply HNs,
apply pnat.le_trans,
rotate 1,
@ -158,11 +158,11 @@ theorem nonneg_of_nonneg_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (He
have Hms' : m⁻¹ + m⁻¹ ≤ (2 * 2 * n)⁻¹ + (2 * 2 * n)⁻¹, from add_le_add Hms Hms,
apply le.trans,
rotate 1,
apply algebra.sub_le_sub_left,
apply sub_le_sub_left,
apply Hms',
rewrite [*pnat.mul_assoc, pnat.add_halves, -neg_sub, -add_halves n, sub_neg_eq_add],
rewrite [*pnat.mul_assoc, pnat.add_halves, -neg_sub, -pnat.add_halves n, sub_neg_eq_add],
apply neg_le_neg,
apply algebra.add_le_add_left,
apply add_le_add_left,
apply inv_two_mul_le_inv
end
@ -229,7 +229,7 @@ theorem s_neg_add_eq_s_add_neg (s t : seq) : sneg (sadd s t) ≡ sadd (sneg s) (
begin
rewrite [↑equiv, ↑sadd, ↑sneg],
intros,
rewrite [neg_add, algebra.sub_self, abs_zero],
rewrite [neg_add, sub_self, abs_zero],
apply add_invs_nonneg
end
@ -271,7 +271,7 @@ theorem equiv_cancel_middle {s t u : seq} (Hs : regular s) (Ht : regular t)
repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
end
protected theorem add_le_add_of_le_right {s t : seq} (Hs : regular s) (Ht : regular t)
protected theorem add_le_add_of_le_right {s t : seq} (Hs : regular s) (Ht : regular t)
(Lst : s_le s t) : ∀ u : seq, regular u → s_le (sadd u s) (sadd u t) :=
begin
intro u Hu,
@ -294,7 +294,7 @@ theorem s_add_lt_add_left {s t : seq} (Hs : regular s) (Ht : regular t) (Hst : s
repeat (apply reg_add_reg | apply reg_neg_reg | assumption)
end
protected theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) :
protected theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg t) :
nonneg (sadd s t) :=
begin
intros,
@ -304,7 +304,7 @@ protected theorem add_nonneg_of_nonneg {s t : seq} (Hs : nonneg s) (Ht : nonneg
apply Ht
end
protected theorem le_trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
protected theorem le_trans {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
(Lst : s_le s t) (Ltu : s_le t u) : s_le s u :=
begin
rewrite ↑s_le at *,
@ -355,19 +355,19 @@ theorem equiv_of_le_of_ge {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s
rotate 2,
rewrite [↑s_le at *, ↑nonneg at *, ↑equiv, ↑sadd at *, ↑sneg at *],
intros,
rewrite [↑zero, algebra.sub_zero],
rewrite [↑zero, sub_zero],
apply abs_le_of_le_of_neg_le,
apply le_of_neg_le_neg,
rewrite [2 neg_add, neg_neg],
apply rat.le_trans,
apply algebra.neg_add_neg_le_neg_of_pos,
apply neg_add_neg_le_neg_of_pos,
apply pnat.inv_pos,
rewrite add.comm,
apply Lst,
apply le_of_neg_le_neg,
rewrite [neg_add, neg_neg],
apply rat.le_trans,
apply algebra.neg_add_neg_le_neg_of_pos,
apply neg_add_neg_le_neg_of_pos,
apply pnat.inv_pos,
apply Lts,
repeat assumption
@ -389,12 +389,12 @@ theorem le_and_sep_of_lt {s t : seq} (Hs : regular s) (Ht : regular t) (Lst : s_
exact (calc
sadd t (sneg s) n ≥ sadd t (sneg s) N - N⁻¹ - n⁻¹ : Habs
... ≥ 0 - n⁻¹: begin
apply algebra.sub_le_sub_right,
apply sub_le_sub_right,
apply rat.le_of_lt,
apply (iff.mpr (sub_pos_iff_lt _ _)),
apply HN
end
... = -n⁻¹ : by rewrite algebra.zero_sub),
... = -n⁻¹ : by rewrite zero_sub),
exact or.inl Lst
end
@ -422,7 +422,7 @@ theorem s_neg_zero : sneg zero ≡ zero :=
begin
rewrite ↑[sneg, zero, equiv],
intros,
rewrite [algebra.sub_zero, abs_neg, abs_zero],
rewrite [sub_zero, abs_neg, abs_zero],
apply add_invs_nonneg
end
@ -487,7 +487,7 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
rewrite ↑smul,
apply lt_of_lt_of_le,
rotate 1,
apply algebra.mul_le_mul,
apply mul_le_mul,
apply HNs,
apply pnat.le_trans,
apply pnat.max_left Ns Nt,
@ -508,9 +508,9 @@ theorem s_mul_pos_of_pos {s t : seq} (Hs : regular s) (Ht : regular t) (Hps : po
rewrite -pnat.mul_assoc,
apply pnat.mul_le_mul_left,
rewrite pnat.inv_mul_eq_mul_inv,
apply algebra.mul_lt_mul,
apply mul_lt_mul,
rewrite [pnat.inv_mul_eq_mul_inv, -one_mul Ns⁻¹],
apply algebra.mul_lt_mul,
apply mul_lt_mul,
apply inv_lt_one_of_gt,
apply dec_trivial,
apply inv_ge_of_le,
@ -556,7 +556,7 @@ theorem s_zero_mul {s : seq} : smul s zero ≡ zero :=
begin
rewrite [↑equiv, ↑smul, ↑zero],
intros,
rewrite [algebra.mul_zero, algebra.sub_zero, abs_zero],
rewrite [mul_zero, sub_zero, abs_zero],
apply add_invs_nonneg
end
@ -596,7 +596,7 @@ theorem s_mul_nonneg_of_nonneg {s t : seq} (Hs : regular s) (Ht : regular t)
intro Htn,
apply rat.le_trans,
rotate 1,
apply algebra.mul_le_mul_of_nonpos_right,
apply mul_le_mul_of_nonpos_right,
apply rat.le_trans,
apply le_abs_self,
apply canon_2_bound_left s t Hs,
@ -667,8 +667,8 @@ protected theorem not_lt_self (s : seq) : ¬ s_lt s s :=
rewrite [↑s_lt at Hlt, ↑pos at Hlt],
apply exists.elim Hlt,
intro n Hn, esimp at Hn,
rewrite [↑sadd at Hn,↑sneg at Hn, -sub_eq_add_neg at Hn, algebra.sub_self at Hn],
apply absurd Hn (algebra.not_lt_of_ge (rat.le_of_lt !pnat.inv_pos))
rewrite [↑sadd at Hn,↑sneg at Hn, -sub_eq_add_neg at Hn, sub_self at Hn],
apply absurd Hn (not_lt_of_ge (rat.le_of_lt !pnat.inv_pos))
end
theorem not_sep_self (s : seq) : ¬ s ≢ s :=
@ -773,7 +773,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
let Runt := reg_add_reg Hu (reg_neg_reg Ht),
have Hcan : ∀ m, sadd u (sneg s) m = (sadd t (sneg s)) m + (sadd u (sneg t)) m, begin
intro m,
rewrite [↑sadd, ↑sneg, -*algebra.sub_eq_add_neg, -sub_eq_sub_add_sub]
rewrite [↑sadd, ↑sneg, -*sub_eq_add_neg, -sub_eq_sub_add_sub]
end,
rewrite [↑s_lt at *, ↑s_le at *],
cases bdd_away_of_pos Rtns Hst with [Nt, HNt],
@ -784,7 +784,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rewrite Hcan,
apply rat.le_trans,
rotate 1,
apply algebra.add_le_add,
apply add_le_add,
apply HNt,
apply pnat.le_trans,
apply pnat.mul_le_mul_left 2,
@ -799,7 +799,7 @@ theorem s_lt_of_lt_of_le {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
apply Hn,
rotate_right 1,
apply pnat.max_right,
rewrite [-add_halves Nt, -sub_eq_add_neg, algebra.add_sub_cancel],
rewrite [-pnat.add_halves Nt, -sub_eq_add_neg, add_sub_cancel],
apply inv_ge_of_le,
apply pnat.max_left
end
@ -822,7 +822,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
rewrite Hcan,
apply rat.le_trans,
rotate 1,
apply algebra.add_le_add,
apply add_le_add,
apply HNt,
apply pnat.le_trans,
rotate 1,
@ -837,7 +837,7 @@ theorem s_lt_of_le_of_lt {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : r
apply Hn,
rotate_right 1,
apply pnat.max_left,
rewrite [-add_halves Nu, neg_add_cancel_left],
rewrite [-pnat.add_halves Nu, neg_add_cancel_left],
apply inv_ge_of_le,
apply pnat.max_left
end
@ -858,7 +858,7 @@ theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b
rewrite [↑s_le, ↑nonneg],
intro n,
rewrite [↑sadd, ↑sneg, ↑const],
apply algebra.le.trans,
apply le.trans,
apply neg_nonpos_of_nonneg,
apply rat.le_of_lt,
apply pnat.inv_pos,
@ -899,7 +899,7 @@ theorem lt_of_const_lt_const {a b : ℚ} (H : s_lt (const a) (const b)) : a < b
rewrite [↑s_lt at H, ↑pos at H, ↑const at H, ↑sadd at H, ↑sneg at H],
cases H with [n, Hn],
apply (iff.mp !sub_pos_iff_lt),
apply algebra.lt.trans,
apply lt.trans,
rotate 1,
exact Hn,
apply pnat.inv_pos
@ -910,7 +910,7 @@ theorem s_le_of_le_pointwise {s t : seq} (Hs : regular s) (Ht : regular t)
begin
rewrite [↑s_le, ↑nonneg, ↑sadd, ↑sneg],
intros,
apply algebra.le.trans,
apply le.trans,
apply iff.mpr !neg_nonpos_iff_nonneg,
apply le_of_lt,
apply pnat.inv_pos,
@ -1008,7 +1008,7 @@ theorem r_lt_of_const_lt_const {a b : ℚ} (H : r_lt (r_const a) (r_const b)) :
theorem r_le_of_le_reprs (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le s (r_const (reg_seq.sq t n))) : r_le s t :=
le_of_le_reprs (reg_seq.is_reg s) (reg_seq.is_reg t) Hle
theorem r_le_of_reprs_le (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le (r_const (reg_seq.sq t n)) s) :
theorem r_le_of_reprs_le (s t : reg_seq) (Hle : ∀ n : ℕ+, r_le (r_const (reg_seq.sq t n)) s) :
r_le t s :=
le_of_reprs_le (reg_seq.is_reg s) (reg_seq.is_reg t) Hle
@ -1018,9 +1018,9 @@ open real
open [classes] rat_seq
namespace real
protected definition lt (x y : ℝ) :=
protected definition lt (x y : ℝ) :=
quot.lift_on₂ x y (λ a b, rat_seq.r_lt a b) rat_seq.r_lt_well_defined
protected definition le (x y : ℝ) :=
protected definition le (x y : ℝ) :=
quot.lift_on₂ x y (λ a b, rat_seq.r_le a b) rat_seq.r_le_well_defined
definition real_has_lt [reducible] [instance] [priority real.prio] : has_lt ℝ :=
@ -1089,8 +1089,8 @@ protected theorem le_of_lt_or_eq (x y : ℝ) : x < y ∨ x = y → x ≤ y :=
apply (or.inr (quot.exact H'))
end)))
definition ordered_ring [reducible] [instance] : algebra.ordered_ring ℝ :=
⦃ algebra.ordered_ring, real.comm_ring,
definition ordered_ring [reducible] [instance] : ordered_ring ℝ :=
⦃ ordered_ring, real.comm_ring,
le_refl := real.le_refl,
le_trans := @real.le_trans,
mul_pos := real.mul_pos,

2
library/data/set/comm_semiring.lean
View file

@ -6,7 +6,7 @@ Author: Leonardo de Moura
(set A) is an instance of a commutative semiring
-/
import data.set.basic algebra.ring
open algebra set
open set
definition set_comm_semiring [instance] (A : Type) : comm_semiring (set A) :=
⦃ comm_semiring,

5
library/data/set/filter.lean
View file

@ -260,7 +260,7 @@ take s, suppose s ∈ F₂,
(bounded_exists.intro `s ∈ F₂` (by rewrite univ_inter; apply subset.refl))
theorem inf_refines (H₁ : F₁ ≽ F) (H₂ : F₂ ≽ F) : F₁ ⊓ F₂ ≽ F :=
take s, suppose s ∈ F₁ ⊓ F₂,
take s : set A, suppose (#set.filter s ∈ F₁ ⊓ F₂),
obtain a₁ [a₁F₁ [a₂ [a₂F₂ (Hsub : s ⊇ a₁ ∩ a₂)]]], from this,
have a₁ ∈ F, from H₁ a₁F₁,
have a₂ ∈ F, from H₂ a₂F₂,
@ -278,9 +278,8 @@ Sup_refines H
theorem refines_Inf {F : filter A} {S : set (filter A)} (FS : F ∈ S) : F ≽ ⨅ S :=
refines_Sup (λ G GS, GS F FS)
open algebra
protected definition complete_lattice_Inf [reducible] [instance] : complete_lattice_Inf (filter A) :=
⦃ algebra.complete_lattice_Inf,
⦃ complete_lattice_Inf,
le := weakens,
le_refl := weakens.refl,
le_trans := @weakens.trans A,

2
library/data/stream.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
import data.nat data.list data.equiv
open nat function option algebra
open nat function option
definition stream (A : Type) := nat → A

2
library/data/tuple.lean
View file

@ -7,7 +7,7 @@ Tuples are lists of a fixed size.
It is implemented as a subtype.
-/
import logic data.list data.fin
open nat list subtype function algebra
open nat list subtype function
definition tuple [reducible] (A : Type) (n : nat) := {l : list A | length l = n}

2
library/theories/analysis/metric_space.lean
View file

@ -6,7 +6,7 @@ Author: Jeremy Avigad
Metric spaces.
-/
import data.real.division
open real eq.ops classical algebra
open real eq.ops classical
structure metric_space [class] (M : Type) : Type :=
(dist : M → M → ℝ)

12
library/theories/analysis/real_limit.lean
View file

@ -20,8 +20,8 @@ The definitions here are noncomputable, for various reasons:
These could be avoided in a constructive theory of analysis, but here we will not
follow that route.
-/
import .metric_space data.real.complete
open real classical algebra
import .metric_space data.real.complete data.set
open real classical
noncomputable theory
namespace real
@ -32,7 +32,7 @@ protected definition to_metric_space [instance] : metric_space ℝ :=
⦃ metric_space,
dist := λ x y, abs (x - y),
dist_self := λ x, abstract by rewrite [sub_self, abs_zero] end,
eq_of_dist_eq_zero := λ x y, algebra.eq_of_abs_sub_eq_zero,
eq_of_dist_eq_zero := λ x y, eq_of_abs_sub_eq_zero,
dist_comm := abs_sub,
dist_triangle := abs_sub_le
⦄
@ -130,8 +130,8 @@ section
(take m n : ℕ+,
assume Hm : m ≥ (pnat.succ N),
assume Hn : n ≥ (pnat.succ N),
have Hm' : elt_of m ≥ N, begin apply algebra.le.trans, apply le_succ, apply Hm end,
have Hn' : elt_of n ≥ N, begin apply algebra.le.trans, apply le_succ, apply Hn end,
have Hm' : elt_of m ≥ N, begin apply le.trans, apply le_succ, apply Hm end,
have Hn' : elt_of n ≥ N, begin apply le.trans, apply le_succ, apply Hn end,
show abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹, from le_of_lt (H _ _ Hm' Hn'))
private definition rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) (k : ℕ+) : ℕ+ :=
@ -589,7 +589,7 @@ theorem translate_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous
split,
assumption,
intros x' Hx',
rewrite [add_sub_comm, sub_self, algebra.add_zero],
rewrite [add_sub_comm, sub_self, add_zero],
apply Hδ₂,
assumption
end

1
library/theories/combinatorics/choose.lean
View file

@ -7,7 +7,6 @@ Binomial coefficients, "n choose k".
-/
import data.nat.div data.nat.fact data.finset
open decidable
open algebra
namespace nat

10
library/theories/group_theory/action.lean
View file

@ -6,8 +6,8 @@ Author : Haitao Zhang
-/
import algebra.group data .hom .perm .finsubg
namespace group
open finset algebra function
namespace group_theory
open finset function
local attribute perm.f [coercion]
@ -249,7 +249,7 @@ lemma subg_moversets_of_orbit_eq_stab_lcosets :
existsi b, subst Ph₂, assumption
end))
open nat nat.finset
open nat
theorem orbit_stabilizer_theorem : card H = card (orbit hom H a) * card (stab hom H a) :=
calc card H = card (fin_lcosets (stab hom H a) H) * card (stab hom H a) : lagrange_theorem stab_subset
@ -297,7 +297,7 @@ take a b, propext (iff.intro
(assume Peq, Peq ▸ in_orbit_refl))
variables (hom) (H)
open nat nat.finset finset.partition fintype
open nat finset.partition fintype
definition orbit_partition : @partition S _ :=
mk univ (orbit hom H) orbit_is_partition
@ -572,4 +572,4 @@ lemma card_perm_step : card (perm (fin (succ n))) = (succ n) * card (perm (fin n
... = (succ n) * card (perm (fin n)) : by rewrite -card_lift_to_stab
end perm_fin
end group
end group_theory

6
library/theories/group_theory/cyclic.lean
View file

@ -7,10 +7,10 @@ Author : Haitao Zhang
import data algebra.group algebra.group_power .finsubg .hom .perm
open function algebra finset
open function finset
open eq.ops
namespace group
namespace group_theory
section cyclic
open nat fin list
@ -389,4 +389,4 @@ lemma rotl_perm_order (Pex : ∃ a b : A, a ≠ b) : order (rotl_perm A (succ n)
order_of_min_pow rotl_perm_pow_eq_one (rotl_perm_pow_ne_one Pex)
end rotg
end group
end group_theory

12
library/theories/group_theory/finsubg.lean
View file

@ -9,11 +9,11 @@ Author : Haitao Zhang
-- can be used directly without translating from the set based theory first
import data algebra.group .subgroup
open function algebra finset
open function finset
-- ⁻¹ in eq.ops conflicts with group ⁻¹
open eq.ops
namespace group
namespace group_theory
open ops
section subg
@ -173,8 +173,8 @@ definition fin_lcoset_partition_subg (Psub : H ⊆ G) :=
open nat
theorem lagrange_theorem (Psub : H ⊆ G) : card G = card (fin_lcosets H G) * card H := calc
card G = nat.finset.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub)
... = nat.finset.Sum (fin_lcosets H G) (λ x, card H) : nat.finset.Sum_ext (take g P, fin_lcosets_card_eq g P)
card G = finset.Sum (fin_lcosets H G) card : class_equation (fin_lcoset_partition_subg Psub)
... = finset.Sum (fin_lcosets H G) (λ x, card H) : finset.Sum_ext (take g P, fin_lcosets_card_eq g P)
... = card (fin_lcosets H G) * card H : Sum_const_eq_card_mul
end fin_lcoset
@ -304,7 +304,7 @@ fintype.mk (all_lcosets G H)
lemma card_lcoset_type : card (lcoset_type G H) = card (fin_lcosets H G) :=
length_all_lcosets
open nat nat.finset
open nat
variable [finsubgH : is_finsubg H]
include finsubgH
@ -532,4 +532,4 @@ is_finsubg.mk fcU_has_one fcU_mul_closed fcU_has_inv
end normalizer
end group
end group_theory

9
library/theories/group_theory/hom.lean
View file

@ -6,15 +6,14 @@ Author : Haitao Zhang
-/
import algebra.group data.set .subgroup
namespace group
namespace group_theory
open algebra
-- ⁻¹ in eq.ops conflicts with group ⁻¹
-- open eq.ops
notation H1 ▸ H2 := eq.subst H1 H2
open set
open function
open group.ops
open group_theory.ops
open quot
local attribute set [reducible]
@ -65,7 +64,7 @@ include h
theorem hom_map_one : f 1 = 1 :=
have P : f 1 = (f 1) * (f 1), from
calc f 1 = f (1*1) : mul_one
calc f 1 = f (1*1) : mul_one
... = (f 1) * (f 1) : is_hom f,
eq.symm (mul.right_inv (f 1) ▸ (mul_inv_eq_of_eq_mul P))
@ -190,4 +189,4 @@ theorem first_isomorphism_theorem : isomorphic (ker_natural_map : coset_of (ker
and.intro ker_map_is_inj ker_map_is_hom
end hom_theorem
end group
end group_theory

6
library/theories/group_theory/perm.lean
View file

@ -6,9 +6,9 @@ Author : Haitao Zhang
-/
import algebra.group data data.fintype.function
open nat list algebra function
open nat list function
namespace group
namespace group_theory
open fintype
section perm
@ -117,4 +117,4 @@ lemma perm_one : (1 : perm A) = perm.one := rfl
end perm
end group
end group_theory

8
library/theories/group_theory/pgroup.lean
View file

@ -6,9 +6,9 @@ Author : Haitao Zhang
import theories.number_theory.primes data algebra.group algebra.group_power algebra.group_bigops
import .cyclic .finsubg .hom .perm .action
open nat fin list algebra function subtype
open nat fin list function subtype
namespace group
namespace group_theory
section pgroup
@ -145,7 +145,7 @@ lemma peo_const_one : ∀ {n : nat}, peo (λ i : fin n, (1 : A))
assert Pconst : constseq s, from take i, rfl,
calc prodseq s = (s !zero) ^ succ n : prodseq_eq_pow_of_constseq s Pconst
... = (1 : A) ^ succ n : rfl
... = 1 : algebra.one_pow
... = 1 : one_pow
variable [deceqA : decidable_eq A]
include deceqA
@ -389,4 +389,4 @@ theorem first_sylow_theorem {p : nat} (Pp : prime p) :
end sylow
end group
end group_theory

17
library/theories/group_theory/subgroup.lean
View file

@ -9,8 +9,6 @@ open function eq.ops
open set
namespace algebra
namespace coset
-- semigroup coset definition
section
@ -54,19 +52,16 @@ definition rmul_by (a : A) := λ x, x * a
definition glcoset a (H : set A) : set A := λ x, H (a⁻¹ * x)
definition grcoset H (a : A) : set A := λ x, H (x * a⁻¹)
end
end algebra
namespace group
open algebra
namespace group_theory
namespace ops
infixr `∘>`:55 := glcoset -- stronger than = (50), weaker than * (70)
infixl `<∘`:55 := grcoset
infixr `∘c`:55 := conj_by
end ops
end group
end group_theory
namespace algebra
open group.ops
open group_theory.ops
section
variable {A : Type}
variable [s : group A]
@ -359,7 +354,7 @@ definition mk_quotient_group : group (coset_of N):=
end normal_subg
namespace group
namespace group_theory
namespace quotient
section
open quot
@ -376,6 +371,4 @@ definition natural (a : A) : coset_of N := ⟦a⟧
end
end quotient
end group
end algebra
end group_theory

15
library/theories/number_theory/bezout.lean
View file

@ -13,7 +13,6 @@ section Bezout
open nat int
open eq.ops well_founded decidable prod
open algebra
private definition pair_nat.lt : ℕ × ℕ → ℕ × ℕ → Prop := measure pr₂
private definition pair_nat.lt.wf : well_founded pair_nat.lt := intro_k (measure.wf pr₂) 20
@ -53,7 +52,7 @@ end
theorem egcd_prop (x y : ℕ) : (pr₁ (egcd x y)) * x + (pr₂ (egcd x y)) * y = gcd x y :=
gcd.induction x y
(take m, by krewrite [egcd_zero, algebra.mul_zero, algebra.one_mul])
(take m, by krewrite [egcd_zero, mul_zero, one_mul])
(take m n,
assume npos : 0 < n,
assume IH,
@ -62,13 +61,13 @@ gcd.induction x y
rewrite H,
esimp,
rewrite [gcd_rec, -IH],
rewrite [algebra.add.comm],
rewrite [add.comm],
rewrite [-of_nat_mod],
rewrite [int.mod_def],
rewrite [+algebra.mul_sub_right_distrib],
rewrite [+algebra.mul_sub_left_distrib, *left_distrib],
rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m % n)) * of_nat m + - _}algebra.add.comm],
rewrite [-algebra.add.assoc ,algebra.mul.assoc]
rewrite [+mul_sub_right_distrib],
rewrite [+mul_sub_left_distrib, *left_distrib],
rewrite [*sub_eq_add_neg, {pr₂ (egcd n (m % n)) * of_nat m + - _}add.comm],
rewrite [-add.assoc, mul.assoc]
end)
theorem Bezout_aux (x y : ℕ) : ∃ a b : ℤ, a * x + b * y = gcd x y :=
@ -90,7 +89,7 @@ implies prime (dvd_or_dvd_of_prime_of_dvd_mul).
-/
namespace nat
open int algebra
open int
example {p x y : ℕ} (pp : prime p) (H : p ∣ x * y) : p ∣ x ∨ p ∣ y :=
decidable.by_cases

9
library/theories/number_theory/irrational_roots.lean
View file

@ -7,7 +7,6 @@ A proof that if n > 1 and a > 0, then the nth root of a is irrational, unless a
-/
import data.rat .prime_factorization
open eq.ops
open algebra
/- First, a textbook proof that sqrt 2 is irrational. -/
@ -23,7 +22,7 @@ section
obtain (c : nat) (aeq : a = 2 * c),
from exists_of_even this,
have 2 * (2 * c^2) = 2 * b^2,
by rewrite [-H, aeq, *pow_two, algebra.mul.assoc, algebra.mul.left_comm c],
by rewrite [-H, aeq, *pow_two, mul.assoc, mul.left_comm c],
have 2 * c^2 = b^2,
from eq_of_mul_eq_mul_left dec_trivial this,
have even (b^2),
@ -99,9 +98,9 @@ section
have bnz : b ≠ (0 : ℚ),
from assume H, `b ≠ 0` (of_int.inj H),
have bnnz : ((b : rat)^n ≠ 0),
from assume bneqz, bnz (algebra.eq_zero_of_pow_eq_zero bneqz),
from assume bneqz, bnz (eq_zero_of_pow_eq_zero bneqz),
have a^n /[rat] b^n = c,
using bnz, begin rewrite [*of_int_pow, -algebra.div_pow, -eq_num_div_denom, -H] end,
using bnz, begin rewrite [*of_int_pow, -div_pow, -eq_num_div_denom, -H] end,
have (a^n : rat) = c *[rat] b^n,
from eq.symm (!mul_eq_of_eq_div bnnz this⁻¹),
have a^n = c * b^n, -- int version
@ -123,7 +122,7 @@ section
have ane0 : a ≠ 0, from
suppose aeq0 : a = 0,
have qeq0 : q = 0,
by rewrite [eq_num_div_denom, aeq0, of_int_zero, algebra.zero_div],
by rewrite [eq_num_div_denom, aeq0, of_int_zero, zero_div],
show false,
from qne0 qeq0,
have nat_abs a ≠ 0, from

6
library/theories/number_theory/prime_factorization.lean
View file

@ -9,12 +9,10 @@ Multiplicity and prime factors. We have:
prime_factors n := the finite set of prime factors of n, assuming n > 0
-/
import data.nat data.finset .primes
open eq.ops finset well_founded decidable nat.finset
open algebra
import data.nat data.finset .primes algebra.group_set_bigops
open eq.ops finset well_founded decidable
namespace nat
-- TODO: this should be proved more generally in ring_bigops
theorem Prod_pos {A : Type} [deceqA : decidable_eq A]
{s : finset A} {f : A → ℕ} (fpos : ∀ n, n ∈ s → f n > 0) :

2
library/theories/number_theory/primes.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
Prime numbers.
-/
import data.nat logic.identities
open bool algebra
open bool
namespace nat
open decidable