feat(library/data/finset): add all combinator theorems

library/data/finset/basic.lean

@@ -57,6 +57,9 @@ definition has_decidable_eq [instance] [h : decidable_eq A] : decidable_eq (fins
      | decidable.inr n := decidable.inr (λ e : ⟦l₁⟧ = ⟦l₂⟧, absurd (quot.exact e) n)
      end)
 
+definition singleton (a : A) : finset A :=
+to_finset_of_nodup [a] !nodup_singleton
+
 definition mem (a : A) (s : finset A) : Prop :=
 quot.lift_on s (λ l, a ∈ elt_of l)
  (λ l₁ l₂ (e : l₁ ~ l₂), propext (iff.intro
@@ -66,12 +69,15 @@ quot.lift_on s (λ l, a ∈ elt_of l)
 infix `∈` := mem
 notation a ∉ b := ¬ mem a b
 
-definition mem_of_mem_list {a : A} {l : nodup_list A} : a ∈ elt_of l → a ∈ ⟦l⟧ :=
+theorem mem_of_mem_list {a : A} {l : nodup_list A} : a ∈ elt_of l → a ∈ ⟦l⟧ :=
 λ ainl, ainl
 
-definition mem_list_of_mem {a : A} {l : nodup_list A} : a ∈ ⟦l⟧ → a ∈ elt_of l :=
+theorem mem_list_of_mem {a : A} {l : nodup_list A} : a ∈ ⟦l⟧ → a ∈ elt_of l :=
 λ ainl, ainl
 
+theorem mem_singleton (a : A) : a ∈ singleton a :=
+mem_of_mem_list !mem_cons
+
 definition decidable_mem [instance] [h : decidable_eq A] : ∀ (a : A) (s : finset A), decidable (a ∈ s) :=
 λ a s, quot.rec_on_subsingleton s
   (λ l, match list.decidable_mem a (elt_of l) with
@@ -107,6 +113,9 @@ quot.lift_on s
 theorem card_empty : card (@empty A) = 0 :=
 rfl
 
+theorem card_singleton (a : A) : card (singleton a) = 1 :=
+rfl
+
 /- insert -/
 section insert
 variable [h : decidable_eq A]
@@ -280,4 +289,22 @@ theorem empty_intersection (s : finset A) : ∅ ∩ s = ∅ :=
 calc ∅ ∩ s = s ∩ ∅ : intersection.comm
        ... = ∅     : intersection_empty
 end intersection
+
+/- upto -/
+section upto
+definition upto (n : nat) : finset nat :=
+to_finset_of_nodup (list.upto n) (nodup_upto n)
+
+theorem card_upto : ∀ n, card (upto n) = n :=
+list.length_upto
+
+theorem lt_of_mem_upto {n a : nat} : a ∈ upto n → a < n :=
+list.lt_of_mem_upto
+
+theorem mem_upto_succ_of_mem_upto {n a : nat} : a ∈ upto n → a ∈ upto (succ n) :=
+list.mem_upto_succ_of_mem_upto
+
+theorem mem_upto_of_lt {n a : nat} : a < n → a ∈ upto n :=
+list.mem_upto_of_lt
+end upto
 end finset

library/data/finset/comb.lean

@@ -7,10 +7,11 @@ Author: Leonardo de Moura
 
 Combinators for finite sets
 -/
-import data.finset.basic
+import data.finset.basic logic.identities
 open list quot subtype decidable perm function
 
 namespace finset
+section map
 variables {A B : Type}
 variable [h : decidable_eq B]
 include h
@@ -22,4 +23,46 @@ quot.lift_on s
 
 theorem map_empty (f : A → B) : map f ∅ = ∅ :=
 rfl
+end map
+
+section all
+variables {A : Type}
+definition all (s : finset A) (p : A → Prop) : Prop :=
+quot.lift_on s
+  (λ l, all (elt_of l) p)
+  (λ l₁ l₂ p, foldr_eq_of_perm (λ a₁ a₂ q, propext !and.left_comm) p true)
+
+theorem all_empty (p : A → Prop) : all ∅ p = true :=
+rfl
+
+theorem of_mem_of_all {p : A → Prop} {a : A} {s : finset A} : a ∈ s → all s p → p a :=
+quot.induction_on s (λ l i h, list.of_mem_of_all i h)
+
+theorem all_implies {p q : A → Prop} {s : finset A} : all s p → (∀ x, p x → q x) → all s q :=
+quot.induction_on s (λ l h₁ h₂, list.all_implies h₁ h₂)
+
+variable [h : decidable_eq A]
+include h
+
+theorem all_union {p : A → Prop} {s₁ s₂ : finset A} :  all s₁ p → all s₂ p → all (s₁ ∪ s₂) p :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ a₁ a₂, all_union a₁ a₂)
+
+theorem all_of_all_union_left {p : A → Prop} {s₁ s₂ : finset A} : all (s₁ ∪ s₂) p → all s₁ p :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ a, list.all_of_all_union_left a)
+
+theorem all_of_all_union_right {p : A → Prop} {s₁ s₂ : finset A} : all (s₁ ∪ s₂) p → all s₂ p :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ a, list.all_of_all_union_right a)
+
+theorem all_insert_of_all {p : A → Prop} {a : A} {s : finset A} : p a → all s p → all (insert a s) p :=
+quot.induction_on s (λ l h₁ h₂, list.all_insert_of_all h₁ h₂)
+
+theorem all_erase_of_all {p : A → Prop} (a : A) {s : finset A}: all s p → all (erase a s) p :=
+quot.induction_on s (λ l h, list.all_erase_of_all a h)
+
+theorem all_intersection_of_all_left {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₁ p → all (s₁ ∩ s₂) p :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_left _ h)
+
+theorem all_intersection_of_all_right {p : A → Prop} {s₁ : finset A} (s₂ : finset A) : all s₂ p → all (s₁ ∩ s₂) p :=
+quot.induction_on₂ s₁ s₂ (λ l₁ l₂ h, list.all_intersection_of_all_right _ h)
+end all
 end finset