computing rat.num

Stream: new members

[Mantas Baksys]

I was surprised I can't find an easier way to prove this :

lemma explicit_num (q : ℚ) (h : q = 1 / 3) : q.num = 1 :=
begin
  convert @rat.num_div_eq_of_coprime 1 3 (by linarith),
  simp [h],
end

Is this the go-to way or is there an easier way?

[Anne Baanen]

Huh, I would have thought by { rw h, refl } would work, since everything is computable...

[Kevin Buzzard]

I tried subst h, norm_num but that didn't work either

[Patrick Johnson]

I'm not an expert, but I think there is no shorter way, not because someone was lazy to implement it, but simply because that's the minimal amount of work you have to invest to express what you want to obtain. Each rational number is fully reduced. Division of rational numbers is a function, not a structure. When written syntactically as 1 / 3 it seems obvious that 1 and 3 are coprime, that 1 is an integer and that 3 is a positive natural number. But note that it could be written as 2 / 6 or (-3) / (-9) or in many other ways.

What I'm trying to say is that each part of the proof is necessary. convert is needed to deal with nat/int/rat conversions. 1 and 3 are needed to explicitly specify that we know what the numerator and the denominator of the reduced fraction are. linarith is needed because it is probably the easiest way to prove that 3 is a positive integer. And simp [h] is needed to actually use the hypothesis.

It is possible to write a tactic to do this automatically. Given a rational number of the form a / b, the tactic would produce a local hypothesis (a / b).num = a, or produce an error if it is not true. I'm not on that level yet to write such tactic, sorry.

[Reid Barton]

This is what I don't understand:

import data.rat.basic

example : (2 : ℚ).num = 2 := rfl -- fails quickly
#reduce (2 : ℚ).num              -- outputs `int.of_nat 2` quickly

[Reid Barton]

Ah progress, this also fails:

example : nat.gcd 1 1 = 1 := rfl

#print axioms indicates that nat.gcd uses propext (in the proof of termination). So the rationals are not so constructive after all :upside_down:
But now I don't totally understand why #reduce nat.gcd 1 1 does work.

[Kyle Miller]

I guess if nat.gcd 1 1 = 1 := rfl doesn't work, then neither should this:

instance nat.coprime' : Π (x y : ℕ), decidable (nat.coprime x y)
| 0     y :=
  if h : y = 1
  then decidable.is_true (by simp [h])
  else decidable.is_false (by simp [h])
| (nat.succ x) y := have y % x.succ < x.succ, from nat.mod_lt _ $ nat.succ_pos _,
  match nat.coprime' (y % x.succ) x.succ with
  | decidable.is_true h := decidable.is_true (by simpa [nat.coprime, nat.gcd] using h)
  | decidable.is_false h := decidable.is_false (by simpa [nat.coprime, nat.gcd] using h)
  end

example : nat.coprime 1 3 := dec_trivial -- error

[Reid Barton]

I guess lean#562 is related

[Kyle Miller]

That seems to be it. It works in an old version of lean)

[Kyle Miller]

I think this might explain all the mysterious problems I had trying to get some dec_trivial proofs to work a few months ago.

[Reid Barton]

and then I think the kernel doesn't care about any of this "lemma" or "irreducible" nonsense, and will just unfold anything that it needs to, and that's why #reduce does still work

[Mario Carneiro]

There are clearly some missing norm_num plugins for nat.gcd, nat.coprime, rat.num and rat.denom

[Mario Carneiro]

the proof should be by rw h; norm_num

[Anatole Dedecker]

I still don’t understand why #reduce works but not rfl

[Eric Wieser]

I assume that #reduce is allowed to reduce acc.rec but rfl isn't?

[Reid Barton]

My conclusion was that the elaborator does not unfold lemmas (like mod_lt used in the proof of termination) but the kernel does