chore(archive/100-theorems-list/30_ballot_problem): golf (#18126)

Also add some supporting lemmas.

Author: urkud

archive/100-theorems-list/30_ballot_problem.lean

@@ -66,73 +66,44 @@ This represents vote sequences where candidate `+1` receives `p` votes and candi
 def counted_sequence (p q : ℕ) : set (list ℤ) :=
 {l | l.count 1 = p ∧ l.count (-1) = q ∧ ∀ x ∈ l, x = (1 : ℤ) ∨ x = -1}
 
-@[simp] lemma counted_right_zero (p : ℕ) : counted_sequence p 0 = {list.repeat 1 p} :=
+/-- An alternative definition of `counted_sequence` that uses `list.perm`. -/
+lemma mem_counted_sequence_iff_perm {p q l} :
+  l ∈ counted_sequence p q ↔ l ~ list.repeat (1 : ℤ) p ++ list.repeat (-1) q :=
 begin
-  ext l,
-  rw [counted_sequence, mem_singleton_iff],
-  split,
-  { rintro ⟨hl₀, hl₁, hl₂⟩,
-    rw list.eq_repeat,
-    have : ∀ x ∈ l, (1 : ℤ) = x,
-    { intros x hx,
-      obtain rfl | rfl := hl₂ x hx,
-      { refl },
-      { exact false.elim (list.not_mem_of_count_eq_zero hl₁ hx) } },
-    split,
-    { rwa ← list.count_eq_length.2 this },
-    { exact λ x hx, (this x hx).symm } },
-  { rintro rfl,
-    simp only [mem_set_of_eq, list.count_repeat_self, eq_self_iff_true, true_and],
-    refine ⟨list.count_eq_zero_of_not_mem _, λ x, _⟩; rw list.mem_repeat,
-    { norm_num },
-    { rintro ⟨-, rfl⟩,
-      exact or.inl rfl } }
+  rw [list.perm_repeat_append_repeat],
+  { simp only [counted_sequence, list.subset_def, mem_set_of_eq, list.mem_cons_iff,
+      list.mem_singleton] },
+  { norm_num1 }
 end
 
+@[simp] lemma counted_right_zero (p : ℕ) : counted_sequence p 0 = {list.repeat 1 p} :=
+by { ext l, simp [mem_counted_sequence_iff_perm] }
+
 @[simp] lemma counted_left_zero (q : ℕ) : counted_sequence 0 q = {list.repeat (-1) q} :=
-begin
-  ext l,
-  rw [counted_sequence, mem_singleton_iff],
-  split,
-  { rintro ⟨hl₀, hl₁, hl₂⟩,
-    rw list.eq_repeat,
-    have : ∀ x ∈ l, (-1 : ℤ) = x,
-    { intros x hx,
-      obtain rfl | rfl := hl₂ x hx,
-      { exact false.elim (list.not_mem_of_count_eq_zero hl₀ hx) },
-      { refl } },
-    split,
-    { rwa ← list.count_eq_length.2 this },
-    { exact λ x hx, (this x hx).symm } },
-  { rintro rfl,
-    simp only [mem_set_of_eq, list.count_repeat_self, eq_self_iff_true, true_and],
-    refine ⟨list.count_eq_zero_of_not_mem _, λ x, _⟩; rw list.mem_repeat,
-    { norm_num },
-    { rintro ⟨-, rfl⟩,
-      exact or.inr rfl } }
-end
+by { ext l, simp [mem_counted_sequence_iff_perm] }
+
+lemma mem_of_mem_counted_sequence {p q} {l} (hl : l ∈ counted_sequence p q) {x : ℤ} (hx : x ∈ l) :
+  x = 1 ∨ x = -1 :=
+hl.2.2 x hx
+
+lemma length_of_mem_counted_sequence {p q} {l : list ℤ} (hl : l ∈ counted_sequence p q) :
+  l.length = p + q :=
+by simp [(mem_counted_sequence_iff_perm.1 hl).length_eq]
+
+lemma counted_eq_nil_iff {p q : ℕ} {l : list ℤ} (hl : l ∈ counted_sequence p q) :
+  l = [] ↔ p = 0 ∧ q = 0 :=
+list.length_eq_zero.symm.trans $ by simp [length_of_mem_counted_sequence hl]
 
 lemma counted_ne_nil_left {p q : ℕ} (hp : p ≠ 0) {l : list ℤ} (hl : l ∈ counted_sequence p q) :
-  l ≠ list.nil :=
-begin
-  obtain ⟨hl₀, hl₁, hl₂⟩ := hl,
-  rintro rfl,
-  rw list.count_nil at hl₀,
-  exact hp hl₀.symm,
-end
+  l ≠ [] :=
+by simp [counted_eq_nil_iff hl, hp]
 
-lemma counted_ne_nil_right {p q : ℕ} (hp : q ≠ 0) {l : list ℤ} (hl : l ∈ counted_sequence p q) :
-  l ≠ list.nil :=
-begin
-  obtain ⟨hl₀, hl₁, hl₂⟩ := hl,
-  rintro rfl,
-  rw list.count_nil at hl₁,
-  exact hp hl₁.symm,
-end
+lemma counted_ne_nil_right {p q : ℕ} (hq : q ≠ 0) {l : list ℤ} (hl : l ∈ counted_sequence p q) :
+  l ≠ [] :=
+by simp [counted_eq_nil_iff hl, hq]
 
 lemma counted_succ_succ (p q : ℕ) : counted_sequence (p + 1) (q + 1) =
-  (counted_sequence p (q + 1)).image (list.cons 1) ∪
-  (counted_sequence (p + 1) q).image (list.cons (-1)) :=
+  list.cons 1 '' counted_sequence p (q + 1) ∪ list.cons (-1) '' counted_sequence (p + 1) q  :=
 begin
   ext l,
   rw [counted_sequence, counted_sequence, counted_sequence],
@@ -193,79 +164,13 @@ lemma counted_sequence_nonempty : ∀ (p q : ℕ), (counted_sequence p q).nonemp
     exact or.inl (counted_sequence_nonempty _ _),
   end
 
-lemma sum_of_mem_counted_sequence :
-  ∀ {p q : ℕ} {l : list ℤ} (hl : l ∈ counted_sequence p q), l.sum = p - q
-| 0 q l hl :=
-  begin
-    rw [counted_left_zero, mem_singleton_iff] at hl,
-    simp [hl],
-  end
-| p 0 l hl :=
-  begin
-    rw [counted_right_zero, mem_singleton_iff] at hl,
-    simp [hl],
-  end
-| (p + 1) (q + 1) l hl :=
-  begin
-    simp only [counted_succ_succ, mem_union, mem_image] at hl,
-    rcases hl with (⟨l, hl, rfl⟩ | ⟨l, hl, rfl⟩),
-    { rw [list.sum_cons, sum_of_mem_counted_sequence hl],
-      push_cast,
-      ring },
-    { rw [list.sum_cons, sum_of_mem_counted_sequence hl],
-      push_cast,
-      ring }
-  end
-
-lemma mem_of_mem_counted_sequence :
-  ∀ {p q : ℕ} {l} (hl : l ∈ counted_sequence p q) {x : ℤ} (hx : x ∈ l), x = 1 ∨ x = -1
-| 0 q l hl x hx :=
-  begin
-    rw [counted_left_zero, mem_singleton_iff] at hl,
-    subst hl,
-    exact or.inr (list.eq_of_mem_repeat hx),
-  end
-| p 0 l hl x hx :=
-  begin
-    rw [counted_right_zero, mem_singleton_iff] at hl,
-    subst hl,
-    exact or.inl (list.eq_of_mem_repeat hx),
-  end
-| (p + 1) (q + 1) l hl x hx :=
-  begin
-    simp only [counted_succ_succ, mem_union, mem_image] at hl,
-    rcases hl with (⟨l, hl, rfl⟩ | ⟨l, hl, rfl⟩);
-    rcases hx with (rfl | hx),
-    { left, refl },
-    { exact mem_of_mem_counted_sequence hl hx },
-    { right, refl },
-    { exact mem_of_mem_counted_sequence hl hx },
-  end
-
-lemma length_of_mem_counted_sequence :
-  ∀ {p q : ℕ} {l : list ℤ} (hl : l ∈ counted_sequence p q), l.length = p + q
-| 0 q l hl :=
-  begin
-    rw [counted_left_zero, mem_singleton_iff] at hl,
-    simp [hl],
-  end
-| p 0 l hl :=
-  begin
-    rw [counted_right_zero, mem_singleton_iff] at hl,
-    simp [hl],
-  end
-| (p + 1) (q + 1) l hl :=
-  begin
-    simp only [counted_succ_succ, mem_union, mem_image] at hl,
-    rcases hl with (⟨l, hl, rfl⟩ | ⟨l, hl, rfl⟩),
-    { rw [list.length_cons, length_of_mem_counted_sequence hl, add_right_comm] },
-    { rw [list.length_cons, length_of_mem_counted_sequence hl, ←add_assoc] }
-  end
+lemma sum_of_mem_counted_sequence {p q} {l : list ℤ} (hl : l ∈ counted_sequence p q) :
+  l.sum = p - q :=
+by simp [(mem_counted_sequence_iff_perm.1 hl).sum_eq, sub_eq_add_neg]
 
 lemma disjoint_bits (p q : ℕ) :
-  disjoint
-    ((counted_sequence p (q + 1)).image (list.cons 1))
-    ((counted_sequence (p + 1) q).image (list.cons (-1))) :=
+  disjoint (list.cons 1 '' counted_sequence p (q + 1))
+    (list.cons (-1) '' counted_sequence (p + 1) q) :=
 begin
   simp_rw [disjoint_left, mem_image, not_exists, exists_imp_distrib],
   rintros _ _ ⟨_, rfl⟩ _ ⟨_, _, _⟩,

src/data/list/basic.lean

@@ -318,6 +318,8 @@ iff.intro or_exists_of_exists_mem_cons
 
 /-! ### list subset -/
 
+instance : is_trans (list α) (⊆) := ⟨λ _ _ _, list.subset.trans⟩
+
 theorem subset_def {l₁ l₂ : list α} : l₁ ⊆ l₂ ↔ ∀ ⦃a : α⦄, a ∈ l₁ → a ∈ l₂ := iff.rfl
 
 theorem subset_append_of_subset_left (l l₁ l₂ : list α) : l ⊆ l₁ → l ⊆ l₁++l₂ :=

src/data/list/perm.lean

@@ -79,6 +79,12 @@ theorem perm.subset {l₁ l₂ : list α} (p : l₁ ~ l₂) : l₁ ⊆ l₂ :=
 theorem perm.mem_iff {a : α} {l₁ l₂ : list α} (h : l₁ ~ l₂) : a ∈ l₁ ↔ a ∈ l₂ :=
 iff.intro (λ m, h.subset m) (λ m, h.symm.subset m)
 
+lemma perm.subset_congr_left {l₁ l₂ l₃ : list α} (h : l₁ ~ l₂) : l₁ ⊆ l₃ ↔ l₂ ⊆ l₃ :=
+⟨h.symm.subset.trans, h.subset.trans⟩
+
+lemma perm.subset_congr_right {l₁ l₂ l₃ : list α} (h : l₁ ~ l₂) : l₃ ⊆ l₁ ↔ l₃ ⊆ l₂ :=
+⟨λ h', h'.trans h.subset, λ h', h'.trans h.symm.subset⟩
+
 theorem perm.append_right {l₁ l₂ : list α} (t₁ : list α) (p : l₁ ~ l₂) : l₁++t₁ ~ l₂++t₁ :=
 perm.rec_on p
   (perm.refl ([] ++ t₁))
@@ -730,6 +736,16 @@ theorem perm_iff_count {l₁ l₂ : list α} : l₁ ~ l₂ ↔ ∀ a, count a l
     by_cases b = a; simp [h] at H ⊢; assumption }
 end⟩
 
