Mathlib zero-argument high-powered tactics for divisibility?

Stream: new members

[Isak Colboubrani]

Is it correct to claim that the following two examples (from MIL chapter 2 section 4) currently cannot be solved in one step using a Mathlib zero-argument high-powered tactic (think simp_all?, exact?, , etc.)?

example (x y z : ℕ) : x ∣ y * x * z := by sorry
example (w x y z : ℕ) (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by sorry

[Eric Wieser]

This works for the first one:

attribute [aesop unsafe apply] dvd_mul_of_dvd_right dvd_mul_of_dvd_left

example (x y z : ℕ) : x ∣ y * x * z := by aesop

[Ruben Van de Velde]

Why do you ask? It seems to get more common recently to ask for tactics that solve goals with no further input, and I wonder where that comes from

[Isak Colboubrani]

@Ruben Van de Velde For a demonstration to my fellow undergraduates, I first present a method for solving MIL exercises from first principles, and then I show how to solve them using high-powered tactics (where possible).

These two example exercises appeared so trivial that I couldn’t dismiss the possibility of a tactic that would solve them (with no further input). (Note: I’m not asserting that such a tactic should exist, nor do I have any difficulty solving these exercises; I simply want to confirm whether my claim is correct.)

[Isak Colboubrani]

@Eric Wieser Is the unsafe part the reason this aesop annotation isn't included in Mathlib, or are there other reasons?

[Eric Wieser]

unsafe in this context doesn't mean "this code is unsafe" but informs aesop that it may lead to a dead end

[Eric Wieser]

Maybe @Jannis Limperg can comment on whether that is an appropriate configuration to include in mathlib

[Jannis Limperg]

Yes, I think it would be appropriate to put these lemmas into the global Aesop set as unsafe 50% (or to make a separate set about divisibility if you want to be careful). As it happens, I recently went through Divisibility.Basic for a talk and there are a few other good Aesop lemmas in there.

[Isak Colboubrani]

@Jannis Limperg Do you happen to have the notes handy, or do you recall which lemmas they were?

[Daniel Weber]

If this is still relevant, you can also do

import Mathlib

example (x y z : ℕ) : x ∣ y * x * z := by simp [← ZMod.natCast_zmod_eq_zero_iff_dvd]
example (w x y z : ℕ) (h : x ∣ w) : x ∣ y * (x * z) + x ^ 2 + w ^ 2 := by simp_all [← ZMod.natCast_zmod_eq_zero_iff_dvd]