Unbundle ApproxZero and ApproxZeroIff

Our Series Approx instances downstream approximate only the germ of
functions, and thus don't satisfy this.

Author: girving

Interval/Approx.lean

@@ -23,6 +23,9 @@ export Approx (approx)
 /-- `0 : A` is conservative, and `0` only approximates `0` -/
 class ApproxZero (A R : Type) [Zero R] [Zero A] [Approx A R] where
   approx_zero : approx (0 : A) (0 : R)
+
+/-- `0 : A` only approximates `0` -/
+class ApproxZeroIff (A R : Type) [Zero R] [Zero A] [Approx A R] where
   approx_zero_imp : ∀ (x : R), approx (0 : A) x → x = 0
 
 /-- `1 : A` is conservative -/
@@ -87,20 +90,19 @@ export ApproxSMul (approx_smul)
 
 attribute [simp] approx_zero approx_one
 
-lemma approx_zero_iff [Approx A R] [Zero A] [Zero R] [ApproxZero A R] (x : R) :
+lemma approx_zero_iff [Approx A R] [Zero A] [Zero R] [ApproxZero A R] [ApproxZeroIff A R] (x : R) :
     approx (0 : A) x ↔ x = 0 := by
   constructor
-  · apply ApproxZero.approx_zero_imp
+  · apply ApproxZeroIff.approx_zero_imp
   · intro x0; rw [x0]; exact approx_zero
 
 /-!
 ## Everything approximates itself
 -/
 
 instance : Approx R R where approx x y := x = y
-instance [Zero R] : ApproxZero R R where
-  approx_zero := by simp only [approx]
-  approx_zero_imp x a := by simp only [approx] at a; simp only [a]
+instance [Zero R] : ApproxZero R R where approx_zero := by simp only [approx]
+instance [Zero R] : ApproxZeroIff R R where approx_zero_imp x a := by rw [approx] at a; rw [a]
 instance [One R] : ApproxOne R R where approx_one := by simp only [approx]
 instance [Neg R] : ApproxNeg R R where approx_neg := by simp only [approx]; aesop
 instance [Add R] : ApproxAdd R R where approx_add := by simp only [approx]; aesop

Interval/Box/Basic.lean

@@ -122,9 +122,8 @@ lemma smul_def {x : Interval} {z : Box} : x • z = ⟨x * z.re, x * z.im⟩ :=
 lemma mem_approx_iff_ext {z : ℂ} {w : Box} : approx w z ↔ approx w.re z.re ∧ approx w.im z.im := by
   rfl
 
-instance : ApproxZero Box ℂ where
-  approx_zero := by simp [mem_approx_iff_ext]
-  approx_zero_imp x a := by simpa only [approx_zero_iff] using a
+instance : ApproxZero Box ℂ where approx_zero := by simp [mem_approx_iff_ext]
+instance : ApproxZeroIff Box ℂ where approx_zero_imp x a := by simpa only [approx_zero_iff] using a
 instance : ApproxOne Box ℂ where approx_one := by simp [mem_approx_iff_ext]
 
 /-- `star` is conservative -/

Interval/Fixed.lean

@@ -249,6 +249,8 @@ instance : ApproxNan (Fixed s) ℝ where
 
 instance : ApproxZero (Fixed s) ℝ where
   approx_zero := by simp only [approx, Fixed.val_zero, or_true]
+
+instance : ApproxZeroIff (Fixed s) ℝ where
   approx_zero_imp x a := by simpa only [Fixed.approx_zero_iff] using a
 
 /-- If we're not `nan`, `approx` is a singleton -/

Interval/Floating/Basic.lean

@@ -154,6 +154,8 @@ instance : ApproxNan Floating ℝ where
 
 instance : ApproxZero Floating ℝ where
   approx_zero := by simp only [approx, val_zero, or_true]
+
+instance : ApproxZeroIff Floating ℝ where
   approx_zero_imp x a := by simpa only [approx_zero_iff] using a
 
 /-- `1 = 1` -/

Interval/Interval/Basic.lean

@@ -137,9 +137,8 @@ instance : ApproxNan Interval ℝ where
   approx_nan a := by simp only [approx, lo_nan, hi_nan, true_or]
 
 -- Basic `approx` lemmas
-instance : ApproxZero Interval ℝ where
-  approx_zero := by simp only [approx_zero]
-  approx_zero_imp x a := by simpa only [approx_zero] using a
+instance : ApproxZero Interval ℝ where approx_zero := by simp only [approx_zero]
+instance : ApproxZeroIff Interval ℝ where approx_zero_imp x a := by simpa only [approx_zero] using a
 instance : ApproxOne Interval ℝ where approx_one := by simp only [approx_one]
 
 /-- `x.lo = nan` if `x = nan` -/