feat(data/{nat,int,zmod,finset}): add a few useful facts (#1220)

* feat(data/finset): add a few useful facts

* feat(data/zmod/basic): express neg in terms of residues

* feat(data/{nat,int}): add theorem 'mod_mod_of_dvd'

Author: avigad

src/data/finset.lean

@@ -508,6 +508,9 @@ ext.2 $ λ a, by simpa only [mem_sdiff, mem_union, or_comm,
 @[simp] theorem union_sdiff_of_subset {s₁ s₂ : finset α} (h : s₁ ⊆ s₂) : s₁ ∪ (s₂ \ s₁) = s₂ :=
 (union_comm _ _).trans (sdiff_union_of_subset h)
 
+theorem inter_sdiff (s t u : finset α) : s ∩ (t \ u) = s ∩ t \ u :=
+by { ext x, simp [and_assoc] }
+
 @[simp] theorem inter_sdiff_self (s₁ s₂ : finset α) : s₁ ∩ (s₂ \ s₁) = ∅ :=
 eq_empty_of_forall_not_mem $
 by simp only [mem_inter, mem_sdiff]; rintro x ⟨h, _, hn⟩; exact hn h
@@ -599,6 +602,19 @@ theorem filter_union_right (p q : α → Prop) [decidable_pred p] [decidable_pre
   s.filter p ∪ s.filter q = s.filter (λx, p x ∨ q x) :=
 ext.2 $ λ x, by simp only [mem_filter, mem_union, and_or_distrib_left.symm]
 
+theorem filter_inter {s t : finset α} : filter p s ∩ t = filter p (s ∩ t) :=
+by {ext, simp [and_assoc], rw [and.left_comm] }
+
+theorem inter_filter {s t : finset α} : s ∩ filter p t = filter p (s ∩ t) :=
+by rw [inter_comm, filter_inter, inter_comm]
+
+theorem filter_insert (a : α) (s : finset α) :
+  filter p (insert a s) = if p a then insert a (filter p s) else (filter p s) :=
+by { ext x, simp, split_ifs with h; by_cases h' : x = a; simp [h, h'] }
+
+theorem filter_singleton (a : α) : filter p (singleton a) = if p a then singleton a else ∅ :=
+by { ext x, simp, split_ifs with h; by_cases h' : x = a; simp [h, h'] }
+
 theorem filter_or (s : finset α) : s.filter (λ a, p a ∨ q a) = s.filter p ∪ s.filter q :=
 ext.2 $ λ _, by simp only [mem_filter, mem_union, and_or_distrib_left]
 
@@ -1124,6 +1140,14 @@ ext.2 $ λ x, by simp only [mem_bind, exists_prop, mem_union, mem_insert,
 @[simp] lemma singleton_bind [decidable_eq α] {a : α} : (singleton a).bind t = t a :=
 show (insert a ∅ : finset α).bind t = t a, from bind_insert.trans $ union_empty _
 
+theorem bind_inter (s : finset α) (f : α → finset β) (t : finset β) :
+  s.bind f ∩ t = s.bind (λ x, f x ∩ t) :=
+by { ext x, simp, exact ⟨λ ⟨xt, y, ys, xf⟩, ⟨y, ys, xt, xf⟩, λ ⟨y, ys, xt, xf⟩, ⟨xt, y, ys, xf⟩⟩ }
+
+theorem inter_bind (t : finset β) (s : finset α) (f : α → finset β) :
+  t ∩ s.bind f = s.bind (λ x, t ∩ f x) :=
+by rw [inter_comm, bind_inter]; simp
+
 theorem image_bind [decidable_eq γ] {f : α → β} {s : finset α} {t : β → finset γ} :
   (s.image f).bind t = s.bind (λa, t (f a)) :=
 by haveI := classical.dec_eq α; exact

src/data/int/basic.lean

@@ -404,9 +404,15 @@ by rw [mul_comm, mul_mod_left]
 @[simp] theorem mod_self {a : ℤ} : a % a = 0 :=
 by have := mul_mod_left 1 a; rwa one_mul at this
 
-@[simp] lemma mod_mod (a b : ℤ) : a % b % b = a % b :=
+@[simp] theorem mod_mod (a b : ℤ) : a % b % b = a % b :=
 by conv {to_rhs, rw [← mod_add_div a b, add_mul_mod_self_left]}
 
+@[simp] theorem mod_mod_of_dvd (n : int) {m k : int} (h : m ∣ k) : n % k % m = n % m :=
+begin
+  conv { to_rhs, rw ←mod_add_div n k },
+  rcases h with ⟨t, rfl⟩, rw [mul_assoc, add_mul_mod_self_left]
+end
+
 /- properties of / and % -/
 
 @[simp] theorem mul_div_mul_of_pos {a : ℤ} (b c : ℤ) (H : a > 0) : a * b / (a * c) = b / c :=

src/data/nat/basic.lean

@@ -469,6 +469,12 @@ exists_congr $ λ d, by rw [mul_right_comm, nat.mul_right_inj hc]
   (λ n0, by simp [n0])
   (λ npos, mod_eq_of_lt (mod_lt _ npos))
 
+@[simp] theorem mod_mod_of_dvd (n : nat) {m k : nat} (h : m ∣ k) : n % k % m = n % m :=
+begin
+  conv { to_rhs, rw ←mod_add_div n k },
+  rcases h with ⟨t, rfl⟩, rw [mul_assoc, add_mul_mod_self_left]
+end
+
 theorem add_pos_left {m : ℕ} (h : m > 0) (n : ℕ) : m + n > 0 :=
 calc
   m + n > 0 + n : nat.add_lt_add_right h n

src/data/zmod/basic.lean

@@ -103,6 +103,20 @@ begin
     exact nat.modeq.modeq_add (nat.mod_mod a n) (nat.mod_mod 1 n) }
 end
 
+lemma neg_val' {m : pnat} (n : zmod m) : (-n).val = (m - n.val) % m :=
+have ((-n).val + n.val) % m = (m - n.val + n.val) % m,
+  by { rw [←add_val, add_left_neg, nat.sub_add_cancel (le_of_lt n.is_lt), nat.mod_self], refl },
+(nat.mod_eq_of_lt (fin.is_lt _)).symm.trans (nat.modeq.modeq_add_cancel_right rfl this)
+
+lemma neg_val {m : pnat} (n : zmod m) : (-n).val = if n = 0 then 0 else m - n.val :=
+begin
+  rw neg_val',
+  by_cases h : n = 0; simp [h],
+  cases n with n nlt; cases n; dsimp, { contradiction },
+  rw nat.mod_eq_of_lt,
+  apply nat.sub_lt m.2 (nat.succ_pos _),
+end
+
 lemma mk_eq_cast {n : ℕ+} {a : ℕ} (h : a < n) : (⟨a, h⟩ : zmod n) = (a : zmod n) :=
 fin.eq_of_veq (by rw [val_cast_nat, nat.mod_eq_of_lt h])