Zulip Chat Archive

Stream: new members

Topic: rat.denom_zero


view this post on Zulip Lars Ericson (Jan 14 2021 at 02:00):

There is a rat.denom_one. There is no rat.denom_zero. However, given the goal

 0.denom = 1

the tactic

exact rfl,

will close the goal.

Question: What is happening under the hood with exact rfl?

view this post on Zulip Thomas Browning (Jan 14 2021 at 02:00):

rfl means that things are definitionally equal

view this post on Zulip Thomas Browning (Jan 14 2021 at 02:00):

refl should also work

view this post on Zulip Thomas Browning (Jan 14 2021 at 02:05):

Here's why 0.denom = 1 is definitionally equal.

First, 0 is defined as: instance : has_zero ℚ := ⟨of_int 0⟩
Second, of_int is defined as def of_int (n : ℤ) : ℚ := ⟨n, 1, nat.one_pos, nat.coprime_one_right _⟩
These four arguments correspond to the four arguments in the definition of a rational:

structure rat := mk' ::
(num : )
(denom : )
(pos : 0 < denom)
(cop : num.nat_abs.coprime denom)

Thus, of_int n means the rational number with num = n, denom = 1. In particular, (of_int n).num = n by definition and (of_int n).denom = 1 by definition.

view this post on Zulip Thomas Browning (Jan 14 2021 at 02:05):

(This is all coming from data/rat/basic.lean)

view this post on Zulip Thomas Browning (Jan 14 2021 at 02:09):

So both of these examples are definitionally true (and 0.denom = 1 is a special case of the second example).

example (n : ) : (rat.of_int n).num = n := rfl
example (n : ) : (rat.of_int n).denom = 1 := rfl

view this post on Zulip Lars Ericson (Jan 14 2021 at 02:28):

Thank you!

view this post on Zulip Eric Wieser (Jan 14 2021 at 08:40):

Presumably denom_zero should be added as a simp lemma?


Last updated: May 16 2021 at 05:21 UTC