Lifting quotient predicate when defining reciprocal

Stream: new members

[Jackson Brough]

Hello everyone! I have started working through Terence Tao's Analysis 1 in Lean, and I was able to use quotient types to construct the integers, but I'm having trouble defining reciprocal for the rational numbers.

The general problem seems to be utilizing a predicate over a quotient type in a proof about the underlying type. I thought it might be possible to use Quotient.rec to construct a function from some $a : ℚ$ to the set of functions which send a proof that $a$ is nonzero to $ℚ$ (making use of the fact that $a$ is nonzero to properly flip the fraction). That actually worked for the function definition, but now I'm very stuck on the proof that the function respects the equivalence relation. Is it possible to make use of predicates in this way when lifting a function to a quotient?

Two other people have had very similar questions:

• https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Quotients.20and.20passing.20an.20inequality.20around
• https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/.E2.9C.94.20Case.20distinction.20in.20definition

Here's a #mwe. I converted the quotient integers I'm using to mathlib's integers, and it should be easy to convert back if I can get the mathlib version working.

import Mathlib

def NonZeroInteger := {a : ℤ // a ≠ 0}

def RationalEquivalent : (ℤ × NonZeroInteger) → (ℤ × NonZeroInteger) → Prop
  | (a, ⟨b, _⟩), (c, ⟨d, _⟩) => a * d = c * b

theorem RationalEquivalent.reflexive : ∀ a, RationalEquivalent a a :=
  λ _ => rfl

theorem RationalEquivalent.symmetric : ∀ {a b}, RationalEquivalent a b → RationalEquivalent b a := by
  intro (a, ⟨b, _⟩) (c, ⟨d, _⟩) h_ab_cd
  have h_ab_cd' : a * d = c * b := h_ab_cd
  show c * b = a * d
  exact Eq.symm h_ab_cd'

theorem RationalEquivalent.transitive : ∀ {a b c}, RationalEquivalent a b → RationalEquivalent b c → RationalEquivalent a c := by
  intro (a, ⟨b, b_nonzero⟩) (c, ⟨d, d_nonzero⟩) (e, ⟨f, _⟩)
  intro (h_ab_cd : a * d = c * b) (h_cd_ef : c * f = e * d)
  show a * f = e * b
  cases Int.decEq c 0 with
  | isTrue c_zero =>
    have ad_zero := c_zero ▸ h_ab_cd
    rw [Int.zero_mul] at ad_zero
    have a_zero := Or.resolve_right (Int.eq_zero_or_eq_zero_of_mul_eq_zero ad_zero) d_nonzero
    have ed_zero := c_zero ▸ h_cd_ef
    rw [Int.zero_mul] at ed_zero
    have e_zero := Or.resolve_right (Int.eq_zero_or_eq_zero_of_mul_eq_zero ed_zero.symm) d_nonzero
    simp [a_zero, e_zero, Int.mul_zero, Int.zero_mul]
  | isFalse c_nonzero =>
    have h_equal := calc
      (c * d) * (a * f) = (c * f) * (a * d) := by simp [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]
      _ = (e * d) * (a * d) := congrArg (. * _) h_cd_ef
      _ = (e * d) * (c * b) := congrArg (_ * .) h_ab_cd
      _ = (c * d) * (e * b) := by simp [Int.mul_assoc, Int.mul_comm, Int.mul_left_comm]
    have cd_nonzero := Int.mul_ne_zero c_nonzero d_nonzero
    exact Int.eq_of_mul_eq_mul_left cd_nonzero h_equal

theorem RationalEquivalent.is_equivalence : Equivalence RationalEquivalent :=
  { refl := RationalEquivalent.reflexive, symm := RationalEquivalent.symmetric, trans := RationalEquivalent.transitive }

instance instanceHasEquivRationalEquivalent : HasEquiv (Int × NonZeroInteger) where
  Equiv := RationalEquivalent

instance instanceSetoidRationalEquivalent : Setoid (Int × NonZeroInteger) where
  r := RationalEquivalent
  iseqv := RationalEquivalent.is_equivalence

@[simp] def RationalEquivalent.definition : (x ≈ y) = RationalEquivalent x y := rfl

def Rational := Quotient instanceSetoidRationalEquivalent

instance : OfNat Rational n where
  ofNat := ⟦(Int.ofNat n, ⟨1, by decide⟩)⟧

def reciprocal (a : Rational) : a ≠ 0 → Rational :=
  let reciprocal' :=
    λ (a : ℤ × NonZeroInteger) =>
    λ (a_nonzero : ⟦a⟧ ≠ (0 : Rational)) =>
    have a1_nonzero : a.1 ≠ 0 := by
    { intro h
      have := calc
        a.1 * 1 = a.1 := Int.mul_one _
        _ = 0 := h
        _ = 0 * a.2.val := (Int.zero_mul _).symm
      exact a_nonzero (Quotient.sound this) }
    -- Couldn't get it to type check without being overly explicit
    Quotient.mk instanceSetoidRationalEquivalent (a.2.val, ({ val := a.1, property := a1_nonzero } : NonZeroInteger))
  Quotient.recOn a reciprocal' <| by
  -- How to close this goal? Use `Quotient.hrecOn`? Applying `heq_of_eq` doesn't seem to work
  skip

[Johan Commelin]

I think that whichever solution you reach, you'll always be happy to extract your

  let reciprocal' :=
    λ (a : ℤ × NonZeroInteger) =>
    λ (a_nonzero : ⟦a⟧ ≠ (0 : Rational)) =>
    have a1_nonzero : a.1 ≠ 0 := by
    { intro h
      have := calc
        a.1 * 1 = a.1 := Int.mul_one _
        _ = 0 := h
        _ = 0 * a.2.val := (Int.zero_mul _).symm
      exact a_nonzero (Quotient.sound this) }

into a helper lemma.

[Johan Commelin]

And maybe you even want to phrase it as an iff?

[Kevin Buzzard]

The "party line" would be to define reciprocal on all rationals, and define the reciprocal of zero to be zero. If you don't like that then try it anyway, and define your reciprocal using it. Does this approach fix the problem in your case or just move it?

[Kevin Buzzard]

PS I would be tempted to make NonZeroInteger an abbrev rather than a def because it's just an abbreviation rather than something you want to develop an API for

[Kevin Buzzard]

theorem RationalEquivalent.symmetric : ∀ {a b}, RationalEquivalent a b → RationalEquivalent b a := by
  intro (a, ⟨b, _⟩) (c, ⟨d, _⟩) h_ab_cd
  exact h_ab_cd.symm

or even

theorem RationalEquivalent.symmetric {a b} (h : RationalEquivalent a b) : RationalEquivalent b a :=
  h.symm

[Kevin Buzzard]

Here's an approach which makes it less painful:

def prereciprocal (x : ℤ × NonZeroInteger) : Rational :=
  if h : x.1 = 0 then 0 else ⟦(x.2.1, ⟨x.1, h⟩)⟧

@[simp]
lemma prereciprocal_zero (x : ℤ × NonZeroInteger) (hx : x.1 = 0) : prereciprocal x = 0 := by
  simp [prereciprocal, hx]

@[simp]
lemma prereciprocal_ne_zero (x : ℤ × NonZeroInteger) (hx : x.1 ≠ 0) :
    prereciprocal x = ⟦(x.2.1, ⟨x.1, hx⟩)⟧ := by
  simp [prereciprocal, hx]

def reciprocal : Rational → Rational :=
  Quotient.lift prereciprocal <| by
  intro ⟨a1, a2, ha⟩ ⟨b1, b2, hb⟩ (h : a1 * b2 = b1 * a2)
  rcases eq_or_ne a1 0 <;> rcases eq_or_ne b1 0 <;> simp_all
  rw [Quotient.eq]
  change a2 * b1  = b2 * a1
  polyrith

[Kevin Buzzard]

And if you like you can call that reciprocal' and define your reciprocal to be my reciprocal but with the random extra hypothesis that the input isn't 0.

[Kevin Buzzard]

theorem RationalEquivalent.transitive : ∀ {a b c}, RationalEquivalent a b → RationalEquivalent b c → RationalEquivalent a c := by
  intro (a, ⟨b, b_nonzero⟩) (c, ⟨d, d_nonzero⟩) (e, ⟨f, _⟩)
  intro (h_ab_cd : a * d = c * b) (h_cd_ef : c * f = e * d)
  apply mul_left_cancel₀ d_nonzero
  polyrith

[Jackson Brough]

Sorry it took me so long to reply! Thank you both for your suggestions, it's always really great to get code/proof suggestions from people with more experience. The transitivity and reciprocal'-respects proofs are both very clean.

[Jackson Brough]

I defined reciprocal using the "party line" method, and this definitely works. I am encouraged by the prereciprocal_ne_zero theorem; I think this should make proving theorems about reciprocal relatively painless.

[Jackson Brough]

Part of my motivation for asking was that I have another case with essentially the same problem. I'm trying to define conversions between the natural numbers and the positive integers (constructed using quotients) and then showing that they are inverses of each other. I tried to apply the same case split method but using an Option instead of zero, and this almost works. The issue is in the "_left_inverse" proofs at the very bottom. It's a bit silly, but is there a reason the simplifier can't close the goals?

[Jackson Brough]

Unfortunately my code sample is pretty large. I did replace any proofs longer than two lines with sorry for brevity. If I can get the last two proofs to type check, I'm satisfied with this approach, but is it possible to avoid the case split entirely?

[Jackson Brough]

import Mathlib

def IntegerEquivalent : (ℕ × ℕ) → (ℕ × ℕ) → Prop
  | (n, m), (k, l) => n + l = k + m

theorem IntegerEquivalent.reflexive : ∀ x, IntegerEquivalent x x :=
  λ _ => rfl

theorem IntegerEquivalent.symmetric : ∀ {x y}, IntegerEquivalent x y → IntegerEquivalent y x :=
  Eq.symm

theorem IntegerEquivalent.transitive : ∀ {x y z}, IntegerEquivalent x y → IntegerEquivalent y z → IntegerEquivalent x z
  | (a, b), (c, d), (e, f), (h₁ : a + d = c + b), (h₂ : c + f = e + d) => by
    apply add_left_cancel (a := (c + d))
    linarith

theorem IntegerEquivalent.is_equivalence : Equivalence IntegerEquivalent :=
  { refl := IntegerEquivalent.reflexive, symm := IntegerEquivalent.symmetric, trans := IntegerEquivalent.transitive }

instance instanceHasEquivIntegerEquivalent : HasEquiv (ℕ × ℕ) where
  Equiv := IntegerEquivalent

instance instanceSetoidIntegerEquivalent : Setoid (ℕ × ℕ) where
  r := IntegerEquivalent
  iseqv := IntegerEquivalent.is_equivalence

def Integer := Quotient instanceSetoidIntegerEquivalent

namespace Integer

@[simp]
def ofNat (n : ℕ) : Integer := ⟦(n, 0)⟧

def ofNat_definition : ofNat n = Quotient.mk instanceSetoidIntegerEquivalent (n, 0) := rfl

instance Zero : Integer := ⟦(0, 0)⟧

instance One : Integer := ⟦(1, 0)⟧

instance : OfNat Integer n where
  ofNat := ⟦(n, 0)⟧

instance : Coe Nat Integer := ⟨ofNat⟩

theorem ofNat_injective : Function.Injective ofNat := by
  intro a b h
  rw [← Nat.add_zero a, Quotient.exact h, Nat.add_zero]

def add : Integer → Integer → Integer :=
  let add' := λ ((n, m) : ℕ × ℕ) ((k, l) : ℕ × ℕ) => (n + k, m + l)
  Quotient.map₂ add' <| by
  sorry

instance : Add Integer where add := add

@[simp] theorem add_definition : add a b = a + b := rfl

theorem add_commutative : ∀ (a b : Integer), a + b = b + a := sorry

theorem add_zero : ∀ (a : Integer), a + 0 = a := sorry

theorem zero_add (a : Integer) : 0 + a = a := by
  rw [add_commutative, add_zero]

def LessEqual (a b : Integer) : Prop := ∃ (n : ℕ), a + ↑n = b

instance : LE Integer where
  le := LessEqual

theorem ofNat_nonnegative (n : ℕ) : ↑n ≥ (0 : Integer) :=
  Exists.intro n (zero_add n)

abbrev NonNegativeInteger := {a : Integer // a ≥ 0}

-- Didn't find any Nat lemmas that looked like this
theorem Nat.left_greater_equal_of_add_right_less_equal {n m k l : ℕ} : n + m = k + l → m ≤ l → n ≥ k := sorry

theorem Nat.right_greater_equal_of_add_left_less_equal {n m k l : ℕ} : n + m = k + l → n ≤ k → m ≥ l := sorry

-- Important stuff starts here

def preToNatural' : ℕ × ℕ → Option ℕ
  | (n, m) => if n ≥ m then some (n - m) else none

@[simp]
theorem preToNatural_none (x : ℕ × ℕ) (h : x.1 < x.2) : preToNatural' x = none := by
  have := not_le_of_gt h
  simp [preToNatural', not_le_of_gt h]

@[simp]
theorem preToNatural_some (x : ℕ × ℕ) (h : x.1 ≥ x.2) : preToNatural' x = some (x.1 - x.2) := by
  simp [preToNatural', h]

def toNatural' : Integer → Option ℕ :=
  Quotient.lift preToNatural' <| by
  intro (n, m) (k, l) (h : n + l = k + m)
  simp [preToNatural', preToNatural_none, preToNatural_some]
  cases Decidable.em (m ≤ n)
  <;> cases Decidable.em (l ≤ k)
  <;> simp_all only [preToNatural', preToNatural_none, preToNatural_some, ite_true, ite_false]
  case inl.inl hnm hkl =>
    apply congrArg some
    apply Nat.add_right_cancel (m := m + l)
    rw [← Nat.add_assoc, Nat.sub_add_cancel, h, ← Nat.sub_add_cancel hkl,
      Nat.add_assoc (k - l) l m, Nat.add_comm l m, Nat.sub_add_cancel]
    exact hkl
    exact hnm
  case inl.inr hnm hkl =>
    rw [Nat.add_comm k m] at h
    have := Nat.right_greater_equal_of_add_left_less_equal h.symm hnm
    exact absurd this hkl
  case inr.inl hnm hkl =>
    rw [Nat.add_comm n l] at h
    have := Nat.right_greater_equal_of_add_left_less_equal h hkl
    exact absurd this hnm

def toNatural : NonNegativeInteger → ℕ
  | (⟨a, a_nonnegative⟩) =>
    let o := toNatural' a
    have : Option.isSome o = true := by
    { have ⟨n, hn⟩ := a_nonnegative
      rw [zero_add, ofNat] at hn
      simp [Option.isSome, toNatural', o]
      rw [← hn, Quotient.lift_mk]
      rw [preToNatural']
      have : n ≥ 0 := Nat.zero_le n
      simp only [this, sub_zero, ite_true, Option.isSome] }
    match o with
    | some n => n

def fromNatural (n : ℕ) : NonNegativeInteger :=
  ⟨n, ofNat_nonnegative n⟩

theorem fromNatural_toNatural_left_inverse : Function.LeftInverse toNatural fromNatural := by
  intro n
  simp [fromNatural, ofNat, toNatural, toNatural']
  have := preToNatural_some (n, 0) (Nat.zero_le n)
  simp only [sub_zero] at this
  simp [this]

theorem toNatural_fromNatural_left_inverse : Function.LeftInverse fromNatural toNatural := by
  unfold Function.LeftInverse
  intro a
  simp [toNatural, toNatural']