feat(data/multiset,...): card_eq_one

based on #200

Author: digama0

algebra/group_power.lean

@@ -308,6 +308,10 @@ by rw [add_monoid.smul_eq_mul', add_monoid.smul_eq_mul', mul_assoc]
 theorem add_monoid.mul_smul_assoc [semiring α] (a b : α) (n : ℕ) : n • (a * b) = n • a * b :=
 by rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_assoc]
 
+theorem neg_one_pow_eq_or {R} [ring R] : ∀ n : ℕ, (-1 : R)^n = 1 ∨ (-1 : R)^n = -1
+| 0     := by simp
+| (n+1) := by cases neg_one_pow_eq_or n; simp [pow_succ, h]
+
 theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, n •ℤ a = n * a
 | (n : ℕ) := by simp [add_monoid.smul_eq_mul]
 | -[1+ n] := by simp [add_monoid.smul_eq_mul, -add_comm, add_mul]

data/list/basic.lean

@@ -71,6 +71,9 @@ theorem exists_mem_of_length_pos : ∀ {l : list α}, 0 < length l → ∃ a, a
 theorem length_pos_iff_exists_mem {l : list α} : 0 < length l ↔ ∃ a, a ∈ l :=
 ⟨exists_mem_of_length_pos, λ ⟨a, h⟩, length_pos_of_mem h⟩
 
+theorem length_eq_one {l : list α} : length l = 1 ↔ ∃ a, l = [a] :=
+⟨match l with [a], _ := ⟨a, rfl⟩ end, λ ⟨a, e⟩, e.symm ▸ rfl⟩
+
 theorem mem_split {a : α} {l : list α} (h : a ∈ l) : ∃ s t : list α, l = s ++ a :: t :=
 begin
   induction l with b l ih; simp at h; cases h with h h,

data/multiset.lean

@@ -49,6 +49,7 @@ instance : has_emptyc (multiset α) := ⟨0⟩
 instance : inhabited (multiset α)  := ⟨0⟩
 
 @[simp] theorem coe_nil_eq_zero : (@nil α : multiset α) = 0 := rfl
+@[simp] theorem empty_eq_zero : (∅ : multiset α) = 0 := rfl
 
 /- cons -/
 
@@ -345,6 +346,11 @@ quot.induction_on s $ λ l, length_pos_iff_exists_mem
   strong_induction_on t ih
 using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf card⟩]}
 
+theorem strong_induction_eq {p : multiset α → Sort*}
+  (s : multiset α) (H) : @strong_induction_on _ p s H =
+    H s (λ t h, @strong_induction_on _ p t H) :=
+by rw [strong_induction_on]
+
 @[elab_as_eliminator] lemma case_strong_induction_on {p : multiset α → Prop}
   (s : multiset α) (h₀ : p 0) (h₁ : ∀ a s, (∀t ≤ s, p t) → p (a :: s)) : p s :=
 multiset.strong_induction_on s $ assume s,
@@ -366,6 +372,11 @@ ne_of_gt (lt_cons_self _ _)
 ⟨λ h, mem_of_le h (mem_singleton_self _),
  λ h, let ⟨t, e⟩ := exists_cons_of_mem h in e.symm ▸ cons_le_cons _ (zero_le _)⟩
 
+theorem card_eq_one {s : multiset α} : card s = 1 ↔ ∃ a, s = a::0 :=
+⟨quot.induction_on s $ λ l h,
+  (list.length_eq_one.1 h).imp $ λ a, congr_arg coe,
+ λ ⟨a, e⟩, e.symm ▸ rfl⟩
+
 /- add -/
 
 /-- The sum of two multisets is the lift of the list append operation.

logic/basic.lean

@@ -150,6 +150,9 @@ iff.intro and.left (λ ha, ⟨ha, h ha⟩)
 theorem and_iff_right_of_imp {a b : Prop} (h : b → a) : (a ∧ b) ↔ b :=
 iff.intro and.right (λ hb, ⟨h hb, hb⟩)
 
+lemma and.congr_right_iff : (a ∧ b ↔ a ∧ c) ↔ (a → (b ↔ c)) :=
+⟨λ h ha, by simp [ha] at h; exact h, and_congr_right⟩
+
 /- or -/
 
 theorem or_of_or_of_imp_of_imp (h₁ : a ∨ b) (h₂ : a → c) (h₃ : b → d) : c ∨ d :=