Lemmas about nat / list / finset

Stream: Is there code for X?

[Patrick Johnson]

Here are some statements that I proved as helper lemmas in some of my other projects. Please let me know which lemmas of them (if any) I should PR to mathlib. Note that some of them trivially follow from what is already in mathlib, but are useful for rewriting.

Statements

import tactic
import tactic.induction
import data.nat.lattice
import data.list.basic
import logic.function.iterate

noncomputable theory
open_locale classical
open_locale big_operators

lemma finset_union_singleton {α : Type*} {s : finset α} {x : α} :
  s ∪ {x} = insert x s := sorry

lemma iter_add {α : Type*} {f : α → α} {x : α} {m n : ℕ} :
  (f^[m + n]) x = (f^[n]) ((f^[m]) x) := sorry

lemma iter_add_mul_eq_of_add_eq {α : Type*}
  {f : α → α} {x : α} {n m d : ℕ}
  (h : (f^[n + d]) x = (f^[n]) x) :
  (f^[n + d * m]) x = (f^[n]) x := sorry

lemma iter_mul_eq_of_eq {α : Type*}
  {f : α → α} {x : α} {m d : ℕ}
  (h : (f^[d]) x = x) :
  (f^[d * m]) x = x := sorry

lemma list_nth_le_eq_iff {α : Type*}
  {l : list α} {n : ℕ} {x : α} {h} :
  l.nth_le n h = x ↔ l.nth n = some x := sorry

lemma list_some_nth_le_eq {α : Type*}
  {l : list α} {n : ℕ} {h} :
  some (l.nth_le n h) = l.nth n := sorry

lemma list_nodup_iff {α : Type*} {l : list α} :
  l.nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.nth i ≠ l.nth j := sorry

lemma nat_sub_lt_of_lt {a b c : ℕ} (h : a < b) : a - c < b := sorry

lemma nat_add_sub {a b : ℕ} (h : a ≤ b) : a + (b - a) = b := sorry

lemma nat_find_spec_lt {P : ℕ → Prop}
  (h : ∃ (n : ℕ), P n) :
  ∀ (n : ℕ), n < nat.find h → ¬P n := sorry

lemma nat_mul_add_mod {a b c : ℕ} : (a * b + c) % b = c % b := sorry

lemma nat_mul_add_mod_of_lt {a b c : ℕ} (h : c < b) : (a * b + c) % b = c := sorry

lemma nat_exi_mul (x y : ℕ) :
  ∃ (a b : ℕ), x / y = a ∧ x % y = b ∧ x = y * a + b := sorry

lemma list_length_eq_card_to_finset_of_nodup {α : Type*} {l : list α}
  (h : l.nodup) : l.length = l.to_finset.card := sorry

lemma list_length_le_fintype_card_of_nodup {α : Type*} [fintype α] {l : list α}
  (h : l.nodup) : l.length ≤ fintype.card α := sorry

lemma list_nth_cons_of_pos {α : Type*} {l : list α} {x : α} {n : ℕ}
  (h : 0 < n) : (x :: l).nth n = l.nth (n - 1) := sorry

lemma list_length_snoc {α : Type*} {l : list α} {x : α} :
  (l ++ [x]).length = l.length + 1 := sorry

lemma list_dedup_singleton {α : Type*} {x : α} : [x].dedup = [x] := sorry

lemma list_length_dedup_le {α : Type*} {l : list α} :
  l.dedup.length ≤ l.length := sorry

lemma list_length_dedup_eq_card_to_finset {α : Type*} {l : list α} :
  l.dedup.length = l.to_finset.card := sorry

lemma list_length_dedup_append_le {α : Type*} {l₁ l₂ : list α} :
  ((l₁ ++ l₂).dedup).length ≤ l₁.dedup.length + l₂.dedup.length := sorry

lemma list_dedup_dup_cons {α : Type*} {l : list α} {x : α} :
  (x :: x :: l).dedup = (x :: l).dedup := sorry

lemma list_length_dedup_cons_le_of_mem {α : Type*} {l : list α} {x : α}
  (h : x ∈ l) : (x :: l).dedup.length ≤ l.length := sorry

