Zulip Chat Archive

Stream: general

Topic: rat.mk_eq


view this post on Zulip 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,
[...]

view this post on Zulip Kenny Lau (Apr 25 2018 at 14:56):

the one in suffices is what I need T_T

view this post on Zulip Mario Carneiro (Apr 25 2018 at 17:03):

Just rewrite mk_pnat into /., they are equal

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 25 2018 at 17:04):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 25 2018 at 17:08):

oh, mk_pnat is not intended to be used?

view this post on Zulip Kenny Lau (Apr 25 2018 at 17:08):

I used it because I am using pnat

view this post on Zulip Kenny Lau (Apr 25 2018 at 17:08):

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

view this post on Zulip Mario Carneiro (Apr 25 2018 at 17:10):

Just use n / d where d : N+

view this post on Zulip 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: May 13 2021 at 06:15 UTC