[Merged by Bors] - feat(data/sign): Allocating signs

src/data/sign.lean

@@ -3,8 +3,7 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
-import order.basic
-import algebra.algebra.basic
+import algebra.big_operators.basic
 import tactic.derive_fintype
 
 /-!
@@ -202,3 +201,58 @@ def sign_hom : α →*₀ sign_type :=
                mul_neg_of_pos_of_neg, mul_pos] }
 
 end linear_ordered_ring
+
+namespace int
+
+lemma sign_eq_sign (n : ℤ) : n.sign = _root_.sign n :=
+begin
+  obtain ((_ | _) | _) := n,
+  { exact congr_arg coe sign_zero.symm },
+  { exact congr_arg coe (sign_pos $ int.succ_coe_nat_pos _).symm },
+  { exact congr_arg coe (_root_.sign_neg $ neg_succ_lt_zero _).symm }
+end
+end int
+
+open finset nat
+open_locale big_operators
+
+-- TODO: Inlining this yields an app-builder exception
+lemma exists_signed_sum_aux [decidable_eq α] {n : ℕ} (sgn : ℕ → sign_type) (b : α) {f : α → ℤ}
+  ⦃a : α⦄ (g : ℕ → α) (i : ℕ) :
+   (if (range (n - (f a).nat_abs)).piecewise g (λ _, a) i = b then
+       ((range (n - (f a).nat_abs)).piecewise sgn (λ _, sign (f a)) i : ℤ) else 0) =
+    (range (n - (f a).nat_abs)).piecewise (λ j, if g j = b then ↑(sgn j) else 0)
+        (λ j, if a = b then ↑(sign (f a)) else 0) i :=
+by { unfold piecewise, split_ifs; refl }
+
+/-- We can decompose a sum of absolute value less than `n` into a sum of at most `n` signs. -/
+lemma exists_signed_sum [decidable_eq α] [nonempty α] (s : finset α) (n : ℕ) (f : α → ℤ)
+  (hn : ∑ i in s, (f i).nat_abs ≤ n) :
+  ∃ (sgn : ℕ → sign_type) (g : ℕ → α), (∀ i, g i ∉ s → sgn i = 0) ∧
+    ∀ a ∈ s, (∑ i in range n, if g i = a then (sgn i : ℤ) else 0) = f a :=
+begin
+  induction s using finset.cons_induction with a s ha ih generalizing n,
+  { exact ⟨0, classical.arbitrary _, λ _ _, rfl, λ _, false.elim⟩ },
+  rw sum_cons at hn,
+  obtain ⟨sgn, g, hg, hf⟩ := ih _ (le_tsub_of_add_le_left hn),
+  refine ⟨(range $ n - (f a).nat_abs).piecewise sgn (λ _, sign (f a)),
+    (range $ n - (f a).nat_abs).piecewise g (λ _, a), λ i hi, _, λ b hb, _⟩,
+  { by_cases i ∈ range (n - (f a).nat_abs),
+    { rw piecewise_eq_of_mem _ _ _ h at ⊢ hi,
+      exact hg _ (λ h, hi $ subset_cons _ h) },
+    { rw piecewise_eq_of_not_mem _ _ _ h at hi,
+      exact (hi $ mem_cons_self _ _).elim } },
+  transitivity ∑ i in range n, (range $ n - (f a).nat_abs).piecewise
+    (λ j, ite (g j = b) (sgn j : ℤ) 0) (λ j, ite (a = b) (sign $ f a) 0) i,
+  { exact sum_congr rfl (λ i _, exists_signed_sum_aux _ _ _ _) },
+  rw [sum_piecewise, (inter_eq_right_iff_subset _ _).2 (range_mono tsub_le_self)],
+  rw mem_cons at hb,
+  obtain rfl | hb := hb,
+  { rw [sum_eq_zero, zero_add, sum_const, if_pos rfl, card_sdiff (range_mono tsub_le_self),
+      card_range, card_range, tsub_tsub_cancel_of_le (le_of_add_le_left hn), nsmul_eq_mul, mul_comm,
+      ←int.sign_eq_sign, int.nat_cast_eq_coe_nat, (f b).sign_mul_nat_abs],
+    refine λ i hi, ite_eq_right_iff.2 _,
+    rintro rfl,
+    rw [hg _ ha, sign_type.coe_zero] },
+  { simp_rw [if_neg (ne_of_mem_of_not_mem hb ha).symm, hf _ hb, sum_const_zero, add_zero] }
+end

src/logic/nonempty.lean

@@ -75,9 +75,6 @@ iff.intro (assume h a, h _) (assume h ⟨a⟩, h _)
 @[simp] lemma nonempty.exists {α} {p : nonempty α → Prop} : (∃h:nonempty α, p h) ↔ (∃a, p ⟨a⟩) :=
 iff.intro (assume ⟨⟨a⟩, h⟩, ⟨a, h⟩) (assume ⟨a, h⟩, ⟨⟨a⟩, h⟩)
 
-lemma classical.nonempty_pi {α} {β : α → Sort*} : nonempty (Πa:α, β a) ↔ (∀a:α, nonempty (β a)) :=
-iff.intro (assume ⟨f⟩ a, ⟨f a⟩) (assume f, ⟨assume a, classical.choice $ f a⟩)
-
 /-- Using `classical.choice`, lifts a (`Prop`-valued) `nonempty` instance to a (`Type`-valued)
   `inhabited` instance. `classical.inhabited_of_nonempty` already exists, in
   `core/init/classical.lean`, but the assumption is not a type class argument,
@@ -112,6 +109,12 @@ h.elim $ f ∘ inhabited.mk
 instance {α β} [h : nonempty α] [h2 : nonempty β] : nonempty (α × β) :=
 h.elim $ λ g, h2.elim $ λ g2, ⟨⟨g, g2⟩⟩
 
+instance {ι : Sort*} {α : ι → Sort*} [Π i, nonempty (α i)] : nonempty (Π i, α i) :=
+⟨λ _, classical.arbitrary _⟩
+
+lemma classical.nonempty_pi {ι} {α : ι → Sort*} : nonempty (Π i, α i) ↔ ∀ i, nonempty (α i) :=
+⟨λ ⟨f⟩ a, ⟨f a⟩, @pi.nonempty _ _⟩
+
 lemma subsingleton_of_not_nonempty {α : Sort*} (h : ¬ nonempty α) : subsingleton α :=
 ⟨λ x, false.elim $ not_nonempty_iff_imp_false.mp h x⟩