refactor(*): move theorems and do minor polishing

Author: avigad

data/bool.lean

@@ -4,9 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura, Jeremy Avigad
 -/
 
--- TODO(Jeremy): these used to be proved by rec_simp. Write a special tactic for these, or
--- get auto or super to do them.
-
 namespace bool
 
 -- TODO(Jeremy): is this right?

data/list/basic.lean

@@ -84,8 +84,7 @@ attribute [simp] concat
 
 @[simp] theorem concat_nil (a : α) : concat [] a = [a] := rfl
 
-@[simp] theorem concat_cons (a b : α) (l : list α) :
-  concat (a :: l) b  = a :: concat l b := rfl
+@[simp] theorem concat_cons (a b : α) (l : list α) : concat (a :: l) b  = a :: concat l b := rfl
 
 @[simp] theorem concat_ne_nil (a : α) (l : list α) : concat l a ≠ [] :=
 by induction l; intro h; contradiction

data/list/sort.lean

@@ -7,43 +7,6 @@ Insertion sort and merge sort.
 -/
 import data.list.perm
 
--- TODO(Jeremy): move this
-
-namespace nat
-
-theorem add_pos_left {m : ℕ} (h : m > 0) (n : ℕ) : m + n > 0 :=
-calc
-  m + n > 0 + n : nat.add_lt_add_right h n
-    ... = n     : nat.zero_add n
-    ... ≥ 0     : zero_le n
-
-theorem add_pos_right (m : ℕ) {n : ℕ} (h : n > 0) : m + n > 0 :=
-begin rw add_comm, exact add_pos_left h m end
-
-theorem add_pos_iff_pos_or_pos (m n : ℕ) : m + n > 0 ↔ m > 0 ∨ n > 0 :=
-iff.intro
-  begin
-    intro h,
-    cases m with m,
-    {simp [zero_add] at h, exact or.inr h},
-    exact or.inl (succ_pos _)
-  end
-  begin
-    intro h, cases h with mpos npos,
-    { apply add_pos_left mpos },
-    apply add_pos_right _ npos
-  end
-
-theorem succ_le_succ_iff (m n : ℕ) : succ m ≤ succ n ↔ m ≤ n :=
-⟨le_of_succ_le_succ, succ_le_succ⟩
-
-theorem lt_succ_iff_le (m n : ℕ) : m < succ n ↔ m ≤ n :=
-succ_le_succ_iff m n
-
-end nat
-
-
-
 namespace list
 
 section sorted

data/nat/basic.lean

@@ -9,8 +9,6 @@ import logic.basic
 
 universe u
 
-open tactic
-
 namespace nat
 
 protected theorem eq_mul_of_div_eq_right {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) : 
@@ -27,6 +25,35 @@ by rw mul_comm; exact nat.div_eq_iff_eq_mul_right H H'
 
 protected theorem eq_mul_of_div_eq_left {a b c : ℕ} (H1 : b ∣ a) (H2 : a / b = c) : 
   a = c * b := 
-by rw [mul_comm, nat.eq_mul_of_div_eq_right H1 H2] 
+by rw [mul_comm, nat.eq_mul_of_div_eq_right H1 H2]
+
+theorem add_pos_left {m : ℕ} (h : m > 0) (n : ℕ) : m + n > 0 :=
+calc
+  m + n > 0 + n : nat.add_lt_add_right h n
+    ... = n     : nat.zero_add n
+    ... ≥ 0     : zero_le n
+
+theorem add_pos_right (m : ℕ) {n : ℕ} (h : n > 0) : m + n > 0 :=
+begin rw add_comm, exact add_pos_left h m end
+
+theorem add_pos_iff_pos_or_pos (m n : ℕ) : m + n > 0 ↔ m > 0 ∨ n > 0 :=
+iff.intro
+  begin
+    intro h,
+    cases m with m,
+    {simp [zero_add] at h, exact or.inr h},
+    exact or.inl (succ_pos _)
+  end
+  begin
+    intro h, cases h with mpos npos,
+    { apply add_pos_left mpos },
+    apply add_pos_right _ npos
+  end
+
+theorem succ_le_succ_iff (m n : ℕ) : succ m ≤ succ n ↔ m ≤ n :=
+⟨le_of_succ_le_succ, succ_le_succ⟩
+
+theorem lt_succ_iff_le (m n : ℕ) : m < succ n ↔ m ≤ n :=
+succ_le_succ_iff m n
 
 end nat

