From 4fc35392bfde791c4ead63260f41c5833b5b6d99 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 9 Jun 2022 01:54:16 +0000 Subject: [PATCH] refactor(data/finset/nat_antidiagonal): state lemmas with cons instead of insert (#14533) This puts less of a burden on the caller rewriting in the forward direction, as they don't have to prove obvious things about membership when evaluating sums. Since this adds the missing `finset.map_cons`, a number of uses of `multiset.map_cons` now need qualified names. --- .../big_operators/nat_antidiagonal.lean | 5 +-- src/algebra/polynomial/big_operators.lean | 6 ++-- src/data/finset/basic.lean | 4 +++ src/data/finset/fold.lean | 4 +-- src/data/finset/nat_antidiagonal.lean | 33 ++++++++++--------- 5 files changed, 27 insertions(+), 25 deletions(-) diff --git a/src/algebra/big_operators/nat_antidiagonal.lean b/src/algebra/big_operators/nat_antidiagonal.lean index 3a9b8428ab5d3..a28d2e4d8eb0a 100644 --- a/src/algebra/big_operators/nat_antidiagonal.lean +++ b/src/algebra/big_operators/nat_antidiagonal.lean @@ -23,10 +23,7 @@ namespace nat lemma prod_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → M} : ∏ p in antidiagonal (n + 1), f p = f (0, n + 1) * ∏ p in antidiagonal n, f (p.1 + 1, p.2) := begin - rw [antidiagonal_succ, prod_insert, prod_map], refl, - intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩, - simp only [prod.mk.inj_iff, function.embedding.coe_prod_map, prod.map_mk] at h2, - apply nat.succ_ne_zero a h2.1, + rw [antidiagonal_succ, prod_cons, prod_map], refl, end lemma sum_antidiagonal_succ {n : ℕ} {f : ℕ × ℕ → N} : diff --git a/src/algebra/polynomial/big_operators.lean b/src/algebra/polynomial/big_operators.lean index 9bdb78fd068cf..87967ccbfdc9d 100644 --- a/src/algebra/polynomial/big_operators.lean +++ b/src/algebra/polynomial/big_operators.lean @@ -142,7 +142,7 @@ lemma leading_coeff_multiset_prod' (h : (t.map leading_coeff).prod ≠ 0) : t.prod.leading_coeff = (t.map leading_coeff).prod := begin induction t using multiset.induction_on with a t ih, { simp }, - simp only [map_cons, multiset.prod_cons] at h ⊢, + simp only [multiset.map_cons, multiset.prod_cons] at h ⊢, rw polynomial.leading_coeff_mul'; { rwa ih, apply right_ne_zero_of_mul h } end @@ -169,7 +169,7 @@ lemma nat_degree_multiset_prod' (h : (t.map (λ f, leading_coeff f)).prod ≠ 0) begin revert h, refine multiset.induction_on t _ (λ a t ih ht, _), { simp }, - rw [map_cons, multiset.prod_cons] at ht ⊢, + rw [multiset.map_cons, multiset.prod_cons] at ht ⊢, rw [multiset.sum_cons, polynomial.nat_degree_mul', ih], { apply right_ne_zero_of_mul ht }, { rwa polynomial.leading_coeff_multiset_prod', apply right_ne_zero_of_mul ht }, @@ -227,7 +227,7 @@ lemma coeff_zero_multiset_prod : t.prod.coeff 0 = (t.map (λ f, coeff f 0)).prod := begin refine multiset.induction_on t _ (λ a t ht, _), { simp }, - rw [multiset.prod_cons, map_cons, multiset.prod_cons, polynomial.mul_coeff_zero, ht] + rw [multiset.prod_cons, multiset.map_cons, multiset.prod_cons, polynomial.mul_coeff_zero, ht] end lemma coeff_zero_prod : diff --git a/src/data/finset/basic.lean b/src/data/finset/basic.lean index 4e782bdae5bcb..7eaf8f879e417 100644 --- a/src/data/finset/basic.lean +++ b/src/data/finset/basic.lean @@ -1907,6 +1907,10 @@ coe_injective $ by simp only [coe_map, coe_singleton, set.image_singleton] (insert a s).map f = insert (f a) (s.map f) := by simp only [insert_eq, map_union, map_singleton] +@[simp] lemma map_cons (f : α ↪ β) (a : α) (s : finset α) (ha : a ∉ s) : + (cons a s ha).map f = cons (f a) (s.map f) (by simpa using ha) := +eq_of_veq $ multiset.map_cons f a s.val + @[simp] theorem map_eq_empty : s.map f = ∅ ↔ s = ∅ := ⟨λ h, eq_empty_of_forall_not_mem $ λ a m, ne_empty_of_mem (mem_map_of_mem _ m) h, λ e, e.symm ▸ rfl⟩ diff --git a/src/data/finset/fold.lean b/src/data/finset/fold.lean index 725e3bfd48945..090ca4ace4742 100644 --- a/src/data/finset/fold.lean +++ b/src/data/finset/fold.lean @@ -30,11 +30,11 @@ variables {op} {f : α → β} {b : β} {s : finset α} {a : α} @[simp] theorem fold_empty : (∅ : finset α).fold op b f = b := rfl @[simp] theorem fold_cons (h : a ∉ s) : (cons a s h).fold op b f = f a * s.fold op b f := -by { dunfold fold, rw [cons_val, map_cons, fold_cons_left], } +by { dunfold fold, rw [cons_val, multiset.map_cons, fold_cons_left], } @[simp] theorem fold_insert [decidable_eq α] (h : a ∉ s) : (insert a s).fold op b f = f a * s.fold op b f := -by unfold fold; rw [insert_val, ndinsert_of_not_mem h, map_cons, fold_cons_left] +by unfold fold; rw [insert_val, ndinsert_of_not_mem h, multiset.map_cons, fold_cons_left] @[simp] theorem fold_singleton : ({a} : finset α).fold op b f = f a * b := rfl diff --git a/src/data/finset/nat_antidiagonal.lean b/src/data/finset/nat_antidiagonal.lean index 66f68b4a912f4..ce3779bfd31ef 100644 --- a/src/data/finset/nat_antidiagonal.lean +++ b/src/data/finset/nat_antidiagonal.lean @@ -39,32 +39,33 @@ by simp [antidiagonal] @[simp] lemma antidiagonal_zero : antidiagonal 0 = {(0, 0)} := rfl -lemma antidiagonal_succ {n : ℕ} : - antidiagonal (n + 1) = insert (0, n + 1) ((antidiagonal n).map - (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _))) := +lemma antidiagonal_succ (n : ℕ) : + antidiagonal (n + 1) = cons (0, n + 1) ((antidiagonal n).map + (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ (function.embedding.refl _))) + (by simp) := begin apply eq_of_veq, - rw [insert_val_of_not_mem, map_val], + rw [cons_val, map_val], { apply multiset.nat.antidiagonal_succ }, - { intro con, rcases mem_map.1 con with ⟨⟨a,b⟩, ⟨h1, h2⟩⟩, - simp only [prod.mk.inj_iff, function.embedding.coe_prod_map, prod.map_mk] at h2, - apply nat.succ_ne_zero a h2.1, } end -lemma antidiagonal_succ' {n : ℕ} : - antidiagonal (n + 1) = insert (n + 1, 0) ((antidiagonal n).map - (function.embedding.prod_map (function.embedding.refl _) ⟨nat.succ, nat.succ_injective⟩)) := +lemma antidiagonal_succ' (n : ℕ) : + antidiagonal (n + 1) = cons (n + 1, 0) ((antidiagonal n).map + (function.embedding.prod_map (function.embedding.refl _) ⟨nat.succ, nat.succ_injective⟩)) + (by simp) := begin apply eq_of_veq, - rw [insert_val_of_not_mem, map_val], - { apply multiset.nat.antidiagonal_succ' }, - { simp }, + rw [cons_val, map_val], + exact multiset.nat.antidiagonal_succ', end lemma antidiagonal_succ_succ' {n : ℕ} : - antidiagonal (n + 2) = insert (0, n + 2) (insert (n + 2, 0) ((antidiagonal n).map - (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ ⟨nat.succ, nat.succ_injective⟩))) := -by { rw [antidiagonal_succ, antidiagonal_succ', map_insert, map_map], refl } + antidiagonal (n + 2) = + cons (0, n + 2) + (cons (n + 2, 0) ((antidiagonal n).map + (function.embedding.prod_map ⟨nat.succ, nat.succ_injective⟩ ⟨nat.succ, nat.succ_injective⟩)) + $ by simp) (by simp) := +by { simp_rw [antidiagonal_succ (n + 1), antidiagonal_succ', finset.map_cons, map_map], refl } lemma map_swap_antidiagonal {n : ℕ} : (antidiagonal n).map ⟨prod.swap, prod.swap_right_inverse.injective⟩ = antidiagonal n :=