refactor(library): move basic theorems to init, remove sorry's from algebra/simplifier.lean

library/algebra/simplifier.lean

@@ -16,13 +16,12 @@ namespace neg_helper
     lemma neg_mul1 : (- a) * b = - (a * b) := eq.symm !algebra.neg_mul_eq_neg_mul
     lemma neg_mul2 : a * (- b) = - (a * b) := eq.symm !algebra.neg_mul_eq_mul_neg
     lemma sub_def : a - b = a + (- b) := rfl
-    lemma
 end neg_helper
 
 namespace ac
 
 -- iff
-lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
+attribute eq_self_iff_true [simp]
 
 -- neg
 attribute neg_helper.neg_mul1 [simp]
@@ -54,7 +53,7 @@ end ac
 namespace som
 
 -- iff
-lemma eq_iff_true [simp] {A : Type} (a : A) : a = a ↔ true := sorry
+attribute eq_self_iff_true [simp]
 
 -- neg
 attribute neg_helper.neg_mul1 [simp]

library/init/logic.lean

@@ -142,7 +142,7 @@ namespace ne
   assume (H₁ : b = a), H (H₁⁻¹)
 end ne
 
-theorem false.of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl
+theorem false_of_ne {A : Type} {a : A} : a ≠ a → false := ne.irrefl
 
 section
   open eq.ops
@@ -322,6 +322,35 @@ attribute iff.refl [refl]
 attribute iff.symm [symm]
 attribute iff.trans [trans]
 
+theorem not_not_intro (Ha : a) : ¬¬a :=
+assume Hna : ¬a, Hna Ha
+
+theorem not_true : (¬ true) ↔ false :=
+iff_false_intro (not_not_intro trivial)
+
+theorem not_false_iff : (¬ false) ↔ true :=
+iff_true_intro not_false
+
+theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
+iff.intro false_of_ne false.elim
+
+theorem eq_self_iff_true {A : Type} (a : A) : (a = a) ↔ true :=
+iff_true_intro rfl
+
+theorem heq_self_iff_true {A : Type} (a : A) : (a == a) ↔ true :=
+iff_true_intro (heq.refl a)
+
+theorem iff_not_self (a : Prop) : (a ↔ ¬a) ↔ false :=
+iff_false_intro (λ H,
+   have H' : ¬a, from (λ Ha, (iff.mp H Ha) Ha),
+   H' (iff.mpr H H'))
+
+theorem true_iff_false : (true ↔ false) ↔ false :=
+iff_false_intro (λ H, iff.mp H trivial)
+
+theorem false_iff_true : (false ↔ true) ↔ false :=
+iff_false_intro (λ H, iff.mpr H trivial)
+
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 intro : ∀ (a : A), P a → Exists P
 

library/logic/connectives.lean

@@ -48,9 +48,6 @@ theorem not.elim {A : Type} (H1 : ¬a) (H2 : a) : A := absurd H2 H1
 
 theorem not.intro (H : a → false) : ¬a := H
 
-theorem not_not_intro (Ha : a) : ¬¬a :=
-assume Hna : ¬a, Hna Ha
-
 theorem not.mto {a b : Prop} : (a → b) → ¬b → ¬a := imp.left
 
 theorem not_imp_not_of_imp {a b : Prop} : (a → b) → ¬b → ¬a := not.mto
@@ -65,16 +62,9 @@ theorem not_not_em : ¬¬(a ∨ ¬a) :=
 assume not_em : ¬(a ∨ ¬a),
 not_em (or.inr (not.mto or.inl not_em))
 
-theorem not_true [simp] : ¬ true ↔ false :=
-iff_false_intro (not_not_intro trivial)
-
-theorem not_false_iff [simp] : ¬ false ↔ true :=
-iff_true_intro not_false
-
 theorem not_iff_not (H : a ↔ b) : ¬a ↔ ¬b :=
 iff.intro (not.mto (iff.mpr H)) (not.mto (iff.mp H))
 
-
 /- and -/
 
 definition not_and_of_not_left (b : Prop) : ¬a → ¬(a ∧ b) :=

library/logic/identities.lean

@@ -102,23 +102,3 @@ theorem exists_of_not_forall_not {A : Type} {p : A → Prop} [D : ∀x, decidabl
     [D' : decidable (∃x, p x)] (H : ¬∀x, ¬ p x) :
   ∃x, p x :=
 by_contradiction (imp.syl H forall_not_of_not_exists)
-
-theorem ne_self_iff_false {A : Type} (a : A) : (a ≠ a) ↔ false :=
-iff.intro false.of_ne false.elim
-
-theorem eq_self_iff_true [simp] {A : Type} (a : A) : (a = a) ↔ true :=
-iff_true_intro rfl
-
-theorem heq_self_iff_true [simp] {A : Type} (a : A) : (a == a) ↔ true :=
-iff_true_intro (heq.refl a)
-
-theorem iff_not_self [simp] (a : Prop) : (a ↔ ¬a) ↔ false :=
-iff_false_intro (λH,
-   have H' : ¬a, from (λHa, (mp H Ha) Ha),
-   H' (iff.mpr H H'))
-
-theorem true_iff_false [simp] : (true ↔ false) ↔ false :=
-not_true ▸ (iff_not_self true)
-
-theorem false_iff_true [simp] : (false ↔ true) ↔ false :=
-not_false_iff ▸ (iff_not_self false)