rat.denom_zero

Stream: new members

[Lars Ericson]

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?

[Thomas Browning]

rfl means that things are definitionally equal

[Thomas Browning]

refl should also work

[Thomas Browning]

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.

[Thomas Browning]

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

[Thomas Browning]

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

[Lars Ericson]

Thank you!

[Eric Wieser]

Presumably denom_zero should be added as a simp lemma?