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

algebra/big_operators.lean

@@ -5,8 +5,8 @@ Authors: Johannes Hölzl
 
 Some big operators for lists and finite sets.
 -/
-import algebra.group data.list data.list.comb algebra.group_power data.set.finite data.finset
-  data.list.perm
+import data.list data.list.comb data.list.perm data.set.finite data.finset
+  algebra.group algebra.ordered_monoid algebra.group_power
 
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
@@ -75,6 +75,9 @@ fold_to_finset_of_nodup h
 @[simp] lemma prod_singleton : ({a}:finset α).prod f = f a :=
 eq.trans fold_singleton (by simp)
 
+@[simp] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
+s.induction_on (by simp) (by simp {contextual:=tt})
+
 @[simp] lemma prod_image [decidable_eq γ] {s : finset γ} {g : γ → α} :
   (∀x∈s, ∀y∈s, g x = g y → x = y) → (s.image g).prod f = s.prod (λx, f (g x)) :=
 fold_image
@@ -88,15 +91,58 @@ fold_union_inter
 lemma prod_union (h : s₁ ∩ s₂ = ∅) : (s₁ ∪ s₂).prod f = s₁.prod f * s₂.prod f :=
 by rw [←prod_union_inter, h]; simp
 
+lemma prod_bind [decidable_eq γ] {s : finset γ} {t : γ → finset α} :
+  (∀x∈s, ∀y∈s, x ≠ y → t x ∩ t y = ∅) → (s.bind t).prod f = s.prod (λx, (t x).prod f) :=
+s.induction_on (by simp) $
+  assume x s hxs ih hd,
+  have hd' : ∀x∈s, ∀y∈s, x ≠ y → t x ∩ t y = ∅,
+    from assume _ hx _ hy, hd _ (mem_insert_of_mem hx) _ (mem_insert_of_mem hy),
+  have t x ∩ finset.bind s t = ∅,
+    from ext $ assume a,
+      by simp [mem_bind_iff];
+      from assume h₁ y hys hy₂,
+      have ha : a ∈ t x ∩ t y, by simp [*],
+      have t x ∩ t y = ∅,
+        from hd _ mem_insert _ (mem_insert_of_mem hys) $ assume h, hxs $ h.symm ▸ hys,
+      by rwa [this] at ha,
+  by simp [hxs, prod_union this, ih hd'] {contextual := tt}
+
+lemma prod_product [decidable_eq γ] {s : finset γ} {t : finset α} {f : γ×α → β} :
+  (s.product t).prod f = (s.prod $ λx, t.prod $ λy, f (x, y)) :=
+calc (s.product t).prod f = (s.prod $ λx, (t.image $ λy, (x, y)).prod f) :
+    prod_bind $ assume x hx y hy h, ext $ by simp [mem_image_iff]; cc
+  ... = _ : begin congr, apply funext, intro x, apply prod_image, simp {contextual := tt} end
+
+lemma prod_sigma {σ : α → Type*} [∀a, decidable_eq (σ a)]
+  {s : finset α} {t : Πa, finset (σ a)} {f : sigma σ → β} :
+  (s.sigma t).prod f = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) :=
+have ∀a₁ a₂:α, ∀s₁ : finset (σ a₁), ∀s₂ : finset (σ a₂), a₁ ≠ a₂ →
+    s₁.image (sigma.mk a₁) ∩ s₂.image (sigma.mk a₂) = ∅,
+  from assume b₁ b₂ s₁ s₂ h, ext $ assume ⟨b₃, c₃⟩,
+    by simp [mem_image_iff, sigma.mk_eq_mk_iff, heq_iff_eq] {contextual := tt}; cc,
+calc (s.bind (λa, (t a).image (λs, sigma.mk a s))).prod f =
+      s.prod (λa, ((t a).image (λs, sigma.mk a s)).prod f) :
+    prod_bind $ assume a₁ ha a₂ ha₂ h, this a₁ a₂ (t a₁) (t a₂) h
+  ... = (s.prod $ λa, (t a).prod $ λs, f ⟨a, s⟩) :
+    by simp [prod_image, sigma.mk_eq_mk_iff, heq_iff_eq]
+
 lemma prod_mul_distrib : s.prod (λx, f x * g x) = s.prod f * s.prod g :=
 eq.trans (by simp; refl) fold_op_distrib
 
