diff --git a/library/algebra/bundled.lean b/library/algebra/bundled.lean index 94efaa25fc..540a3f2b1a 100644 --- a/library/algebra/bundled.lean +++ b/library/algebra/bundled.lean @@ -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 diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean index 82f321b37c..d4ddbf07f6 100644 --- a/library/algebra/complete_lattice.lean +++ b/library/algebra/complete_lattice.lean @@ -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 diff --git a/library/algebra/field.lean b/library/algebra/field.lean index df47d3dff7..288b6da616 100644 --- a/library/algebra/field.lean +++ b/library/algebra/field.lean @@ -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 := diff --git a/library/algebra/group.lean b/library/algebra/group.lean index 05154e4a9b..60769bd90d 100644 --- a/library/algebra/group.lean +++ b/library/algebra/group.lean @@ -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 diff --git a/library/algebra/group_bigops.lean b/library/algebra/group_bigops.lean index 41f0222359..ea04e14aa7 100644 --- a/library/algebra/group_bigops.lean +++ b/library/algebra/group_bigops.lean @@ -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 diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean index d89d688ba6..6b11d96277 100644 --- a/library/algebra/group_power.lean +++ b/library/algebra/group_power.lean @@ -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 diff --git a/library/algebra/group_set_bigops.lean b/library/algebra/group_set_bigops.lean index cc5da4260c..6f836df0c5 100644 --- a/library/algebra/group_set_bigops.lean +++ b/library/algebra/group_set_bigops.lean @@ -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 diff --git a/library/algebra/lattice.lean b/library/algebra/lattice.lean index 30f70f78e7..c01980753f 100644 --- a/library/algebra/lattice.lean +++ b/library/algebra/lattice.lean @@ -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 diff --git a/library/algebra/order.lean b/library/algebra/order.lean index d5bd3b91ee..f9f8e9d05d 100644 --- a/library/algebra/order.lean +++ b/library/algebra/order.lean @@ -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 diff --git a/library/algebra/ordered_field.lean b/library/algebra/ordered_field.lean index ce1f099a75..b7f4fae5e7 100644 --- a/library/algebra/ordered_field.lean +++ b/library/algebra/ordered_field.lean @@ -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 diff --git a/library/algebra/ordered_group.lean b/library/algebra/ordered_group.lean index c900ebea22..2c9576b6a8 100644 --- a/library/algebra/ordered_group.lean +++ b/library/algebra/ordered_group.lean @@ -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 diff --git a/library/algebra/ordered_ring.lean b/library/algebra/ordered_ring.lean index 5255670588..31cb32f1a2 100644 --- a/library/algebra/ordered_ring.lean +++ b/library/algebra/ordered_ring.lean @@ -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 diff --git a/library/algebra/priority.lean b/library/algebra/priority.lean index 6c3145e611..aa2ac4c5c8 100644 --- a/library/algebra/priority.lean +++ b/library/algebra/priority.lean @@ -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 diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index 2ac0ad36b8..89c99a82ff 100644 --- a/library/algebra/ring.lean +++ b/library/algebra/ring.lean @@ -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 diff --git a/library/algebra/ring_power.lean b/library/algebra/ring_power.lean index 16ae88cfe4..20e4a77e82 100644 --- a/library/algebra/ring_power.lean +++ b/library/algebra/ring_power.lean @@ -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 diff --git a/library/data/bag.lean b/library/data/bag.lean index 0bbfa3a3a3..e3a6fa5b46 100644 --- a/library/data/bag.lean +++ b/library/data/bag.lean @@ -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} diff --git a/library/data/bv.lean b/library/data/bv.lean index 4c6c1ccb53..2907beb2f7 100644 --- a/library/data/bv.lean +++ b/library/data/bv.lean @@ -11,7 +11,6 @@ import data.list import data.tuple namespace bv -open algebra open bool open eq.ops open list diff --git a/library/data/complex.lean b/library/data/complex.lean index 1531dbb27d..4915440410 100644 --- a/library/data/complex.lean +++ b/library/data/complex.lean @@ -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, diff --git a/library/data/encodable.lean b/library/data/encodable.lean index 319fba650c..c3f3101734 100644 --- a/library/data/encodable.lean +++ b/library/data/encodable.lean @@ -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) diff --git a/library/data/examples/vector.lean b/library/data/examples/vector.lean index b6d04a300b..6f7ef484aa 100644 --- a/library/data/examples/vector.lean +++ b/library/data/examples/vector.lean @@ -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 diff --git a/library/data/fin.lean b/library/data/fin.lean index b64a1772f8..5830042b91 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -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 diff --git a/library/data/finset/bigops.lean b/library/data/finset/bigops.lean index 14845f8308..51407a0d57 100644 --- a/library/data/finset/bigops.lean +++ b/library/data/finset/bigops.lean @@ -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) : diff --git a/library/data/finset/card.lean b/library/data/finset/card.lean index a30964e302..b716b61420 100644 --- a/library/data/finset/card.lean +++ b/library/data/finset/card.lean @@ -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 diff --git a/library/data/finset/equiv.lean b/library/data/finset/equiv.lean index 107a30f93d..27a7d6caa9 100644 --- a/library/data/finset/equiv.lean +++ b/library/data/finset/equiv.lean @@ -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) diff --git a/library/data/finset/partition.lean b/library/data/finset/partition.lean index 49de48afb7..34326a7b5b 100644 --- a/library/data/finset/partition.lean +++ b/library/data/finset/partition.lean @@ -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 diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean index 8b5d97e2b6..a0d5cf923f 100644 --- a/library/data/fintype/function.lean +++ b/library/data/fintype/function.lean @@ -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 diff --git a/library/data/hf.lean b/library/data/hf.lean index bd02c4d57b..d92e3f50da 100644 --- a/library/data/hf.lean +++ b/library/data/hf.lean @@ -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 diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index af13ee87e7..edbfc1ef16 100644 --- a/library/data/int/basic.lean +++ b/library/data/int/basic.lean @@ -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 diff --git a/library/data/int/bigops.lean b/library/data/int/bigops.lean deleted file mode 100644 index 8f830733a5..0000000000 --- a/library/data/int/bigops.lean +++ /dev/null @@ -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 diff --git a/library/data/int/default.lean b/library/data/int/default.lean index 5e3478af4e..c71c4f767e 100644 --- a/library/data/int/default.lean +++ b/library/data/int/default.lean @@ -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 diff --git a/library/data/int/div.lean b/library/data/int/div.lean index f7185ec7bd..f03705334a 100644 --- a/library/data/int/div.lean +++ b/library/data/int/div.lean @@ -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) diff --git a/library/data/int/gcd.lean b/library/data/int/gcd.lean index f694188a6b..44d63ee3ba 100644 --- a/library/data/int/gcd.lean +++ b/library/data/int/gcd.lean @@ -7,7 +7,6 @@ Definitions and properties of gcd, lcm, and coprime. -/ import .div data.nat.gcd open eq.ops -open algebra namespace int diff --git a/library/data/int/order.lean b/library/data/int/order.lean index e88f5c4a8c..8c623d7c8e 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -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, diff --git a/library/data/int/power.lean b/library/data/int/power.lean index f461849c0d..a97d654611 100644 --- a/library/data/int/power.lean +++ b/library/data/int/power.lean @@ -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 diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index d0237c31a0..1ce63e2298 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -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 diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index 45bef1e927..6aaf24d027 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -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} diff --git a/library/data/list/sort.lean b/library/data/list/sort.lean index c41838c026..3f3708490f 100644 --- a/library/data/list/sort.lean +++ b/library/data/list/sort.lean @@ -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 diff --git a/library/data/matrix.lean b/library/data/matrix.lean index d8910f0dbd..acb4bfb604 100644 --- a/library/data/matrix.lean +++ b/library/data/matrix.lean @@ -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 diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index aa8dfc02b6..48d18fd197 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -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, diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean deleted file mode 100644 index 5dd70a54e0..0000000000 --- a/library/data/nat/bigops.lean +++ /dev/null @@ -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 diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index b7d58b627e..200347eb07 100644 --- a/library/data/nat/div.lean +++ b/library/data/nat/div.lean @@ -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 diff --git a/library/data/nat/examples/fib2.lean b/library/data/nat/examples/fib2.lean index f49002324e..2ff8e444f0 100644 --- a/library/data/nat/examples/fib2.lean +++ b/library/data/nat/examples/fib2.lean @@ -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 diff --git a/library/data/nat/examples/partial_sum.lean b/library/data/nat/examples/partial_sum.lean index f507936863..5e697b95d4 100644 --- a/library/data/nat/examples/partial_sum.lean +++ b/library/data/nat/examples/partial_sum.lean @@ -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 diff --git a/library/data/nat/fact.lean b/library/data/nat/fact.lean index c915f7f456..9b56fd0e83 100644 --- a/library/data/nat/fact.lean +++ b/library/data/nat/fact.lean @@ -6,7 +6,6 @@ Authors: Leonardo de Moura Factorial -/ import data.nat.div -open algebra namespace nat definition fact : nat → nat diff --git a/library/data/nat/find.lean b/library/data/nat/find.lean index 782840b013..bba8d29a59 100644 --- a/library/data/nat/find.lean +++ b/library/data/nat/find.lean @@ -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 diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean index 422ec7f2db..c3470b9095 100644 --- a/library/data/nat/gcd.lean +++ b/library/data/nat/gcd.lean @@ -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 diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean index 6a0776fdc5..2fdce70a94 100644 --- a/library/data/nat/order.lean +++ b/library/data/nat/order.lean @@ -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 diff --git a/library/data/nat/pairing.lean b/library/data/nat/pairing.lean index 5befe9ef77..3af9a1d591 100644 --- a/library/data/nat/pairing.lean +++ b/library/data/nat/pairing.lean @@ -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) diff --git a/library/data/nat/parity.lean b/library/data/nat/parity.lean index 5ad13ab715..1c2a1d17eb 100644 --- a/library/data/nat/parity.lean +++ b/library/data/nat/parity.lean @@ -9,7 +9,6 @@ import data.nat.power logic.identities namespace nat open decidable -open algebra definition even (n : nat) := n % 2 = 0 diff --git a/library/data/nat/power.lean b/library/data/nat/power.lean index 0526d5d6c6..f6b9bab287 100644 --- a/library/data/nat/power.lean +++ b/library/data/nat/power.lean @@ -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) diff --git a/library/data/nat/sqrt.lean b/library/data/nat/sqrt.lean index 4d35d6e6a4..18c5a3d057 100644 --- a/library/data/nat/sqrt.lean +++ b/library/data/nat/sqrt.lean @@ -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 diff --git a/library/data/nat/sub.lean b/library/data/nat/sub.lean index b74db85183..ec58eed201 100644 --- a/library/data/nat/sub.lean +++ b/library/data/nat/sub.lean @@ -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]) diff --git a/library/data/pnat.lean b/library/data/pnat.lean index f5da33dd90..8c90792bd4 100644 --- a/library/data/pnat.lean +++ b/library/data/pnat.lean @@ -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 diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean index bf9c2dab2d..837ab5afec 100644 --- a/library/data/rat/basic.lean +++ b/library/data/rat/basic.lean @@ -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 diff --git a/library/data/rat/bigops.lean b/library/data/rat/bigops.lean deleted file mode 100644 index 0ff99b7b50..0000000000 --- a/library/data/rat/bigops.lean +++ /dev/null @@ -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 diff --git a/library/data/rat/default.lean b/library/data/rat/default.lean index a9b26fa4b7..a9cb20ed7c 100644 --- a/library/data/rat/default.lean +++ b/library/data/rat/default.lean @@ -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 diff --git a/library/data/rat/order.lean b/library/data/rat/order.lean index ba8bd015b4..95c3cf8486 100644 --- a/library/data/rat/order.lean +++ b/library/data/rat/order.lean @@ -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) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 4acabb989e..039a79de77 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -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, diff --git a/library/data/real/bigops.lean b/library/data/real/bigops.lean deleted file mode 100644 index 10d6d3b66b..0000000000 --- a/library/data/real/bigops.lean +++ /dev/null @@ -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 diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index ccf9fefbfe..41759108e8 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -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 diff --git a/library/data/real/default.lean b/library/data/real/default.lean index 4567ee42ff..21e4a435fd 100644 --- a/library/data/real/default.lean +++ b/library/data/real/default.lean @@ -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 diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 0db408acc6..422421ebdf 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -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 ≤ ε) : diff --git a/library/data/real/order.lean b/library/data/real/order.lean index c37c025e7f..ba42173436 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -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, diff --git a/library/data/set/comm_semiring.lean b/library/data/set/comm_semiring.lean index 7d9345a2fe..c19f90914d 100644 --- a/library/data/set/comm_semiring.lean +++ b/library/data/set/comm_semiring.lean @@ -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, diff --git a/library/data/set/filter.lean b/library/data/set/filter.lean index a382f78bec..5e2fed02dc 100644 --- a/library/data/set/filter.lean +++ b/library/data/set/filter.lean @@ -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, diff --git a/library/data/stream.lean b/library/data/stream.lean index dbe66ed195..ca616b1ac2 100644 --- a/library/data/stream.lean +++ b/library/data/stream.lean @@ -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 diff --git a/library/data/tuple.lean b/library/data/tuple.lean index 8b4feae403..196ba8ac14 100644 --- a/library/data/tuple.lean +++ b/library/data/tuple.lean @@ -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} diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index e4568b1e91..3869ccfa7f 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -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 → ℝ) diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 8291755b8b..6697c7c199 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -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 diff --git a/library/theories/combinatorics/choose.lean b/library/theories/combinatorics/choose.lean index 2815ec80a6..c0c6c221f0 100644 --- a/library/theories/combinatorics/choose.lean +++ b/library/theories/combinatorics/choose.lean @@ -7,7 +7,6 @@ Binomial coefficients, "n choose k". -/ import data.nat.div data.nat.fact data.finset open decidable -open algebra namespace nat diff --git a/library/theories/group_theory/action.lean b/library/theories/group_theory/action.lean index 5985aada4c..36deaf31de 100644 --- a/library/theories/group_theory/action.lean +++ b/library/theories/group_theory/action.lean @@ -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 diff --git a/library/theories/group_theory/cyclic.lean b/library/theories/group_theory/cyclic.lean index 752dd8150b..9b490220fd 100644 --- a/library/theories/group_theory/cyclic.lean +++ b/library/theories/group_theory/cyclic.lean @@ -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 diff --git a/library/theories/group_theory/finsubg.lean b/library/theories/group_theory/finsubg.lean index 67dff70792..b7f480d2c1 100644 --- a/library/theories/group_theory/finsubg.lean +++ b/library/theories/group_theory/finsubg.lean @@ -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 diff --git a/library/theories/group_theory/hom.lean b/library/theories/group_theory/hom.lean index 4eba4563ee..4c5a919471 100644 --- a/library/theories/group_theory/hom.lean +++ b/library/theories/group_theory/hom.lean @@ -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 diff --git a/library/theories/group_theory/perm.lean b/library/theories/group_theory/perm.lean index b415bd686f..28c3703175 100644 --- a/library/theories/group_theory/perm.lean +++ b/library/theories/group_theory/perm.lean @@ -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 diff --git a/library/theories/group_theory/pgroup.lean b/library/theories/group_theory/pgroup.lean index ef02fdf529..ff15733291 100644 --- a/library/theories/group_theory/pgroup.lean +++ b/library/theories/group_theory/pgroup.lean @@ -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 diff --git a/library/theories/group_theory/subgroup.lean b/library/theories/group_theory/subgroup.lean index 2ff001b14b..553a8a4182 100644 --- a/library/theories/group_theory/subgroup.lean +++ b/library/theories/group_theory/subgroup.lean @@ -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 diff --git a/library/theories/number_theory/bezout.lean b/library/theories/number_theory/bezout.lean index dd7cf7385e..97f7974063 100644 --- a/library/theories/number_theory/bezout.lean +++ b/library/theories/number_theory/bezout.lean @@ -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 diff --git a/library/theories/number_theory/irrational_roots.lean b/library/theories/number_theory/irrational_roots.lean index 81c2268b9b..96082ba136 100644 --- a/library/theories/number_theory/irrational_roots.lean +++ b/library/theories/number_theory/irrational_roots.lean @@ -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 diff --git a/library/theories/number_theory/prime_factorization.lean b/library/theories/number_theory/prime_factorization.lean index e3385d71c3..93daba201f 100644 --- a/library/theories/number_theory/prime_factorization.lean +++ b/library/theories/number_theory/prime_factorization.lean @@ -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) : diff --git a/library/theories/number_theory/primes.lean b/library/theories/number_theory/primes.lean index 6bf2532858..ca2624ffd4 100644 --- a/library/theories/number_theory/primes.lean +++ b/library/theories/number_theory/primes.lean @@ -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