Zulip Chat Archive

Stream: new members

Topic: How to use dvd_of_mul_left_dvd and friends?


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

view this post on Zulip Kevin Buzzard (Oct 11 2020 at 20:16):

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

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

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

view this post on Zulip Jordan Scales (Oct 11 2020 at 20:22):

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

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

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

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