+lemma prod_comm [decidable_eq γ] {s : finset γ} {t : finset α} {f : γ → α → β} :
+  (s.prod $ λx, t.prod $ f x) = (t.prod $ λy, s.prod $ λx, f x y) :=
+s.induction_on (by simp) (by simp [prod_mul_distrib] {contextual := tt})
+
 lemma prod_hom [comm_monoid γ] (g : β → γ)
   (h₁ : g 1 = 1) (h₂ : ∀x y, g (x * y) = g x * g y) : s.prod (λx, g (f x)) = g (s.prod f) :=
 eq.trans (by rw [h₁]; refl) (fold_hom h₂)
 
-@[simp] lemma prod_const_one : s.prod (λx, (1 : β)) = 1 :=
-s.induction_on (by simp) (by simp {contextual:=tt})
+lemma prod_subset (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → f x = 1) : s₁.prod f = s₂.prod f :=
+have (s₂ \ s₁).prod f = (s₂ \ s₁).prod (λx, 1),
+  from prod_congr begin simp [hf] {contextual := tt} end,
+calc s₁.prod f = (s₂ \ s₁).prod f * s₁.prod f : by simp [this]
+  ... = ((s₂ \ s₁) ∪ s₁).prod f : by rw [prod_union]; exact sdiff_inter_self
+  ... = s₂.prod f : by rw [sdiff_union_of_subset h]
 
 end comm_monoid
 
@@ -115,9 +161,7 @@ end finset
 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),
+  (`has_one, `has_zero), (`has_mul, `has_add), (`has_inv, `has_neg),
   /- map structures -/
   (`semigroup, `add_semigroup),
   (`monoid, `add_monoid),
@@ -144,16 +188,6 @@ run_cmd transport_multiplicative_to_additive [
   (`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),
@@ -164,45 +198,16 @@ run_cmd transport_multiplicative_to_additive [
   (`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)
-
-  --NEW:
+  /- new lemmas -/
   (`list.prod, `list.sum),
   (`list.prod.equations._eqn_1, `list.sum.equations._eqn_1),
   (`list.prod_nil, `list.sum_nil),
@@ -215,19 +220,23 @@ run_cmd transport_multiplicative_to_additive [
   (`finset.prod._proof_2, `finset.sum._proof_2),
   (`finset.prod, `finset.sum),
   (`finset.prod.equations._eqn_1, `finset.sum.equations._eqn_1),
+  (`finset.prod_to_finset_of_nodup, `finset.sum_to_finset_of_nodup),
   (`finset.prod_empty, `finset.sum_empty),
   (`finset.prod_insert, `finset.sum_insert),
   (`finset.prod_singleton, `finset.sum_singleton),
   (`finset.prod_union_inter, `finset.sum_union_inter),
   (`finset.prod_union, `finset.sum_union),
-  (`finset.prod_to_finset_of_nodup, `finset.sum_to_finset_of_nodup),
   (`finset.prod_image, `finset.sum_image),
+  (`finset.prod_bind, `finset.sum_bind),
+  (`finset.prod_product, `finset.sum_product),
   (`finset.prod_congr, `finset.sum_congr),
   (`finset.prod_hom, `finset.sum_hom),
-  (`finset.prod_const_one, `finset.sum_const_zero),
   (`finset.prod_mul_distrib, `finset.sum_add_distrib),
-  (`finset.prod_inv_distrib, `finset.sum_neg_distrib)
-  ]
+  (`finset.prod_inv_distrib, `finset.sum_neg_distrib),
+  (`finset.prod_const_one, `finset.sum_const_zero),
+  (`finset.prod_comm, `finset.sum_comm),
+  (`finset.prod_sigma, `finset.sum_sigma),
+  (`finset.prod_subset, `finset.sum_subset)]
 
 namespace finset
 variables [decidable_eq α] {s s₁ s₂ : finset α} {f g : α → β} {b : β} {a : α}
@@ -281,4 +290,45 @@ end
 
 end integral_domain
 
