## Stream: general

### Topic: Case distinction in definition

#### Julian Külshammer (Jun 16 2022 at 20:05):

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 (Jun 16 2022 at 20:10):

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

Fixed.

#### Patrick Massot (Jun 16 2022 at 20:12):

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 (Jun 16 2022 at 20:13):

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 (Jun 16 2022 at 20:17):

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


#### Julian Külshammer (Jun 16 2022 at 20:18):

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

#### Patrick Massot (Jun 16 2022 at 20:20):

Leaving out this condition I guess.

#### Patrick Massot (Jun 16 2022 at 20:23):

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

#### Patrick Massot (Jun 16 2022 at 20:23):

So I should go to bed instead.

#### Patrick Massot (Jun 16 2022 at 20:23):

Have fun!

Last updated: Aug 03 2023 at 10:10 UTC