Zulip Chat Archive

Stream: new members

Topic: computing rat.num


Mantas Baksys (Dec 06 2021 at 18:03):

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 (Dec 06 2021 at 21:28):

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

Kevin Buzzard (Dec 06 2021 at 21:35):

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

Patrick Johnson (Dec 07 2021 at 05:57):

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 (Dec 07 2021 at 06:32):

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 (Dec 07 2021 at 06:47):

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 (Dec 07 2021 at 06:55):

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 (Dec 07 2021 at 07:15):

I guess lean#562 is related

Kyle Miller (Dec 07 2021 at 07:22):

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

Kyle Miller (Dec 07 2021 at 07:23):

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 (Dec 07 2021 at 07:23):

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 (Dec 07 2021 at 09:05):

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

Mario Carneiro (Dec 07 2021 at 09:05):

the proof should be by rw h; norm_num

Anatole Dedecker (Dec 07 2021 at 10:07):

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

Eric Wieser (Dec 07 2021 at 10:21):

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

Reid Barton (Dec 07 2021 at 15:46):

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


Last updated: Dec 20 2023 at 11:08 UTC