Case distinction in definition

Stream: general

[Julian Külshammer]

For teaching purposes I would like to define my own version of the rational numbers and prove that they form a field. I have managed to set them up and prove that they form a commutative ring (adapting the construction of the integers from the natural numbers in Kevin's PhD course). However, I struggle to define the multiplicative inverse. I was not able to make the necessary case distinction depending on whether the rational number is zero (in which case the inverse should be 0) and the reasonable case. Here is an mwe.

import data.int.basic
import tactic.linear_combination
import tactic.linarith

structure int_plane_non_zero :=
(fst : ℤ) (snd : ℤ) (non_zero : snd ≠ 0)

def S (r s : int_plane_non_zero) : Prop :=
r.1 * s.2 = s.1 * r.2

lemma S_def (r s : int_plane_non_zero) :
S r s ↔ r.1 * s.2 = s.1 * r.2 := by refl

lemma S_refl : reflexive S :=
λ r, by rw S_def

lemma S_symm : symmetric S :=
begin
  intros r s hrs,
  rw S_def at *,
  exact hrs.symm,
end

lemma S_trans : transitive S :=
begin
  intros r s t hrs hst,
  rw S_def at *,
  rw ← mul_right_inj' (s.non_zero),
  linear_combination t.snd * hrs + r.snd * hst,
end

lemma S_equiv : equivalence S :=
begin
  exact ⟨S_refl, S_symm, S_trans⟩,
end

instance s : setoid (int_plane_non_zero) :=
{ r := S,
  iseqv := S_equiv }

notation `myrat` := quotient s

attribute [instance] s

namespace «myrat»

lemma equiv_def (r s : int_plane_non_zero) :
r ≈ s ↔ r.1 * s.2 = s.1 * r.2 :=
begin
  refl
end

instance : has_zero myrat :=
{ zero := ⟦⟨0,1,by linarith⟩⟧ }

instance : has_inv myrat :=
{ inv := _ }

end «myrat»

[Patrick Massot]

You didn't provide a has_zero instance, so it isn't a good start to do this case distinction.

[Julian Külshammer]

Fixed.

[Patrick Massot]

Maybe add

instance : has_zero myrat := ⟨⟦(⟨0, 1, by norm_num⟩ : int_plane_non_zero)⟧⟩

instance : has_inv myrat :=
{ inv := quotient.lift (λ x : int_plane_non_zero, (if h : x.1 = 0 then (0 : myrat) else ⟦⟨x.2, x.1, h⟩⟧ : myrat)) begin

end }

[Patrick Massot]

Of course insisting on the non-zero condition in int_plane_nonzero is a footgun, especially since you plan to define the inverse of zero in myrat anyway.

[Patrick Massot]

And the missing proof would start with

rintros ⟨n, d, hd⟩ ⟨n', d', hd'⟩ (h : n*d' = n'*d),
dsimp,
split_ifs,

[Julian Külshammer]

Thank you. What definition would you suggest instead for avoiding the non-zero condition?

[Patrick Massot]

Leaving out this condition I guess.

[Patrick Massot]

Except that everybody would be equivalent to (0, 0)...

[Patrick Massot]

So I should go to bed instead.

[Patrick Massot]

Have fun!