Writing rationals

Stream: new members

[Abhimanyu Pallavi Sudhir]

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

[Abhimanyu Pallavi Sudhir]

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

[Kevin Buzzard]

Try cases on r?

[Abhimanyu Pallavi Sudhir]

Yep, just tried that, works.

[Kevin Buzzard]

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]

\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]

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

[Kevin Buzzard]

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]

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