feat(data/finset): add list.to_finset theorems

Author: spl

data/finset.lean

@@ -588,6 +588,12 @@ multiset.to_finset_eq n
 @[simp] theorem mem_to_finset {a : α} {l : list α} : a ∈ l.to_finset ↔ a ∈ l :=
 mem_erase_dup
 
+@[simp] theorem to_finset_nil : to_finset (@nil α) = ∅ :=
+rfl
+
+@[simp] theorem to_finset_cons {a : α} {l : list α} : to_finset (a :: l) = insert a (to_finset l) :=
+finset.eq_of_veq $ by by_cases h : a ∈ l; simp [finset.insert_val', multiset.erase_dup_cons, h]
+
 end list
 
 namespace finset
@@ -995,3 +1001,20 @@ list.to_finset_eq (sort_nodup r s) ▸ eq_of_veq (sort_eq r s)
 end sort
 
 end finset
+
+namespace list
+variable [decidable_eq α]
+
+theorem to_finset_card_of_nodup {l : list α} : l.nodup → l.to_finset.card = l.length :=
+begin
+  induction l,
+  case list.nil { simp },
+  case list.cons : _ _ ih {
+    intros nd,
+    simp at nd,
+    simp [finset.card_insert_of_not_mem ((not_iff_not_of_iff mem_to_finset).mpr nd.1),
+          ih nd.2]
+  }
+end
+
+end list

data/list/basic.lean

@@ -2656,6 +2656,10 @@ theorem pw_filter_eq_self {l : list α} : pw_filter R l = l ↔ pairwise R l :=
   rw [pw_filter_cons_of_pos (ball.imp_left (pw_filter_subset l) al), IH p],
 end⟩
 
+@[simp] theorem pw_filter_idempotent {l : list α} :
+  pw_filter R (pw_filter R l) = pw_filter R l :=
+pw_filter_eq_self.mpr (pairwise_pw_filter l)
+
 theorem forall_mem_pw_filter (neg_trans : ∀ {x y z}, R x z → R x y ∨ R y z)
   (a : α) (l : list α) : (∀ b ∈ pw_filter R l, R a b) ↔ (∀ b ∈ l, R a b) :=
 ⟨begin
@@ -2999,6 +3003,9 @@ theorem nodup_erase_dup : ∀ l : list α, nodup (erase_dup l) := pairwise_pw_fi
 
 theorem erase_dup_eq_self {l : list α} : erase_dup l = l ↔ nodup l := pw_filter_eq_self
 
+@[simp] theorem erase_dup_idempotent {l : list α} : erase_dup (erase_dup l) = erase_dup l :=
+pw_filter_idempotent
+
 theorem erase_dup_append (l₁ l₂ : list α) : erase_dup (l₁ ++ l₂) = l₁ ∪ erase_dup l₂ :=
 begin
   induction l₁ with a l₁ IH; simp, rw ← IH,