refactor(library): rename theorems "iff.flip_sign -> not_iff_not_of_iff" and "decidable_iff_equiv -> decidable_of_decidable_of_iff"

library/data/int/order.lean

@@ -431,8 +431,8 @@ have aux : Πx, decidable (0 ≤ x), from
       iff.intro
         (assume H1, nat_abs_nonneg_eq H1)
         (assume H1, H1 ▸ of_nat_nonneg (nat_abs x)),
-    decidable_iff_equiv _ (iff.symm H),
-decidable_iff_equiv !aux (iff.symm (le_iff_sub_nonneg a b))
+    decidable_of_decidable_of_iff _ (iff.symm H),
+decidable_of_decidable_of_iff !aux (iff.symm (le_iff_sub_nonneg a b))
 
 definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
 definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _

library/data/list/basic.lean

@@ -203,7 +203,7 @@ rec_on l
                 (assume Heq, absurd Heq Hne)
                 (assume Hp,  absurd Hp Hn),
             have H2 : ¬x ∈ h::l, from
-              iff.elim_right (iff.flip_sign !mem.cons) H1,
+              iff.elim_right (not_iff_not_of_iff !mem.cons) H1,
             decidable.inr H2)))
 
 -- Find
@@ -225,7 +225,7 @@ rec_on l
    (take y l,
       assume iH : ¬x ∈ l → find x l = length l,
       assume P₁ : ¬x ∈ y::l,
-      have P₂ : ¬(x = y ∨ x ∈ l), from iff.elim_right (iff.flip_sign !mem.cons) P₁,
+      have P₂ : ¬(x = y ∨ x ∈ l), from iff.elim_right (not_iff_not_of_iff !mem.cons) P₁,
       have P₃ : ¬x = y ∧ ¬x ∈ l, from (iff.elim_left not_or_iff_not_and_not P₂),
       calc
         find x (y::l) = if x = y then 0 else succ (find x l) : !find.cons

library/data/prod/thms.lean

@@ -23,7 +23,7 @@ namespace prod
       iff.intro
         (assume H, H ▸ and.intro rfl rfl)
         (assume H, and.elim H (assume H₄ H₅, equal H₄ H₅)),
-    decidable_iff_equiv _ (iff.symm H₃)
+    decidable_of_decidable_of_iff _ (iff.symm H₃)
 
   -- ### flip operation
 

library/data/subtype.lean

@@ -29,5 +29,5 @@ namespace subtype
   take a1 a2 : {x | P x},
     have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
       iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
-    decidable_iff_equiv _ (iff.symm H1)
+    decidable_of_decidable_of_iff _ (iff.symm H1)
 end subtype

library/data/sum.lean

@@ -50,13 +50,13 @@ namespace sum
           (take b₂,
             have H₃ : (inl B a₁ = inr A b₂) ↔ false,
               from iff.intro inl_neq_inr (assume H₄, !false.rec H₄),
-            show decidable (inl B a₁ = inr A b₂), from decidable_iff_equiv _ (iff.symm H₃)))
+            show decidable (inl B a₁ = inr A b₂), from decidable_of_decidable_of_iff _ (iff.symm H₃)))
       (take b₁, show decidable (inr A b₁ = s₂), from
         rec_on s₂
           (take a₂,
             have H₃ : (inr A b₁ = inl B a₂) ↔ false,
               from iff.intro (assume H₄, inl_neq_inr (H₄⁻¹)) (assume H₄, !false.rec H₄),
-            show decidable (inr A b₁ = inl B a₂), from decidable_iff_equiv _ (iff.symm H₃))
+            show decidable (inr A b₁ = inl B a₂), from decidable_of_decidable_of_iff _ (iff.symm H₃))
           (take b₂, show decidable (inr A b₁ = inr A b₂), from
             decidable.rec_on (H₂ b₁ b₂)
               (assume Heq : b₁ = b₂, decidable.inl (Heq ▸ rfl))

library/init/logic.lean

@@ -200,11 +200,6 @@ namespace iff
 
   definition mp' := @elim_right
 
-  definition flip_sign (H₁ : a ↔ b) : ¬a ↔ ¬b :=
-  intro
-    (assume (Hna : ¬ a) (Hb : b), absurd (elim_right H₁ Hb) Hna)
-    (assume (Hnb : ¬ b) (Ha : a), absurd (elim_left H₁ Ha) Hnb)
-
   definition refl (a : Prop) : a ↔ a :=
   intro (assume H, H) (assume H, H)
 
@@ -226,6 +221,11 @@ namespace iff
   iff.intro (λ Ha, H ▸ Ha) (λ Hb, H⁻¹ ▸ Hb)
 end iff
 
+definition not_iff_not_of_iff (H₁ : a ↔ b) : ¬a ↔ ¬b :=
+iff.intro
+ (assume (Hna : ¬ a) (Hb : b), absurd (iff.elim_right H₁ Hb) Hna)
+ (assume (Hnb : ¬ b) (Ha : a), absurd (iff.elim_left H₁ Ha) Hnb)
+
 theorem of_iff_true (H : a ↔ true) : a :=
 iff.mp (iff.symm H) trivial
 
@@ -278,15 +278,20 @@ namespace decidable
     (assume H1 : p, H1)
     (assume H1 : ¬p, false.rec _ (H H1))
 
-  definition decidable_iff_equiv (Hp : decidable p) (H : p ↔ q) : decidable q :=
-  rec_on Hp
-    (assume Hp : p,   inl (iff.elim_left H Hp))
-    (assume Hnp : ¬p, inr (iff.elim_left (iff.flip_sign H) Hnp))
-
-  definition decidable_eq_equiv (Hp : decidable p) (H : p = q) : decidable q :=
-  decidable_iff_equiv Hp (iff.of_eq H)
 end decidable
 
+section
+  variables {p q : Prop}
+  open decidable
+  definition  decidable_of_decidable_of_iff (Hp : decidable p) (H : p ↔ q) : decidable q :=
+  decidable.rec_on Hp
+    (assume Hp : p,   inl (iff.elim_left H Hp))
+    (assume Hnp : ¬p, inr (iff.elim_left (not_iff_not_of_iff H) Hnp))
+
+  definition  decidable_of_decidable_of_eq (Hp : decidable p) (H : p = q) : decidable q :=
+  decidable_of_decidable_of_iff Hp (iff.of_eq H)
+end
+
 section
   variables {p q : Prop}
   open decidable (rec_on inl inr)

library/init/nat.lean

@@ -146,7 +146,7 @@ namespace nat
     (λ hr, le.of_lt hr)
 
   definition le.is_decidable_rel [instance] : decidable_rel le :=
-  λ a b, decidable_iff_equiv _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
+  λ a b, decidable_of_decidable_of_iff _ (iff.intro le.of_eq_or_lt eq_or_lt_of_le)
 
   definition le.rec_on {a : nat} {P : nat → Prop} {b : nat} (H : a ≤ b) (H₁ : P a) (H₂ : ∀ b, a < b → P b) : P b :=
   begin

library/logic/connectives.lean

@@ -176,7 +176,7 @@ section
 
   theorem if_congr [H₁ : decidable c₁] {t₁ t₂ e₁ e₂ : A} (Hc : c₁ ↔ c₂) (Ht : t₁ = t₂)
       (He : e₁ = e₂) :
-    (if c₁ then t₁ else e₁) = (@ite c₂ (decidable.decidable_iff_equiv H₁ Hc) A t₂ e₂) :=
-  have H2 [visible] : decidable c₂, from (decidable.decidable_iff_equiv H₁ Hc),
+    (if c₁ then t₁ else e₁) = (@ite c₂ (decidable_of_decidable_of_iff H₁ Hc) A t₂ e₂) :=
+  have H2 [visible] : decidable c₂, from (decidable_of_decidable_of_iff H₁ Hc),
   if_congr_aux Hc Ht He
 end

tests/lean/run/sum_bug.lean

@@ -49,13 +49,13 @@ rec_on s1
       (take b2,
         have H3 : (inl B a1 = inr A b2) ↔ false,
           from iff.intro inl_neq_inr (assume H4, false.elim H4),
-        show decidable (inl B a1 = inr A b2), from decidable_iff_equiv _ (iff.symm H3)))
+        show decidable (inl B a1 = inr A b2), from decidable_of_decidable_of_iff _ (iff.symm H3)))
   (take b1, show decidable (inr A b1 = s2), from
     rec_on s2
       (take a2,
         have H3 : (inr A b1 = inl B a2) ↔ false,
           from iff.intro (assume H4, inl_neq_inr (symm H4)) (assume H4, false.elim H4),
-        show decidable (inr A b1 = inl B a2), from decidable_iff_equiv _ (iff.symm H3))
+        show decidable (inr A b1 = inl B a2), from decidable_of_decidable_of_iff _ (iff.symm H3))
       (take b2, show decidable (inr A b1 = inr A b2), from H2 b1 b2))
 
 end sum