Stream: new members

Topic: How to use dvd_of_mul_left_dvd and friends?

Jordan Scales (Oct 11 2020 at 20:15):

Hey :) I'm toying around with some modular arithmetic, and am struggling to prove a basic premise: 3 ∣ n → ¬ 5 ∣ n → ¬ 15 ∣ n

I'd like to prove this by assuming divisibility by 15, and finding a contradiction with divisibility by 5. However, dvd_of_mul_left_dvd is giving me pause.

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
intros h₃ h₅ h,
have q : 15 = 3 * 5, { refl },
rw q at h,
have contra := dvd_of_mul_left_dvd h,
end


specifically:

type mismatch at application
dvd_of_mul_left_dvd h
term
h
has type
3 * 5 ∣ n
but is expected to have type
?m_3 * ?m_4 ∣ ?m_5


I am unsure why the pattern matching isn't working here. Any pointers?

Kevin Buzzard (Oct 11 2020 at 20:16):

What do I need to import/open to get this working? Can you post a #mwe?

Jordan Scales (Oct 11 2020 at 20:17):

my apologies! I have the following imported:

import tactic.suggest
import algebra.divisibility


so the entire (not working :( ) file is as follows:

import tactic.suggest
import algebra.divisibility

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
intros h₃ h₅ h,
have q : 15 = 3 * 5, { refl },
rw q at h,
have contra := dvd_of_mul_left_dvd h,
end


Kevin Buzzard (Oct 11 2020 at 20:21):

You don't have enough imports, apparently: you seem to have managed to avoid importing the fact that the naturals are a commutative monoid.

import tactic

example (n : ℕ) : 3 ∣ n -> ¬ 5 ∣ n -> ¬ 15 ∣ n := begin
intros h₃ h₅ h,
have q : 15 = 3 * 5, { refl },
rw q at h,
have contra := dvd_of_mul_left_dvd h,
sorry
end


works fine.

Jordan Scales (Oct 11 2020 at 20:22):

fascinating! works for me as well :) thank you.

Kevin Buzzard (Oct 11 2020 at 20:22):

These facts used to be in core Lean 3 but in the community fork we ripped them out and moved them to mathlib, so now you have to explicitly import them.

Kevin Buzzard (Oct 11 2020 at 20:22):

I didn't know this wasn't there by default any more because every Lean file I write starts with import tactic.

Jordan Scales (Oct 11 2020 at 20:23):

starting every file with import tactic is something I can definitely accept

Last updated: May 14 2021 at 06:16 UTC