+theorem perm_repeat_append_repeat {l : list α} {a b : α} {m n : ℕ} (h : a ≠ b) :
+  l ~ repeat a m ++ repeat b n ↔ count a l = m ∧ count b l = n ∧ l ⊆ [a, b] :=
+begin
+  rw [perm_iff_count, ← decidable.and_forall_ne a, ← decidable.and_forall_ne b],
+  suffices : l ⊆ [a, b] ↔ ∀ c, c ≠ b → c ≠ a → c ∉ l,
+  { simp [count_repeat, h, h.symm, this] { contextual := tt } },
+  simp_rw [ne.def, ← and_imp, ← not_or_distrib, decidable.not_imp_not, subset_def, mem_cons_iff,
+    not_mem_nil, or_false, or_comm],
+end
+
 lemma subperm.cons_right {α : Type*} {l l' : list α} (x : α) (h : l <+~ l') : l <+~ x :: l' :=
 h.trans (sublist_cons x l').subperm
 

src/logic/basic.lean

@@ -1146,10 +1146,13 @@ by simp [and_comm]
 @[simp] theorem forall_eq' {a' : α} : (∀a, a' = a → p a) ↔ p a' :=
 by simp [@eq_comm _ a']
 
-theorem and_forall_ne (a : α) : (p a ∧ ∀ b ≠ a, p b) ↔ ∀ b, p b :=
-by simp only [← @forall_eq _ p a, ← forall_and_distrib, ← or_imp_distrib, classical.em,
+theorem decidable.and_forall_ne [decidable_eq α] (a : α) : (p a ∧ ∀ b ≠ a, p b) ↔ ∀ b, p b :=
+by simp only [← @forall_eq _ p a, ← forall_and_distrib, ← or_imp_distrib, decidable.em,
   forall_const]
 
+theorem and_forall_ne (a : α) : (p a ∧ ∀ b ≠ a, p b) ↔ ∀ b, p b :=
+decidable.and_forall_ne a
+
 -- this lemma is needed to simplify the output of `list.mem_cons_iff`
 @[simp] theorem forall_eq_or_imp {a' : α} : (∀ a, a = a' ∨ q a → p a) ↔ p a' ∧ ∀ a, q a → p a :=
 by simp only [or_imp_distrib, forall_and_distrib, forall_eq]