+section ordered_comm_monoid
+variables [ordered_comm_monoid β] [∀a b : β, decidable (a ≤ b)]
+
+lemma sum_le_sum' : (∀x∈s, f x ≤ g x) → s.sum f ≤ s.sum g :=
+s.induction_on (by simp; refl) $ assume a s ha ih h,
+  have f a + s.sum f ≤ g a + s.sum g,
+    from add_le_add' (h _ mem_insert) (ih $ assume x hx, h _ $ mem_insert_of_mem hx),
+  by simp [*]
+
+lemma zero_le_sum' (h : ∀x∈s, 0 ≤ f x) : 0 ≤ s.sum f := le_trans (by simp) (sum_le_sum' h)
+lemma sum_le_zero' (h : ∀x∈s, f x ≤ 0) : s.sum f ≤ 0 := le_trans (sum_le_sum' h) (by simp)
+
+lemma sum_le_sum_of_subset_of_nonneg
+  (h : s₁ ⊆ s₂) (hf : ∀x∈s₂, x ∉ s₁ → 0 ≤ f x) : s₁.sum f ≤ s₂.sum f :=
+calc s₁.sum f ≤ (s₂ \ s₁).sum f + s₁.sum f :
+    le_add_of_nonneg_left' $ zero_le_sum' $ by simp [hf] {contextual := tt}
+  ... = (s₂ \ s₁ ∪ s₁).sum f : (sum_union sdiff_inter_self).symm
+  ... = s₂.sum f : by rw [sdiff_union_of_subset h]
+
+lemma sum_eq_zero_iff_of_nonneg : (∀x∈s, 0 ≤ f x) → (s.sum f = 0 ↔ ∀x∈s, f x = 0) :=
+s.induction_on (by simp) $
+  by simp [or_imp_distrib, forall_and_distrib, zero_le_sum' ,
+           add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg'] {contextual := tt}
+
+end ordered_comm_monoid
+
+section canonically_ordered_monoid
+variables [canonically_ordered_monoid β] [∀a b:β, decidable (a ≤ b)]
+
+lemma sum_le_sum_of_subset (h : s₁ ⊆ s₂) : s₁.sum f ≤ s₂.sum f :=
+sum_le_sum_of_subset_of_nonneg h $ assume x h₁ h₂, zero_le
+
+lemma sum_le_sum_of_ne_zero (h : ∀x∈s₁, f x ≠ 0 → x ∈ s₂) : s₁.sum f ≤ s₂.sum f :=
+calc s₁.sum f = (s₁.filter (λx, f x = 0)).sum f + (s₁.filter (λx, f x ≠ 0)).sum f :
+    by rw [←sum_union filter_inter_filter_neg_eq, filter_union_filter_neg_eq]
+  ... ≤ s₂.sum f : add_le_of_nonpos_of_le'
+      (sum_le_zero' $ by simp {contextual:=tt})
+      (sum_le_sum_of_subset $ by simp [subset_iff, *] {contextual:=tt})
+
+end canonically_ordered_monoid
+
 end finset

algebra/functions.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2017 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+-/
+
+universe u
+variables {α : Type u}
+
+section
+variables [decidable_linear_order α] {a b c : α}
+
+lemma le_min_iff : c ≤ min a b ↔ c ≤ a ∧ c ≤ b :=
+⟨λ h, ⟨le_trans h (min_le_left a b), le_trans h (min_le_right a b)⟩,
+ λ ⟨h₁, h₂⟩, le_min h₁ h₂⟩
+
+lemma max_le_iff : max a b ≤ c ↔ a ≤ c ∧ b ≤ c :=
+⟨λ h, ⟨le_trans (le_max_left a b) h, le_trans (le_max_right a b) h⟩,
+ λ ⟨h₁, h₂⟩, max_le h₁ h₂⟩
+
+lemma max_lt_iff : max a b < c ↔ (a < c ∧ b < c) :=
+⟨assume h, ⟨lt_of_le_of_lt (le_max_left _ _) h, lt_of_le_of_lt (le_max_right _ _) h⟩,
+  assume ⟨h₁, h₂⟩, max_lt h₁ h₂⟩
+
+lemma lt_min_iff : a < min b c ↔ (a < b ∧ a < c) :=
+⟨assume h, ⟨lt_of_lt_of_le h (min_le_left _ _), lt_of_lt_of_le h (min_le_right _ _)⟩,
+  assume ⟨h₁, h₂⟩, lt_min h₁ h₂⟩
+
+end
+
+section decidable_linear_ordered_comm_group
+variables [decidable_linear_ordered_comm_group α] {a b : α}
+
+theorem abs_le : 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₁⟩
+
+lemma abs_lt : abs a < b ↔ (- b < a ∧ a < b) :=
+⟨assume h, ⟨neg_lt_of_neg_lt $ lt_of_le_of_lt (neg_le_abs_self _) h, lt_of_le_of_lt (le_abs_self _) h⟩,
+  assume ⟨h₁, h₂⟩, abs_lt_of_lt_of_neg_lt h₂ $ neg_lt_of_neg_lt h₁⟩
+
+@[simp] lemma abs_eq_zero : abs a = 0 ↔ a = 0 :=
+⟨eq_zero_of_abs_eq_zero, λ e, e.symm ▸ abs_zero⟩
+
+end decidable_linear_ordered_comm_group