lemma list_eq_append {α : Type*} {l : list α} {i : ℕ}
  (h : i < l.length) : l = l.take i ++ l.drop i := sorry

lemma list_eq_tail_of_cons_eq {α : Type*} {l₁ l₂ : list α} {x : α}
  (h : x :: l₁ = l₂) : l₁ = l₂.tail := sorry

lemma list_length_dedup_lt_of_dup {α : Type*} {l : list α}
  (h : ¬l.nodup) : l.dedup.length < l.length := sorry

lemma list_dedup_length_eq_length_iff {α : Type*} {l : list α} :
  l.dedup.length = l.length ↔ l.nodup := sorry

lemma list_nth_snoc_right {α : Type*} {l : list α} {x : α} :
  (l ++ [x]).nth l.length = some x := sorry

lemma nat_pred_eq_self_iff {n : ℕ} : n.pred = n ↔ n = 0 := sorry

lemma list_count_erase {α : Type*} {l : list α} {x : α} :
  (l.erase x).count x = l.count x - (ite (x ∈ l) 1 0) := sorry

lemma list_mem_diff_iff {α : Type*} {l₁ l₂ : list α} {x : α} :
  x ∈ l₁ \ l₂ ↔ l₂.count x < l₁.count x := sorry

lemma finset_sum_le_sum_of_le {α : Type*} {f g : α → ℕ} {s : finset α}
  (h : ∀ (a : α), a ∈ s → f a ≤ g a) :
  ∑ (a : α) in s, f a ≤ ∑ (a : α) in s, g a := sorry

lemma list_sum_count_cons_diff_singleton {α : Type*} {l : list α} {x : α} :
  ∑ (a : α) in l.to_finset \ {x}, (x :: l).count a =
  ∑ (a : α) in l.to_finset \ {x}, l.count a := sorry

lemma list_sum_count_cons {α : Type*} {l : list α} {x : α} :
  ∑ (a : α) in l.to_finset, (x :: l).count a =
  ∑ (a : α) in l.to_finset, l.count a + ite (x ∈ l) 1 0 := sorry

lemma list_length_eq_sum_count {α : Type*} {l : list α} :
  l.length = ∑ (x : α) in l.to_finset, l.count x := sorry

lemma list_sum_union_eq_sum {α : Type*} {l : list α} {s : finset α} :
  ∑ (x : α) in l.to_finset ∪ s, l.count x =
  ∑ (x : α) in l.to_finset, l.count x := sorry

lemma list_length_le_length_of_count_le_count {α : Type*}
  {l₁ l₂ : list α} (h : ∀ (a : α), l₁.count a ≤ l₂.count a) :
  l₁.length ≤ l₂.length := sorry

lemma list_count_map_eq_length_filter {α β : Type*} {f : α → β}
  {l : list α} {y : β} :
  (l.map f).count y = (l.filter (λ (x : α), f x = y)).length := sorry

lemma list_count_filter_eq_ite {α : Type*} {P : α → Prop}
  {l : list α} {x : α} : (l.filter P).count x = ite (P x) (l.count x) 0 := sorry

lemma list_diff_map_subset {α β : Type*} {f : α → β} {l₁ l₂ : list α} :
  l₁.map f \ l₂.map f ⊆ (l₁ \ l₂).map f := sorry

lemma snoc_eq_snoc_iff {α : Type*} {xs ys : list α} {x y : α} :
  xs ++ [x] = ys ++ [y] ↔ xs = ys ∧ x = y := sorry

lemma length_snoc {α : Type*} {xs : list α} {x : α} :
  (xs ++ [x]).length = xs.length.succ := sorry

lemma length_lt_length_append_cons {α : Type*} {xs ys : list α} {y : α} :
  xs.length < (xs ++ y :: ys).length := sorry

lemma length_lt_length_append_snoc {α : Type*} {xs ys : list α} {y : α} :
  xs.length < (xs ++ (ys ++ [y])).length := sorry

lemma length_lt_length_snoc {α : Type*} {xs : list α} {x : α} :
  xs.length < (xs ++ [x]).length := sorry

