Zulip Chat Archive

Stream: new members

Topic: Unable to apply dvd_sub


Ben Nale (Aug 11 2020 at 22:39):

I want to show that gcd(a,b) \mid a-b
this is what I typed into lean:
have h3: nat.gcd a b ∣ a - b ,
cases nat.gcd_dvd a b,
apply dvd_sub,

However, I get an error under apply saying that unable to unify m_1 \mid m_2-m_3 even though the goal is in this exact form.
Note that using the exact same technique and div_add I am able to prove the addition version of this lemma.
image.png

Kenny Lau (Aug 11 2020 at 22:47):

the typeclasses are different

Kenny Lau (Aug 11 2020 at 22:47):

dvd_sub is for commutative rings

Kenny Lau (Aug 11 2020 at 22:47):

but nat is only a commutative semiring

Kenny Lau (Aug 11 2020 at 22:48):

the subtraction in nat is different

Ben Nale (Aug 11 2020 at 22:48):

Oh so I could say (nat.gcd a b : \Z ) \mid (a-b :\Z)

Kevin Buzzard (Aug 11 2020 at 22:48):

Yes

Kevin Buzzard (Aug 11 2020 at 22:50):

If you type #check @dvd_sub you can see all the type classes required to make the lemma work, and you can see if nat has them by trying to construct them with apply_instance, e.g. example : comm_ring \N := by apply_instance, which of course fails because nat isn't a ring.

Ben Nale (Aug 11 2020 at 22:50):

Oh the apply works now. Though using cases on nat.gcd_dvd a b produces to hypotheses with no arrows. But we need arrows

Ben Nale (Aug 11 2020 at 22:50):

image.png

Kevin Buzzard (Aug 11 2020 at 22:51):

the arrow is just the function from nat to int. You might be able to get rid of it with the norm_cast tactic.

Ben Nale (Aug 11 2020 at 22:52):

Nice. It works and I get it. Thanks.

Ben Nale (Aug 11 2020 at 22:53):

have h3: (nat.gcd a b :ℤ ) ∣ (a - b :ℤ) ,
cases nat.gcd_dvd a b,
apply dvd_sub,
norm_cast,
exact left,
norm_cast,
exact right,

Ben Nale (Aug 11 2020 at 22:53):

no goals :)

Kenny Lau (Aug 12 2020 at 06:34):

#backticks


Last updated: Dec 20 2023 at 11:08 UTC