Merge branch 'master' of https://github.com/leanprover/mathlib

algebra/field.lean

@@ -50,6 +50,20 @@ calc (λx, x * c) '' {r | a ≤ r ∧ r ≤ b } = (λx, x / c) ⁻¹' {r | a ≤
   ... = {r | a * c ≤ r ∧ r ≤ b * c} :
     set.ext $ by simp [le_div_iff_mul_le_of_pos, div_le_iff_le_mul_of_pos, hc]
 
+instance linear_ordered_field.to_densely_ordered [linear_ordered_field α] : densely_ordered α :=
+{ dense := assume a₁ a₂ h, ⟨(a₁ + a₂) / 2,
+  calc a₁ = (a₁ + a₁) / 2 : (add_self_div_two a₁).symm
+    ... < (a₁ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_left h _) two_pos,
+  calc (a₁ + a₂) / 2 < (a₂ + a₂) / 2 : div_lt_div_of_lt_of_pos (add_lt_add_right h _) two_pos
+    ... = a₂ : add_self_div_two a₂⟩ }
+
+instance linear_ordered_field.to_no_top_order [linear_ordered_field α] : no_top_order α :=
+{ no_top := assume a, ⟨a + 1, lt_add_of_le_of_pos (le_refl a) zero_lt_one ⟩ }
+
+instance linear_ordered_field.to_no_bot_order [linear_ordered_field α] : no_bot_order α :=
+{ no_bot := assume a, ⟨a + -1,
+    add_lt_of_le_of_neg (le_refl _) (neg_lt_of_neg_lt $ by simp [zero_lt_one]) ⟩ }
+
 end
 
 section

algebra/group.lean

@@ -42,18 +42,93 @@ section group
 end group
 
 /- transport versions to additive -/
