# Zulip Chat Archive

## 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.

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

Fixed.

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

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 (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):

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 (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: Dec 20 2023 at 11:08 UTC