Zulip Chat Archive

Stream: general

Topic: rat.mk_eq


Kenny Lau (Apr 25 2018 at 14:55):

theorem mk_eq :  {a b c d : } (hb : b  0) (hd : d  0),
  a /. b = c /. d  a * d = c * b :=
suffices  a b c d hb hd, mk_pnat a b, hb = mk_pnat c d, hd  a * d = c * b,
[...]

Kenny Lau (Apr 25 2018 at 14:56):

the one in suffices is what I need T_T

Mario Carneiro (Apr 25 2018 at 17:03):

Just rewrite mk_pnat into /., they are equal

Kenny Lau (Apr 25 2018 at 17:04):

this is what I did at the end:

theorem rat.mk_pnat_eq_iff (a b c d) : rat.mk_pnat a b = rat.mk_pnat c d  a * d = c * b :=
begin
  cases b with b hb, cases d with d hd,
  simp [rat.mk_pnat_eq],
  rw [rat.mk_eq],
  exact ne_of_gt (int.coe_nat_pos.2 hb),
  exact ne_of_gt (int.coe_nat_pos.2 hd),
end

Kenny Lau (Apr 25 2018 at 17:04):

this part of the code is not going to be PR'd so the neatness of the proof doesn't really matter ot me

Kenny Lau (Apr 25 2018 at 17:04):

but I did write a whole bunch of lemmas in the meantime

Mario Carneiro (Apr 25 2018 at 17:07):

The real question is why are you dealing with mk_pnat? The interface should let you just use field operations and avoid mk entirely

Kenny Lau (Apr 25 2018 at 17:08):

oh, mk_pnat is not intended to be used?

Kenny Lau (Apr 25 2018 at 17:08):

I used it because I am using pnat

Kenny Lau (Apr 25 2018 at 17:08):

or are you going to tell me that pnat is not to be used either

Mario Carneiro (Apr 25 2018 at 17:10):

Just use n / d where d : N+

Mario Carneiro (Apr 25 2018 at 17:11):

The only reason you might want mk_pnat is if you care about the efficiency of computing this value (this will translate d to rat by adding ones)


Last updated: Dec 20 2023 at 11:08 UTC