logic/basic.lean

@@ -56,6 +56,15 @@ theorem implies_intro (h : a) (h₂ : b) : a := h
 
 theorem implies_false_iff (a : Prop) : (a → false) ↔ ¬ a := iff.rfl
 
+theorem implies_and_iff (p q r : Prop) : (p → q ∧ r) ↔ (p → q) ∧ (p → r) :=
+iff.intro (λ h, ⟨λ hp, (h hp).left, λ hp, (h hp).right⟩) (λ h hp, ⟨h.left hp, h.right hp⟩)
+
+theorem and_implies_iff (p q r : Prop) : (p ∧ q → r) ↔ (p → q → r) :=
+iff.intro (λ h hp hq, h ⟨hp, hq⟩) (λ h ⟨hp, hq⟩, h hp hq)
+
+theorem iff_def (p q : Prop) : (p ↔ q) ↔ (p → q) ∧ (q → p) :=
+⟨ λh, ⟨h.1, h.2⟩, λ ⟨h₁, h₂⟩, ⟨h₁, h₂⟩ ⟩
+
 /- not -/
 
 theorem {u} not_elim {A : Sort u} (H1 : ¬a) (H2 : a) : A := absurd H2 H1
@@ -358,6 +367,9 @@ section bounded_quantifiers
 universe variable u
 variables {α : Type u} {r p q : α → Prop} {b : Prop}
 
+theorem bexists_def {α : Type u} (p q : α → Prop) : (∃ x (h : p x), q x) ↔ ∃ x, p x ∧ q x :=
+⟨λ ⟨x, px, qx⟩, ⟨x, px, qx⟩, λ ⟨x, px, qx⟩, ⟨x, px, qx⟩⟩
+
 theorem bexists.elim {b : Prop} (h : ∃ x : α, ∃ h : p x, q x) (h' : ∀ (a : α), p a → q a → b) :
   b :=
 exists.elim h (λ a h₁, exists.elim h₁ (h' a))

tactic/finish.lean

@@ -29,17 +29,7 @@ declare_trace auto.done
 declare_trace auto.finish
 
 -- TODO(Jeremy): move these
-theorem implies_and_iff (p q r : Prop) : (p → q ∧ r) ↔ (p → q) ∧ (p → r) :=
-iff.intro (λ h, ⟨λ hp, (h hp).left, λ hp, (h hp).right⟩) (λ h hp, ⟨h.left hp, h.right hp⟩)
 
-theorem curry_iff (p q r : Prop) : (p ∧ q → r) ↔ (p → q → r) :=
-iff.intro (λ h hp hq, h ⟨hp, hq⟩) (λ h ⟨hp, hq⟩, h hp hq)
-
-theorem iff_def (p q : Prop) : (p ↔ q) ↔ (p → q) ∧ (q → p) :=
-⟨ λh, ⟨h.1, h.2⟩, λ ⟨h₁, h₂⟩, ⟨h₁, h₂⟩ ⟩
-
-theorem {u} bexists_def {α : Type u} (p q : α → Prop) : (∃ x (h : p x), q x) ↔ ∃ x, p x ∧ q x :=
-⟨λ ⟨x, px, qx⟩, ⟨x, px, qx⟩, λ ⟨x, px, qx⟩, ⟨x, px, qx⟩⟩
 
 namespace tactic