## Stream: new members

### Topic: Writing rationals

#### Abhimanyu Pallavi Sudhir (Oct 17 2018 at 16:42):

How can I rewrite a known rational r : \Q in the form rat.mk (...) (...)?

#### Abhimanyu Pallavi Sudhir (Oct 17 2018 at 16:44):

I expected something like change rat.mk (rat.num) (rat.denom) at r, but that doesn't work.

Try cases on r?

#### Abhimanyu Pallavi Sudhir (Oct 17 2018 at 16:44):

Yep, just tried that, works.

#### Kevin Buzzard (Oct 17 2018 at 16:45):

I agree that rat.num / rat.denom = r but that looks to me like a theorem rather than something which is true by definition.

#### Kevin Buzzard (Oct 17 2018 at 16:45):

\Q is an inductive type, so you can always do cases on it. It only has one constructor so the number of goals won't change.

#### Scott Olson (Oct 17 2018 at 16:46):

I just found theorem rat.num_denom : ∀ (a : ℚ), a = rat.mk (a.num) ↑(a.denom)

#### Kevin Buzzard (Oct 17 2018 at 17:03):

If you want _anything_ other than what cases provides (and you might well find that you want what @Scott Olson says rather than what I said -- I am breaking the interface) then my advice to you is to open data/rat.lean and pore through it until you spot what you need. Either that or get good at guessing the names of theorems (there are tips for doing this).

#### Kevin Buzzard (Oct 17 2018 at 17:03):

By the way, the actual construtor rat.mk' needs a couple of proofs, and that's what you'll get with cases. The reason the initial constructor is so inconvenient is that it guarantees that two rationals are equal if and only if they're made with the same data (remember that all proofs of a proposition are equal by definition).

Last updated: May 08 2021 at 03:17 UTC