feat(data/*): lemmas about lists and finsets (#4457)

A part of #4316

src/algebra/big_operators/basic.lean

@@ -39,7 +39,7 @@ namespace finset
 of the finite set `s`."]
 protected def prod [comm_monoid β] (s : finset α) (f : α → β) : β := (s.1.map f).prod
 
-@[simp] lemma prod_mk [comm_monoid β] (s : multiset α) (hs) (f : α → β) :
+@[simp, to_additive] lemma prod_mk [comm_monoid β] (s : multiset α) (hs) (f : α → β) :
   (⟨s, hs⟩ : finset α).prod f = (s.map f).prod :=
 rfl
 

src/data/fintype/basic.lean

@@ -40,8 +40,14 @@ fintype.complete x
 @[simp] lemma coe_univ : ↑(univ : finset α) = (set.univ : set α) :=
 by ext; simp
 
-lemma univ_nonempty [h : nonempty α] : (univ : finset α).nonempty :=
-nonempty.elim h (λ x, ⟨x, mem_univ x⟩)
+lemma univ_nonempty_iff : (univ : finset α).nonempty ↔ nonempty α :=
+by rw [← coe_nonempty, coe_univ, set.nonempty_iff_univ_nonempty]
+
+lemma univ_nonempty [nonempty α] : (univ : finset α).nonempty :=
+univ_nonempty_iff.2 ‹_›
+
+lemma univ_eq_empty : (univ : finset α) = ∅ ↔ ¬nonempty α :=
+by rw [← univ_nonempty_iff, nonempty_iff_ne_empty, ne.def, not_not]
 
 theorem subset_univ (s : finset α) : s ⊆ univ := λ a _, mem_univ a
 
@@ -303,6 +309,8 @@ finset.card_univ_diff s
 instance (n : ℕ) : fintype (fin n) :=
 ⟨finset.fin_range n, finset.mem_fin_range⟩
 
+lemma fin.univ_def (n : ℕ) : (univ : finset (fin n)) = finset.fin_range n := rfl
+
 @[simp] theorem fintype.card_fin (n : ℕ) : fintype.card (fin n) = n :=
 list.length_fin_range n
 

src/data/fintype/card.lean

@@ -74,6 +74,16 @@ end fintype
 
 open finset
 
+@[to_additive]
+theorem fin.prod_univ_def [comm_monoid β] {n : ℕ} (f : fin n → β) :
+  ∏ i, f i = ((list.fin_range n).map f).prod :=
+by simp [fin.univ_def, finset.fin_range]
+
+@[to_additive]
+theorem fin.prod_of_fn [comm_monoid β] {n : ℕ} (f : fin n → β) :
+  (list.of_fn f).prod = ∏ i, f i :=
+by rw [list.of_fn_eq_map, fin.prod_univ_def]
+
 /-- A product of a function `f : fin 0 → β` is `1` because `fin 0` is empty -/
 @[simp, to_additive "A sum of a function `f : fin 0 → β` is `0` because `fin 0` is empty"]
 theorem fin.prod_univ_zero [comm_monoid β] (f : fin 0 → β) : ∏ i, f i = 1 := rfl

src/data/list/basic.lean

@@ -1965,6 +1965,13 @@ lemma prod_take_succ :
 lemma length_pos_of_prod_ne_one (L : list α) (h : L.prod ≠ 1) : 0 < L.length :=
 by { cases L, { simp at h, cases h, }, { simp, }, }
 
+lemma prod_update_nth : ∀ (L : list α) (n : ℕ) (a : α),
+  (L.update_nth n a).prod =
+    (L.take n).prod * (if n < L.length then a else 1) * (L.drop (n + 1)).prod
+| (x::xs) 0     a := by simp [update_nth]
+| (x::xs) (i+1) a := by simp [update_nth, prod_update_nth xs i a, mul_assoc]
+| []      _     _ := by simp [update_nth, (nat.zero_le _).not_lt]
+
 end monoid
 
 @[simp]
@@ -2490,6 +2497,12 @@ by induction l; [refl, simp only [*, pmap, length]]
 
 @[simp] lemma length_attach (L : list α) : L.attach.length = L.length := length_pmap
 
+@[simp] lemma pmap_eq_nil {p : α → Prop} {f : Π a, p a → β}
+  {l H} : pmap f l H = [] ↔ l = [] :=
+by rw [← length_eq_zero, length_pmap, length_eq_zero]
+
+@[simp] lemma attach_eq_nil (l : list α) : l.attach = [] ↔ l = [] := pmap_eq_nil
+
 /-! ### find -/
 
 section find

src/data/list/nodup.lean

@@ -6,6 +6,12 @@ Authors: Mario Carneiro, Kenny Lau
 import data.list.pairwise
 import data.list.forall2
 
+/-!
+# Lists with no duplicates
+
+`list.nodup` is defined in `data/list/defs`. In this file we prove various properties of this predicate.
+-/
+
 universes u v
 
 open nat function
@@ -14,8 +20,6 @@ variables {α : Type u} {β : Type v}
 
 namespace list
 
-/- no duplicates predicate -/
-
 @[simp] theorem forall_mem_ne {a : α} {l : list α} : (∀ (a' : α), a' ∈ l → ¬a = a') ↔ a ∉ l :=
 ⟨λ h m, h _ m rfl, λ h a' m e, h (e.symm ▸ m)⟩
 
@@ -257,6 +261,19 @@ lemma nodup_update_nth : ∀ {l : list α} {n : ℕ} {a : α} (hl : l.nodup) (ha
       (λ hba, ha (hba ▸ mem_cons_self _ _)),
     nodup_update_nth (nodup_cons.1 hl).2 (mt (mem_cons_of_mem _) ha)⟩
 
+lemma nodup.map_update [decidable_eq α] {l : list α} (hl : l.nodup) (f : α → β) (x : α) (y : β) :
+  l.map (function.update f x y) =
+    if x ∈ l then (l.map f).update_nth (l.index_of x) y else l.map f :=
+begin
+  induction l with hd tl ihl, { simp },
+  rw [nodup_cons] at hl,
+  simp only [mem_cons_iff, map, ihl hl.2],
+  by_cases H : hd = x,
+  { subst hd,
+    simp [update_nth, hl.1] },
+  { simp [ne.symm H, H, update_nth, ← apply_ite (cons (f hd))] }
+end
+
 end list
 
 theorem option.to_list_nodup {α} : ∀ o : option α, o.to_list.nodup

src/data/list/of_fn.lean

@@ -60,9 +60,9 @@ begin
   simp only [d_array.rev_iterate_aux, of_fn_aux, IH]
 end
 
-theorem of_fn_zero (f : fin 0 → α) : of_fn f = [] := rfl
+@[simp] theorem of_fn_zero (f : fin 0 → α) : of_fn f = [] := rfl
 
-theorem of_fn_succ {n} (f : fin (succ n) → α) :
+@[simp] theorem of_fn_succ {n} (f : fin (succ n) → α) :
   of_fn f = f 0 :: of_fn (λ i, f i.succ) :=
 suffices ∀ {m h l}, of_fn_aux f (succ m) (succ_le_succ h) l =
   f 0 :: of_fn_aux (λ i, f i.succ) m h l, from this,
@@ -88,4 +88,8 @@ end
   (∀ i ∈ of_fn f, P i) ↔ ∀ j : fin n, P (f j) :=
 by simp only [mem_of_fn, set.forall_range_iff]
 
+@[simp] lemma of_fn_const (n : ℕ) (c : α) :
+  of_fn (λ i : fin n, c) = repeat c n :=
+nat.rec_on n (by simp) $ λ n ihn, by simp [ihn]
+
 end list

src/data/list/range.lean

@@ -16,11 +16,13 @@ universe u
 
 variables {α : Type u}
 
-
 @[simp] theorem length_range' : ∀ (s n : ℕ), length (range' s n) = n
 | s 0     := rfl
 | s (n+1) := congr_arg succ (length_range' _ _)
 
+@[simp] theorem range'_eq_nil {s n : ℕ} : range' s n = [] ↔ n = 0 :=
+by rw [← length_eq_zero, length_range']
+
 @[simp] theorem mem_range' {m : ℕ} : ∀ {s n : ℕ}, m ∈ range' s n ↔ s ≤ m ∧ m < s + n
 | s 0     := (false_iff _).2 $ λ ⟨H1, H2⟩, not_le_of_lt H2 H1
 | s (succ n) :=
@@ -100,6 +102,9 @@ by rw [range_eq_range', map_add_range']; refl
 @[simp] theorem length_range (n : ℕ) : length (range n) = n :=
 by simp only [range_eq_range', length_range']
 
+@[simp] theorem range_eq_nil {n : ℕ} : range n = [] ↔ n = 0 :=
+by rw [← length_eq_zero, length_range]
+
 theorem pairwise_lt_range (n : ℕ) : pairwise (<) (range n) :=
 by simp only [range_eq_range', pairwise_lt_range']
 
@@ -157,6 +162,8 @@ theorem reverse_range' : ∀ s n : ℕ,
 def fin_range (n : ℕ) : list (fin n) :=
 (range n).pmap fin.mk (λ _, list.mem_range.1)
 
+@[simp] lemma fin_range_zero : fin_range 0 = [] := rfl
+
 @[simp] lemma mem_fin_range {n : ℕ} (a : fin n) : a ∈ fin_range n :=
 mem_pmap.2 ⟨a.1, mem_range.2 a.2, fin.eta _ _⟩
 
@@ -166,6 +173,9 @@ nodup_pmap (λ _ _ _ _, fin.veq_of_eq) (nodup_range _)
 @[simp] lemma length_fin_range (n : ℕ) : (fin_range n).length = n :=
 by rw [fin_range, length_pmap, length_range]
 
+@[simp] lemma fin_range_eq_nil {n : ℕ} : fin_range n = [] ↔ n = 0 :=
+by rw [← length_eq_zero, length_fin_range]
+
 @[to_additive]
 theorem prod_range_succ {α : Type u} [monoid α] (f : ℕ → α) (n : ℕ) :
   ((range n.succ).map f).prod = ((range n).map f).prod * f n :=
@@ -200,6 +210,12 @@ theorem of_fn_eq_pmap {α n} {f : fin n → α} :
 by rw [pmap_eq_map_attach]; from ext_le (by simp)
   (λ i hi1 hi2, by { simp at hi1, simp [nth_le_of_fn f ⟨i, hi1⟩, -subtype.val_eq_coe] })
 
+theorem of_fn_id (n) : of_fn id = fin_range n := of_fn_eq_pmap
+
+theorem of_fn_eq_map {α n} {f : fin n → α} :
+  of_fn f = (fin_range n).map f :=
+by rw [← of_fn_id, map_of_fn, function.right_id]
+
 theorem nodup_of_fn {α n} {f : fin n → α} (hf : function.injective f) :
   nodup (of_fn f) :=
 by rw of_fn_eq_pmap; from nodup_pmap

src/data/multiset/basic.lean

@@ -752,6 +752,8 @@ theorem prod_eq_foldl [comm_monoid α] (s : multiset α) :
 theorem coe_prod [comm_monoid α] (l : list α) : prod ↑l = l.prod :=
 prod_eq_foldl _
 
+attribute [norm_cast] coe_prod coe_sum
+
 @[simp, to_additive]
 theorem prod_zero [comm_monoid α] : @prod α _ 0 = 1 := rfl