How can I define the inverse of a real number?

Stream: new members

[Kent Van Vels]

I am implementing a home-brew version of the real numbers as the equivalence classes of Cauchy sequence of rational numbers. I need to define real number (non-zero) inversion $x:\mathbb{R} \mapsto 1/x$. I am having trouble figuring out how to implement this. What follows is a Minimal (non) Working example.

import tactic

--import data.real.basic
import data.nat.basic
import data.rat.order

abbreviation seqQ := ℕ → ℚ

namespace seqQ

--inversion
protected def inv : seqQ → seqQ := λ u0 : seqQ, λ n : ℕ,  (u0 n)⁻¹
instance : has_inv seqQ := ⟨seqQ.inv⟩
@[simp] lemma inv_def (u0 : seqQ) : u0⁻¹ = λ n : ℕ, (u0 n)⁻¹ := rfl
@[simp] lemma inv_def_at (u0 :seqQ) (n : ℕ) : (u0⁻¹) n =  (u0 n)⁻¹  := rfl

end seqQ

def isCauchy : seqQ → Prop :=
begin
  intro u,
  exact (∀ (ε : ℚ) (ε_pos : 0 < ε), ∃ N : ℕ, ∀ (n ≥ N) (m≥ N), abs(u n - u m) ≤ ε )
end

@[simp] lemma isCauchy_def (u : seqQ) :
isCauchy u ↔ (∀ (ε : ℚ) (ε_pos : 0 < ε), ∃ N : ℕ, ∀ (n ≥ N) (m≥ N), abs(u n - u m) ≤ ε ) := iff.rfl

namespace cauchyQ
open seqQ

structure cauchyQ :=
mk :: (z : seqQ) (h1 : isCauchy z)


protected def inv (q0 : cauchyQ)  : cauchyQ  :=
begin


  --I can only define this for a cauchy sequence that doesn't converge to zero,
-- i.e. if have the following hypothesis.
  have h0 : ∃ (ε : ℚ ) (ε_pos : 0 < ε) (N : ℕ), ∀ n ≥ N, |q0.z n| ≥ ε := by sorry,

  --But, of course, some cauchy sequences of rationals do converge to zero
 -- so I think the correct thing to do is follow convention that 0^{-1} = 0.

  --What do I need here?  I suspect I need something about
  --the non-computabilty or non-decidability of  equivalence relation r,

  sorry,
end

instance : has_inv cauchyQ := ⟨cauchyQ.inv⟩

end cauchyQ

namespace R
open cauchyQ
open seqQ

def r (u v : cauchyQ) : Prop
:= ∀ (ε : ℚ) (ε_pos : 0 < ε), (∃ N : ℕ, (∀ (n ≥ N), abs (u.z n - v.z n) ≤ ε) )

@[simp] lemma r_def (u0 u1 : cauchyQ) :
  r u0 u1 ↔ ∀ (ε : ℚ ) (ε_pos : 0 < ε), ∃ N : ℕ, (∀ (n ≥ N) , abs (u0.z n - u1.z n) ≤ ε) := iff.rfl

def r_refl : reflexive r := sorry
def r_symm : symmetric r := sorry
def r_trans : transitive r := sorry


instance mysetoidR : setoid cauchyQ := ⟨r,r_refl,r_symm,r_trans⟩

@[simp] lemma equiv_def (u0 u1 : cauchyQ) : (u0 ≈ u1) ↔ r u0 u1 := iff.rfl

def R := quotient R.mysetoidR



def inv_aux (z: cauchyQ) : R :=
begin
  exact ⟦z⁻¹⟧,
end

def inv : R→ R := quotient.lift inv_aux
begin
  --I am pretty sure I know what to do here.
  sorry,
end

Any help and direction is appreciated.

[Kent Van Vels]

I should mention that I tried to use a dite on the eqiovalamce/non-equivalence to zero of a Cauchy sequence and I got an an error about missing decidable_le or decidable_nonneg.

I stripped out this attempt in my MWE.

[Jireh Loreaux]

You can just case split on your needed hypothesis and its negation with tactic#by_cases (this uses excluded middle under the hood when necessary, which is where the noncomputability will creep in).

[Jireh Loreaux]

You can also use tactic#classical to make everything decidable within a proof, or else open classical at some point earlier in the file.

[Kent Van Vels]

Ok I will attempt to use by_cases. I will write again if I have more questions. Thank you.

[Kent Van Vels]

Thanks, I think I got it to work.

[Junyan Xu]

If you want to see how it's done in mathlib:

• a lim_zero predicate was introduced for docs#cau_seq.inv.
• open_locale classical is called before the definition of src#cau_seq.completion.Cauchy.has_inv.

[Kent Van Vels]

@Junyan Xu Thanks. I have been looking at the mathlib docs but I couldn't make sense of much without exploring a bunch of other things. I appreciate the insight and the suggestion. I will take another look. Thanks.