Zulip Chat Archive

Stream: new members

Topic: Writing rationals


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 17 2018 at 16:42):

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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 17 2018 at 16:44):

Try cases on r?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 17 2018 at 16:44):

Yep, just tried that, works.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Olson (Oct 17 2018 at 16:46):

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

view this post on Zulip 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).

view this post on Zulip 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