lemma length_lt_length_snoc₂ {α : Type*} {xs : list α} {x y : α} :
  xs.length < ((xs ++ [x]) ++ [y]).length := sorry

lemma exi_ge_of_set_inf {P : ℕ → Prop} {n : ℕ}
  (h : {n : ℕ | P n}.infinite) : ∃ (k : ℕ), n ≤ k ∧ P k := sorry

lemma exi_set_infinite_of_forall_exi {α β : Type*} {P : α → β → Prop}
  (h₁ : (set.univ : set α).infinite) (h₂ : (set.univ : set β).finite)
  (h₃ : ∀ (a : α), ∃ (b : β), P a b) : ∃ (b : β), {a : α | P a b}.infinite := sorry

lemma exi_set_infinite_of_forall_exi_nat {α : Type*} [fintype α] {P : ℕ → α → Prop}
  (h : ∀ (n : ℕ), ∃ (a : α), P n a) :
  ∃ (a : α), {n : ℕ | P n a}.infinite := sorry

lemma fintype_subtype_of_set_finite {α : Type*} {P : α → Prop}
  (h : {x : α | P x}.finite) : fintype {x : α // P x} := sorry

lemma set_finite_of_set_equiv_finite' {α β : Type*} (e : α ≃ β) {P : α → Prop}
  (h : {x : α | P x}.finite) : {y : β | P (e.inv_fun y)}.finite := sorry

lemma set_finite_of_set_equiv_finite {α β : Type*} (e : α ≃ β) {P : β → Prop}
  (h : {x : α | P (e.to_fun x)}.finite) : {y : β | P y}.finite := sorry

lemma abs_le_finite {d : ℤ} : {a : ℤ | |a| ≤ d}.finite := sorry

lemma abs_sub_le_finite {c d : ℤ} : {a : ℤ | |a - c| ≤ d}.finite := sorry

lemma nat_find_le_find_of_imp {P Q : ℕ → Prop}
  {hh₁ : ∃ (n : ℕ), P n} {hh₂ : ∃ (n : ℕ), Q n}
  (h : ∀ (n : ℕ), Q n → P n) : nat.find hh₁ ≤ nat.find hh₂ := sorry

lemma nat_Inf_le_Inf_of_subset {P Q : set ℕ}
  (h₁ : Q.nonempty) (h₂ : Q ⊆ P) : Inf P ≤ Inf Q := sorry

lemma finset_card_insert_erase_eq {α : Type*} {s : finset α} {x y : α}
  (h₁ : x ∈ s) (h₂ : y ∉ s) : (insert y (s.erase x)).card = s.card := sorry

[Eric Wieser]

Have you library_search'd all of them to no avail?

[Kyle Miller]

I think it would be helpful to take small chunks of thematically related lemmas (say 5-ish) and repost them to help focus discussion -- you have a lot of lemmas to take in all at once! (Having thematic chunks for PRs would be helpful for review too.)

[Kyle Miller]

The set.finite -> fintype definition is docs#set.finite.fintype

noncomputable def fintype_subtype_of_set_finite {α : Type*} {P : α → Prop}
  (h : {x : α | P x}.finite) : fintype {x : α // P x} := h.fintype

[Kyle Miller]

For the set.finite lemmas, they should generally be made by defining some fintype instances (or just definitions) and then making use of them. For example, once #14136 is merged,

instance {d : ℤ} : fintype {a : ℤ | |a| ≤ d} := sorry

lemma abs_le_finite {d : ℤ} : {a : ℤ | |a| ≤ d}.finite := set.finite_of_fintype _

(And at this point, you probably don't need the lemma since {a : ℤ | |a| ≤ d}.finite_of_fintype would likely suffice.)

[Floris van Doorn]

I see a couple things already in mathlib: docs#function.iterate_add_apply and docs#list.take_append_drop

[Patrick Johnson]

Ok, removed statements for which library_search found a result. Also, removed set.finite lemmas (I will refactor them later).
I'll try to make PRs as small as possible, yes.

nat

lemma nat.sub_lt_of_lt {a b c : ℕ} (h : a < b) : a - c < b := sorry

lemma nat.mul_add_mod {a b c : ℕ} : (a * b + c) % b = c % b := sorry

lemma nat.mul_add_mod_of_lt {a b c : ℕ} (h : c < b) : (a * b + c) % b = c := sorry

lemma nat.exists_mul (x y : ℕ) :
  ∃ (a b : ℕ), x / y = a ∧ x % y = b ∧ x = y * a + b := sorry

lemma nat.pred_eq_self_iff {n : ℕ} : n.pred = n ↔ n = 0 := sorry

lemma nat.Inf_le_Inf_of_subset {P Q : set ℕ}
  (h₁ : Q.nonempty) (h₂ : Q ⊆ P) : Inf P ≤ Inf Q := sorry

lemma nat.exists_ge_of_set_inf {P : ℕ → Prop} {n : ℕ}
  (h : {n : ℕ | P n}.infinite) : ∃ (k : ℕ), n ≤ k ∧ P k := sorry

list

lemma list.nth_le_eq_iff {α : Type*}
  {l : list α} {n : ℕ} {x : α} {h} :
  l.nth_le n h = x ↔ l.nth n = some x := sorry

lemma list.some_nth_le_eq {α : Type*}
  {l : list α} {n : ℕ} {h} :
  some (l.nth_le n h) = l.nth n := sorry

lemma list.nodup_iff {α : Type*} {l : list α} :
  l.nodup ↔ ∀ (i j : ℕ), i < j → j < l.length → l.nth i ≠ l.nth j := sorry

lemma list.length_le_fintype_card_of_nodup {α : Type*} [fintype α] {l : list α}
  (h : l.nodup) : l.length ≤ fintype.card α := sorry

lemma list.nth_cons_of_pos {α : Type*} {l : list α} {x : α} {n : ℕ}
  (h : 0 < n) : (x :: l).nth n = l.nth (n - 1) := sorry

lemma list.length_snoc {α : Type*} {l : list α} {x : α} :
  (l ++ [x]).length = l.length + 1 := sorry

lemma list.dedup_singleton {α : Type*} {x : α} : [x].dedup = [x] := sorry

lemma list.length_dedup_le {α : Type*} {l : list α} :
  l.dedup.length ≤ l.length := sorry

lemma list.length_dedup_append_le {α : Type*} {l₁ l₂ : list α} :
  ((l₁ ++ l₂).dedup).length ≤ l₁.dedup.length + l₂.dedup.length := sorry

lemma list.dedup_dup_cons {α : Type*} {l : list α} {x : α} :
  (x :: x :: l).dedup = (x :: l).dedup := sorry

lemma list.length_dedup_cons_le_of_mem {α : Type*} {l : list α} {x : α}
  (h : x ∈ l) : (x :: l).dedup.length ≤ l.length := sorry

lemma list.eq_tail_of_cons_eq {α : Type*} {l₁ l₂ : list α} {x : α}
  (h : x :: l₁ = l₂) : l₁ = l₂.tail := sorry

lemma list.length_dedup_lt_of_dup {α : Type*} {l : list α}
  (h : ¬l.nodup) : l.dedup.length < l.length := sorry

lemma list.dedup_length_eq_length_iff {α : Type*} {l : list α} :
  l.dedup.length = l.length ↔ l.nodup := sorry

lemma list.count_erase {α : Type*} {l : list α} {x : α} :
  (l.erase x).count x = l.count x - (ite (x ∈ l) 1 0) := sorry

lemma list.mem_diff_iff {α : Type*} {l₁ l₂ : list α} {x : α} :
  x ∈ l₁ \ l₂ ↔ l₂.count x < l₁.count x := sorry

lemma list.sum_count_cons_diff_singleton {α : Type*} {l : list α} {x : α} :
  ∑ (a : α) in l.to_finset \ {x}, (x :: l).count a =
  ∑ (a : α) in l.to_finset \ {x}, l.count a := sorry

lemma list.sum_count_cons {α : Type*} {l : list α} {x : α} :
  ∑ (a : α) in l.to_finset, (x :: l).count a =
  ∑ (a : α) in l.to_finset, l.count a + ite (x ∈ l) 1 0 := sorry

lemma list.length_eq_sum_count {α : Type*} {l : list α} :
  l.length = ∑ (x : α) in l.to_finset, l.count x := sorry

lemma list.sum_union_eq_sum {α : Type*} {l : list α} {s : finset α} :
  ∑ (x : α) in l.to_finset ∪ s, l.count x =
  ∑ (x : α) in l.to_finset, l.count x := sorry

lemma list.length_le_length_of_count_le_count {α : Type*}
  {l₁ l₂ : list α} (h : ∀ (a : α), l₁.count a ≤ l₂.count a) :
  l₁.length ≤ l₂.length := sorry

lemma list.count_map_eq_length_filter {α β : Type*} {f : α → β}
  {l : list α} {y : β} :
  (l.map f).count y = (l.filter (λ (x : α), f x = y)).length := sorry

lemma list.count_filter_eq_ite {α : Type*} {P : α → Prop}
  {l : list α} {x : α} : (l.filter P).count x = ite (P x) (l.count x) 0 := sorry

lemma list.diff_map_subset {α β : Type*} {f : α → β} {l₁ l₂ : list α} :
  l₁.map f \ l₂.map f ⊆ (l₁ \ l₂).map f := sorry

lemma list.snoc_eq_snoc_iff {α : Type*} {xs ys : list α} {x y : α} :
  xs ++ [x] = ys ++ [y] ↔ xs = ys ∧ x = y := sorry

lemma list.length_lt_length_append_cons {α : Type*} {xs ys : list α} {y : α} :
  xs.length < (xs ++ y :: ys).length := sorry

lemma list.length_lt_length_snoc {α : Type*} {xs : list α} {x : α} :
  xs.length < (xs ++ [x]).length := sorry

lemma list.length_lt_length_snoc₂ {α : Type*} {xs : list α} {x y : α} :
  xs.length < ((xs ++ [x]) ++ [y]).length := sorry

finset

lemma finset.union_singleton {α : Type*} {s : finset α} {x : α} :
  s ∪ {x} = insert x s := sorry

lemma finset.sum_le_sum_of_le {α : Type*} {f g : α → ℕ} {s : finset α}
  (h : ∀ (a : α), a ∈ s → f a ≤ g a) :
  ∑ (a : α) in s, f a ≤ ∑ (a : α) in s, g a := sorry

lemma finset.card_insert_erase_eq {α : Type*} {s : finset α} {x y : α}
  (h₁ : x ∈ s) (h₂ : y ∉ s) : (insert y (s.erase x)).card = s.card := sorry

set

lemma set.exists_infinite_of_forall_exi {α β : Type*} {P : α → β → Prop}
  (h₁ : (set.univ : set α).infinite) (h₂ : (set.univ : set β).finite)
  (h₃ : ∀ (a : α), ∃ (b : β), P a b) : ∃ (b : β), {a : α | P a b}.infinite := sorry

lemma set.exists_infinite_of_forall_exists_nat {α : Type*} [fintype α]
  {P : ℕ → α → Prop} (h : ∀ (n : ℕ), ∃ (a : α), P n a) :
  ∃ (a : α), {n : ℕ | P n a}.infinite := sorry

function

lemma function.iterate_add_apply' {α : Type*} {f : α → α} {x : α} {m n : ℕ} :
  (f^[m + n]) x = (f^[n]) ((f^[m]) x) := sorry

lemma function.iterate_add_mul_eq_of_add_eq {α : Type*}
  {f : α → α} {x : α} {n m d : ℕ}
  (h : (f^[n + d]) x = (f^[n]) x) :
  (f^[n + d * m]) x = (f^[n]) x := sorry

lemma function.iterate_mul_eq_of_eq {α : Type*} {f : α → α} {x : α} {m d : ℕ}
  (h : (f^[d]) x = x) : (f^[d * m]) x = x := sorry

[Patrick Johnson]

Floris van Doorn said:

I see a couple things already in mathlib: docs#function.iterate_add_apply and docs#list.take_append_drop

I know about function.iterate_add_apply, but my version has flipped addition operands. I often find myself using rw add_comm before rw function.iterate_add_apply, so maybe we should have the other version too for rewriting?

[Eric Wieser]

nat.exists_mul looks kind of silly; what's the point in having an existential of the form ∃ (a b : ℕ), f x = a ∧ g y = b ∧ p a b vs the lemma just being p (f x) (g y)?

[Mario Carneiro]

list.length_dedup_le is covered by dedup_sublist and sublist_length_le

[Mario Carneiro]

same for list.length_dedup_append_le - I would want that to be presented as (l1 ++ l2).dedup <+ l1.dedup ++ l2.dedup

[Mario Carneiro]

list.length_dedup_append_le should be (x :: l).dedup.length = l.dedup.length or possibly (x :: l).dedup = l.dedup if the order of dedup works out

[Mario Carneiro]

list.length_dedup_lt_of_dup is an iff

[Mario Carneiro]

list.length_dedup_lt_of_dup looks too specific to be a general purpose lemma, unless that sum was a definition

[Mario Carneiro]

list.length_dedup_lt_of_dup can be stated without the sum

[Mario Carneiro]

list.sum_union_eq_sum is more flexible if the lhs uses s instead of l.to_finset ∪ s with an assumption that l \sub s. Also the rhs is l.length given the previous lemma

[Mario Carneiro]

another way to get to list.length_le_length_of_count_le_count is to map the two lists to multisets, since the hypothesis is saying that multiset.mk l1 <= multiset.mk l2 and this implies the length fact

[Mario Carneiro]

list.count_map_eq_length_filter should be stated in terms of countp. In fact this theorem generalizes to countp on both sides, which would be list.countp_map

[Mario Carneiro]

list.diff_map_subset should be upgraded to sublist if true (not 100% sure)

[Mario Carneiro]

list.length_lt_length_snoc₂ seems unnecessary, it's just two applications of the previous lemma

[Mario Carneiro]

finset.card_insert_erase_eq is just theorems about insert and erase stuck together + pred_succ

[Mario Carneiro]

set.exists_infinite_of_forall_exi: I'm pretty sure there is a way to write those hypotheses as just infinite α

[Mario Carneiro]

it might also be better to generalize β to a finset

[Mario Carneiro]

set.exists_infinite_of_forall_exists_nat is just the specialization of the previous lemma, it does not seem necessary

[Mario Carneiro]

function.iterate_mul_eq_of_eq and function.iterate_add_mul_eq_of_add_eq seem to be encouraging the wrong kind of buildup of the expression. I would instead say that f^[d * m] = (f^[d])^[m], and if f x = x then f^[n] x = x. For function.iterate_add_mul_eq_of_add_eq you can rewrite (f^[n + d]) x to (f^[d]) ((f^[n]) x) and then it's just the same as the other one

[Mario Carneiro]

nat.exists_ge_of_set_inf is an iff (with the n quantifier in the right place)

[Patrick Johnson]

Sorry for the late response. I was busy last week.

list.length_dedup_append_le should be (x :: l).dedup.length = l.dedup.length or possibly (x :: l).dedup = l.dedup if the order of dedup works out

I guess you mean length_dedup_cons_le_of_mem instead? I think it can also be stated as dedup_cons_eq_self_iff_mem, because it's an iff.

list.length_dedup_lt_of_dup is an iff

Then length_dedup_lt_of_dup is just list.dedup_eq_self, so I guess it's redundant.

list.length_dedup_lt_of_dup looks too specific to be a general purpose lemma, unless that sum was a definition
list.length_dedup_lt_of_dup can be stated without the sum

Copy-paste artifact? Which lemmas are you referring to?

nat.exists_mul looks kind of silly; what's the point in having an existential of the form ∃ (a b : ℕ), f x = a ∧ g y = b ∧ p a b vs the lemma just being p (f x) (g y)?

I personally find it handy for rewriting, because I often use generalize after obtain ... := nat.div_add_mod _ so that the proof state looks cleaner. But I understand it's probably not suitable for mathlib.

[Patrick Johnson]

I will open one PR at a time. Here is the PR for list.nodup_iff: #14371