-run_cmd transport_multiplicative_to_additive
-  [  (`left_inverse_inv, `left_inverse_neg),
-     (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
-     (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
-     (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
-     (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
-     (`mul_right_inv, `add_right_inv),
-     (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
-     (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
-     (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg)
-     -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
-     -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
+run_cmd transport_multiplicative_to_additive [
+  /- map operations -/
+  (`has_mul.mul, `has_add.add), (`has_one.one, `has_zero.zero), (`has_inv.inv, `has_neg.neg),
+  (`has_mul, `has_add), (`has_one, `has_zero), (`has_inv, `has_neg),
+  /- map constructors -/
+  (`has_mul.mk, `has_add.mk), (`has_one, `has_zero.mk), (`has_inv, `has_neg.mk),
+  /- map structures -/
+  (`semigroup, `add_semigroup),
+  (`monoid, `add_monoid),
+  (`group, `add_group),
+  (`comm_semigroup, `add_comm_semigroup),
+  (`comm_monoid, `add_comm_monoid),
+  (`comm_group, `add_comm_group),
+  (`left_cancel_semigroup, `add_left_cancel_semigroup),
+  (`right_cancel_semigroup, `add_right_cancel_semigroup),
+  (`left_cancel_semigroup.mk, `add_left_cancel_semigroup.mk),
+  (`right_cancel_semigroup.mk, `add_right_cancel_semigroup.mk),
+  /- map instances -/
+  (`semigroup.to_has_mul, `add_semigroup.to_has_add),
+  (`monoid.to_has_one, `add_monoid.to_has_zero),
+  (`group.to_has_inv, `add_group.to_has_neg),
+  (`comm_semigroup.to_semigroup, `add_comm_semigroup.to_add_semigroup),
+  (`monoid.to_semigroup, `add_monoid.to_add_semigroup),
+  (`comm_monoid.to_monoid, `add_comm_monoid.to_add_monoid),
+  (`comm_monoid.to_comm_semigroup, `add_comm_monoid.to_add_comm_semigroup),
+  (`group.to_monoid, `add_group.to_add_monoid),
+  (`comm_group.to_group, `add_comm_group.to_add_group),
+  (`comm_group.to_comm_monoid, `add_comm_group.to_add_comm_monoid),
+  (`left_cancel_semigroup.to_semigroup, `add_left_cancel_semigroup.to_add_semigroup),
+  (`right_cancel_semigroup.to_semigroup, `add_right_cancel_semigroup.to_add_semigroup),
+  /- map projections -/
+  (`semigroup.mul_assoc, `add_semigroup.add_assoc),
+  (`comm_semigroup.mul_comm, `add_comm_semigroup.add_comm),
+  (`left_cancel_semigroup.mul_left_cancel, `add_left_cancel_semigroup.add_left_cancel),
+  (`right_cancel_semigroup.mul_right_cancel, `add_right_cancel_semigroup.add_right_cancel),
+  (`monoid.one_mul, `add_monoid.zero_add),
+  (`monoid.mul_one, `add_monoid.add_zero),
+  (`group.mul_left_inv, `add_group.add_left_neg),
+  (`group.mul, `add_group.add),
+  (`group.mul_assoc, `add_group.add_assoc),
+  /- map lemmas -/
+  (`mul_assoc, `add_assoc),
+  (`mul_comm, `add_comm),
+  (`mul_left_comm, `add_left_comm),
+  (`mul_right_comm, `add_right_comm),
+  (`one_mul, `zero_add),
+  (`mul_one, `add_zero),
+  (`mul_left_inv, `add_left_neg),
+  (`mul_left_cancel, `add_left_cancel),
+  (`mul_right_cancel, `add_right_cancel),
+  (`mul_left_cancel_iff, `add_left_cancel_iff),
+  (`mul_right_cancel_iff, `add_right_cancel_iff),
+  (`inv_mul_cancel_left, `neg_add_cancel_left),
+  (`inv_mul_cancel_right, `neg_add_cancel_right),
+  (`eq_inv_mul_of_mul_eq, `eq_neg_add_of_add_eq),
+  (`inv_eq_of_mul_eq_one, `neg_eq_of_add_eq_zero),
+  (`inv_inv, `neg_neg),
+  (`mul_right_inv, `add_right_neg),
+  (`mul_inv_cancel_left, `add_neg_cancel_left),
+  (`mul_inv_cancel_right, `add_neg_cancel_right),
+  (`mul_inv_rev, `neg_add_rev),
+  (`mul_inv, `neg_add),
+  (`inv_inj, `neg_inj),
+  (`group.mul_left_cancel, `add_group.add_left_cancel),
+  (`group.mul_right_cancel, `add_group.add_right_cancel),
+  (`group.to_left_cancel_semigroup, `add_group.to_left_cancel_add_semigroup),
+  (`group.to_right_cancel_semigroup, `add_group.to_right_cancel_add_semigroup),
+  (`eq_inv_of_eq_inv, `eq_neg_of_eq_neg),
+  (`eq_inv_of_mul_eq_one, `eq_neg_of_add_eq_zero),
+  (`eq_mul_inv_of_mul_eq, `eq_add_neg_of_add_eq),
+  (`inv_mul_eq_of_eq_mul, `neg_add_eq_of_eq_add),
+  (`mul_inv_eq_of_eq_mul, `add_neg_eq_of_eq_add),
+  (`eq_mul_of_mul_inv_eq, `eq_add_of_add_neg_eq),
+  (`eq_mul_of_inv_mul_eq, `eq_add_of_neg_add_eq),
+  (`mul_eq_of_eq_inv_mul, `add_eq_of_eq_neg_add),
+  (`mul_eq_of_eq_mul_inv, `add_eq_of_eq_add_neg),
+  (`one_inv, `neg_zero),
+  (`left_inverse_inv, `left_inverse_neg),
+  (`inv_eq_inv_iff_eq, `neg_eq_neg_iff_eq),
+  (`inv_eq_one_iff_eq_one, `neg_eq_zero_iff_eq_zero),
+  (`eq_one_of_inv_eq_one, `eq_zero_of_neg_eq_zero),
+  (`eq_inv_iff_eq_inv, `eq_neg_iff_eq_neg),
+  (`eq_of_mul_inv_eq_one, `eq_of_add_neg_eq_zero),
+  (`mul_eq_iff_eq_inv_mul, `add_eq_iff_eq_neg_add),
+  (`mul_eq_iff_eq_mul_inv, `add_eq_iff_eq_add_neg)
+  -- (`mul_eq_one_of_mul_eq_one, `add_eq_zero_of_add_eq_zero)   not needed for commutative groups
+  -- (`muleq_one_iff_mul_eq_one, `add_eq_zero_iff_add_eq_zero)
   ]
 
 section add_group
@@ -109,6 +184,9 @@ lemma abs_le_iff  : abs a ≤ b ↔ (- b ≤ a ∧ a ≤ b) :=
 ⟨assume h, ⟨neg_le_of_neg_le $ le_trans (neg_le_abs_self _) h, le_trans (le_abs_self _) h⟩,
   assume ⟨h₁, h₂⟩, abs_le_of_le_of_neg_le h₂ $ neg_le_of_neg_le h₁⟩
 
+@[simp] lemma abs_eq_zero_iff : abs a = 0 ↔ a = 0 :=
+⟨eq_zero_of_abs_eq_zero, by simp [abs_zero] {contextual := tt}⟩
+
 end decidable_linear_ordered_comm_group
 
 /-

algebra/module.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2015 Nathaniel Thomas. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nathaniel Thomas, Jeremy Avigad
+
+Modules and vector spaces over a ring.
+-/
+import algebra.field
+
+universes u v
+
+class has_scalar (α : inout Type u) (γ : Type v) := (smul : α → γ → γ)
+
+infixl ` • `:73 := has_scalar.smul
+
+/- modules over a ring -/
+
+class module (α : inout Type u) (β : Type v) [ring α] extends has_scalar α β, add_comm_group β :=
+(smul_left_distrib  : ∀r (x y : β), r • (x + y) = r • x + r • y)
+(smul_right_distrib : ∀r s (x : β), (r + s) • x = r • x + s • x)
+(mul_smul           : ∀r s (x : β), (r * s) • x = r • (s • x))
+(one_smul           : ∀x : β, (1 : α) • x = x)
+
+section module
+variables {α : Type u} {β : Type v} [ring α] [module α β]
+variables {a b c : α} {u v w : β}
+
+theorem smul_left_distrib : a • (u + v) = a • u + a • v := module.smul_left_distrib a u v
+theorem smul_right_distrib : (a + b) • u = a • u + b • u := module.smul_right_distrib a b u
+theorem mul_smul : (a * b) • u = a • (b • u) :=  module.mul_smul a b u
+@[simp] theorem one_smul : (1 : α) • u = u := module.one_smul _ u
+
+@[simp] theorem zero_smul : (0 : α) • u = 0 :=
+have (0 : α) • u + 0 • u = 0 • u + 0, by rewrite [←smul_right_distrib]; simp,
+add_left_cancel this
+
+@[simp] theorem smul_zero : a • (0 : β) = 0 :=
+have a • (0:β) + a • 0 = a • 0 + 0, by rewrite [←smul_left_distrib]; simp,
+add_left_cancel this
+
+@[simp] theorem neg_smul : (-a) • u = - (a • u) :=
+eq_neg_of_add_eq_zero (by rewrite [←smul_right_distrib, add_left_neg, zero_smul])
+
+@[simp] theorem smul_neg : a • (-u) = -(a • u) :=
+calc a • (-u) = a • (-(1 • u)) : by simp
+  ... = (a * -1) • u : by rw [←neg_smul, mul_smul]; simp
+  ... = -(a • u) : by rw [mul_neg_eq_neg_mul_symm]; simp
+
+theorem smul_sub_left_distrib (a : α) (u v : β) : a • (u - v) = a • u - a • v :=
+by simp [smul_left_distrib]
+
+theorem sub_smul_right_distrib (a b : α) (v : β) : (a - b) • v = a • v - b • v :=
+by simp [smul_right_distrib]
+
+end module
+
+def ring.to_module {α : Type u} [r : ring α] : module α α :=
+{ r with
+  smul := λa b, a * b,
+  smul_left_distrib := assume a b c, mul_add _ _ _,
+  smul_right_distrib := assume a b c, add_mul _ _ _,
+  mul_smul := assume a b c, mul_assoc _ _ _,
+  one_smul := assume a, one_mul _ }
+
+/- vector spaces -/
+
+class vector_space (α : inout Type u)  (β : Type v) [field α] extends module α β

data/fp/basic.lean

@@ -183,7 +183,7 @@ namespace float
 
 variable [S : fpsettings]
 
-def default_nan : float := nan (fpsettings.default_nan C)
+def default_nan : float := nan fpsettings.default_nan
 
 instance : has_neg float := ⟨float.neg⟩
 

data/rat.lean

@@ -6,7 +6,7 @@ Authors: Johannes Hölzl
 Introduces the rational numbers as discrete, linear ordered field.
 -/
 
-import data.nat.gcd data.pnat data.int.basic pending
+import data.nat.gcd data.pnat data.int.basic order.basic pending
 
 /- linorder -/
 

order/basic.lean

@@ -111,3 +111,45 @@ theorem monotone_app (f : β → α → γ) (b : β) (m : monotone (λa b, f b a
 assume a a' h, m h b
 
 end monotone
+
+/- additional order classes -/
+
+/-- order without a top element; somtimes called cofinal -/
+class no_top_order (α : Type u) [preorder α] : Prop :=
+(no_top : ∀a:α, ∃a', a < a')
+
+lemma no_top [preorder α] [no_top_order α] : ∀a:α, ∃a', a < a' :=
+no_top_order.no_top
+
+/-- order without a bottom element; somtimes called coinitial or dense -/
+class no_bot_order (α : Type u) [preorder α] : Prop :=
+(no_bot : ∀a:α, ∃a', a' < a)
+
+lemma no_bot [preorder α] [no_bot_order α] : ∀a:α, ∃a', a' < a :=
+no_bot_order.no_bot
+
+class densely_ordered (α : Type u) [preorder α] : Prop :=
+(dense : ∀a₁ a₂:α, a₁ < a₂ → ∃a, a₁ < a ∧ a < a₂)
+
+lemma dense [preorder α] [densely_ordered α] : ∀{a₁ a₂:α}, a₁ < a₂ → ∃a, a₁ < a ∧ a < a₂ :=
+densely_ordered.dense
+
+lemma le_of_forall_le [linear_order α] [densely_ordered α] {a₁ a₂ : α} (h : ∀a₃>a₂, a₁ ≤ a₃) :
+  a₁ ≤ a₂ :=
+le_of_not_gt $ assume ha,
+  let ⟨a, ha₁, ha₂⟩ := dense ha in
+  lt_irrefl a $ lt_of_lt_of_le ‹a < a₁› (h _ ‹a₂ < a›)
+
+lemma eq_of_le_of_forall_le [linear_order α] [densely_ordered α] {a₁ a₂ : α}
+  (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃>a₂, a₁ ≤ a₃) : a₁ = a₂ :=
+le_antisymm (le_of_forall_le h₂) h₁
+
+lemma le_of_forall_ge [linear_order α] [densely_ordered α] {a₁ a₂ : α}(h : ∀a₃<a₁, a₂ ≥ a₃) :
+  a₁ ≤ a₂ :=
+le_of_not_gt $ assume ha,
+  let ⟨a, ha₁, ha₂⟩ := dense ha in
+  lt_irrefl a $ lt_of_le_of_lt (h _ ‹a < a₁›) ‹a₂ < a›
+
+lemma eq_of_le_of_forall_ge [linear_order α] [densely_ordered α] {a₁ a₂ : α}
+  (h₁ : a₂ ≤ a₁) (h₂ : ∀a₃<a₁, a₂ ≥ a₃) : a₁ = a₂ :=
+le_antisymm (le_of_forall_ge h₂) h₁

order/complete_lattice.lean

@@ -286,12 +286,6 @@ le_antisymm
 
 attribute [ematch] le_refl
 
-@[ematch] theorem foo {a b : α} (h : a = b) : a ≤ b :=
-by rw h; apply le_refl
-
-@[ematch] theorem foo' {a b : α} (h : b = a) : a ≤ b :=
-by rw h; apply le_refl
-
 theorem infi_inf_eq {f g : β → α} : (⨅ x, f x ⊓ g x) = (⨅ x, f x) ⊓ (⨅ x, g x) :=
 le_antisymm
   (le_inf
@@ -310,6 +304,14 @@ begin
 end
 -/
 
+lemma infi_inf {f : ι → α} {a : α} (i : ι) : (⨅x, f x) ⊓ a = (⨅ x, f x ⊓ a) :=
+le_antisymm
+  (le_infi $ assume i, le_inf (inf_le_left_of_le $ infi_le _ _) inf_le_right)
+  (le_inf (infi_le_infi $ assume i, inf_le_left) (infi_le_of_le i inf_le_right))
+
+lemma inf_infi {f : ι → α} {a : α} (i : ι) : a ⊓ (⨅x, f x) = (⨅ x, a ⊓ f x) :=
+by rw [inf_comm, infi_inf i]; simp [inf_comm]
+
 theorem supr_sup_eq {f g : β → α} : (⨆ x, f x ⊔ g x) = (⨆ x, f x) ⊔ (⨆ x, g x) :=
 le_antisymm
   (supr_le $ assume i, sup_le

order/filter.lean

@@ -726,6 +726,18 @@ lemma tendsto_inf {f : α → β} {x : filter α} {y₁ y₂ : filter β}
   (h₁ : tendsto f x y₁) (h₂ : tendsto f x y₂) : tendsto f x (y₁ ⊓ y₂) :=
 le_inf h₁ h₂
 
+lemma tendsto_infi {f : α → β} {x : filter α} {y : ι → filter β}
+  (h : ∀i, tendsto f x (y i)) : tendsto f x (⨅i, y i) :=
+le_infi h
+
+lemma tendsto_infi' {f : α → β} {x : ι → filter α} {y : filter β} (i : ι)
+  (h : tendsto f (x i) y) : tendsto f (⨅i, x i) y :=
+le_trans (map_mono $ infi_le _ _) h
+
+lemma tendsto_principal_principal {f : α → β} {s : set α} {t : set β}
+  (h : ∀a∈s, f a ∈ t) : tendsto f (principal s) (principal t) :=
+by simp [tendsto, image_subset_iff_subset_preimage]; exact h
+
 section lift
 
 protected def lift (f : filter α) (g : set α → filter β) :=
@@ -1016,21 +1028,21 @@ by simp [filter.prod, mem_inf_sets, mem_vmap];
 -/
 
 section prod
+variables {s : set α} {t : set β} {f : filter α} {g : filter β}
 
 protected def prod (f : filter α) (g : filter β) : filter (α × β) :=
 f.lift $ λs, g.lift' $ λt, set.prod s t
 
-lemma prod_mem_prod {s : set α} {t : set β} {f : filter α} {g : filter β}
-  (hs : s ∈ f.sets) (ht : t ∈ g.sets) : set.prod s t ∈ (filter.prod f g).sets :=
+lemma prod_mem_prod (hs : s ∈ f.sets) (ht : t ∈ g.sets) : set.prod s t ∈ (filter.prod f g).sets :=
 le_principal_iff.mp $ show filter.prod f g ≤ principal (set.prod s t),
   from infi_le_of_le s $ infi_le_of_le hs $ infi_le_of_le t $ infi_le _ ht
 
-lemma prod_same_eq {f : filter α} : filter.prod f f = f.lift' (λt, set.prod t t) :=
+lemma prod_same_eq : filter.prod f f = f.lift' (λt, set.prod t t) :=
 lift_lift'_same_eq_lift'
   (assume s, set.monotone_prod monotone_const monotone_id)
   (assume t, set.monotone_prod monotone_id monotone_const)
 
-lemma mem_prod_iff {s : set (α×β)} {f : filter α} {g : filter β} :
+lemma mem_prod_iff {s : set (α×β)} :
   s ∈ (filter.prod f g).sets ↔ (∃t₁∈f.sets, ∃t₂∈g.sets, set.prod t₁ t₂ ⊆ s) :=
 begin
   delta filter.prod,
@@ -1042,16 +1054,33 @@ begin
   exact (monotone_lift' monotone_const $ monotone_lam $ assume b, set.monotone_prod monotone_id monotone_const)
 end
 
-lemma mem_prod_same_iff {s : set (α×α)} {f : filter α} :
+lemma prod_def : filter.prod f g = f.vmap prod.fst ⊓ g.vmap prod.snd :=
+filter_eq $ set.ext $ assume s,
+  begin
+    simp [mem_prod_iff, mem_inf_sets],
+    exact ⟨assume ⟨t₁, ht₁, t₂, ht₂, h⟩,
+        ⟨prod.fst ⁻¹' t₁, ⟨t₁, ht₁, subset.refl _⟩, prod.snd ⁻¹' t₂, h, ⟨t₂, ht₂, subset.refl _⟩⟩,
+      assume ⟨t₁, ⟨s₁, hs₁, hts₁⟩, t₂, h, ⟨s₂, hs₂, hts₂⟩⟩,
+      ⟨s₁, hs₁, s₂, hs₂, subset.trans (inter_subset_inter hts₁ hts₂) h⟩⟩
+  end
+
+lemma prod_infi_left {f : ι → filter α} {g : filter β} (i : ι) :
+  filter.prod (⨅i, f i) g = (⨅i, filter.prod (f i) g) :=
+by rw [prod_def, vmap_infi, infi_inf i]; simp [prod_def]
+
+lemma prod_infi_right {f : filter α} {g : ι → filter β} (i : ι) :
+  filter.prod f (⨅i, g i) = (⨅i, filter.prod f (g i)) :=
+by rw [prod_def, vmap_infi, inf_infi i]; simp [prod_def]
+
+lemma mem_prod_same_iff {s : set (α×α)} :
   s ∈ (filter.prod f f).sets ↔ (∃t∈f.sets, set.prod t t ⊆ s) :=
 by rw [prod_same_eq, mem_lift'_iff]; exact set.monotone_prod monotone_id monotone_id
 
 lemma prod_mono {f₁ f₂ : filter α} {g₁ g₂ : filter β} (hf : f₁ ≤ f₂) (hg : g₁ ≤ g₂) :
   filter.prod f₁ g₁ ≤ filter.prod f₂ g₂ :=
 lift_mono hf $ assume s, lift'_mono hg $ le_refl _
 
-lemma prod_comm {f : filter α} {g : filter β} :
-  filter.prod f g = map (λp:β×α, (p.2, p.1)) (filter.prod g f) :=
+lemma prod_comm : filter.prod f g = map (λp:β×α, (p.2, p.1)) (filter.prod g f) :=
 eq.symm $ calc map (λp:β×α, (p.2, p.1)) (filter.prod g f) =
         (g.lift $ λt, map (λp:β×α, (p.2, p.1)) (f.lift' $ λs, set.prod t s)) :
     map_lift_eq $ assume a b h, lift'_mono (le_refl f) (assume t, set.prod_mono h (subset.refl t))