Prevent aesop from unfolding specific definitions

Stream: lean4

[Arend Mellendijk]

I've been playing around with a custom aesop ruleset for dispensing with simple (Nat) divisibility goals. I basically just want it to compute the transitive closure of ∣, and to deal properly with a ∈ b.divisors, which involves occasionally proving b≠0 by substituting until it finds a contradiction.

I've disabled the simp step as it has a tendency to do unwanted rewrites, but I'm still running into the issue with slightly longer proofs that aesop has a tendency to unfold a ∣ b into b=a*w and start rewriting, making it blind to the fact that it's already proved the goal.

MWE

First you need a separate file Init.lean to declare the ruleset

import aesop

declare_aesop_rule_sets [Divisibility]

Then

import Aesop
import <FolderName>.Init
import Mathlib.NumberTheory.ArithmeticFunction


open Finset

macro (name := aesop_div?) "aesop_div?" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  aesop? $c* (options := { introsTransparency? := some .default, terminal := false})
  (simp_options := { enabled := false})
  (rule_sets [$(Lean.mkIdent `Divisibility):ident]))


attribute [aesop unsafe forward 60% (rule_sets [Divisibility])] Nat.dvd_trans
attribute [aesop safe forward (rule_sets [Divisibility])] Nat.dvd_of_mem_divisors

@[aesop safe (rule_sets [Divisibility])]
theorem mem_divisors_mpr {n m : ℕ}: n ∣ m ∧ m ≠ 0 → n ∈ m.divisors := Nat.mem_divisors.mpr

@[aesop forward safe (rule_sets [Divisibility])]
theorem nat_eq_zero_of_zero_dvd (a : ℕ) : 0 ∣ a → a = 0 := by
  apply zero_dvd_iff.mp

@[aesop forward safe (rule_sets [Divisibility])]
theorem zero_mem_divisors (a : ℕ) (h : 0 ∈ a.divisors) : False := by simp at h

attribute [aesop safe (rule_sets [Divisibility])] Nat.pos_of_ne_zero

example (a b c d :ℕ) (h: d ≠ 0) : (b ∈ c.divisors) → a ∣ b → c ∣ d → a ∈ d.divisors := by
  aesop_div?

/- Works -/
example {P : ℕ} (n : ℕ) (hP : P ≠ 0) (hn : n ∣ P) :
    (P.divisors.filter (· ∣ n)) = n.divisors :=
  by
  ext k; rw [mem_filter];
  constructor
  · intro ⟨_,_⟩
    aesop_div?
  · aesop_div?

/- Fails -/
example {P : ℕ} (n : ℕ) (hP : P ≠ 0) (hn : n ∣ P) :
    (P.divisors.filter (· ∣ n)) = n.divisors :=
  by
  ext k; rw [mem_filter];
  /- ⊢ k ∈ Nat.divisors P ∧ k ∣ n ↔ k ∈ Nat.divisors n -/
  aesop_div?
  /-
  case a.mp.a.left
  k w w_1 : ℕ
  hP : k * w_1 * w ≠ 0
  left : k ∈ Nat.divisors (k * w_1 * w)
  fwd : k ∣ k * w_1 * w
  ⊢ k ∣ k * w_1
  ... (three more similar cases)
  -/
  repeat sorry

As you can see in the first subcase of the failed proof aesop decided to substitute P=n*w to eliminate P, not realising it could have just proved the goal by transitivity. Is there a good way to just prevent aesop from unfolding a ∣ b into ∃w, b=a*w?

[Alex Keizer]

You can erase lemmas for a specific Aesop call, so presumably you should erase the rule that does that unfold

[Jannis Limperg]

What happens here is that divisibilty on Nat is defined as ∃ c, b = a * c. The builtin destructProducts rule therefore matches hypotheses of the form . | . and splits them into c and b = a * c. (I found this out by inspecting the trace output from set_option trace.aesop true.) As a workaround, you can try to disable the destructProducts rule as Alex suggests.

A more radical approach would be to change the definition of divisibility so that . | . is no longer reducibly defeq to an existential. I imagine this would create a lot of breakage.

[Jannis Limperg]

I could probably also implement an option that lets destructProducts match only syntactically, not up to defeq.

[Arend Mellendijk]

Thanks for the help!
I've tried disabling destructProducts altogether, but it has the unintended (yet expected) side effect that it won't unfold ∧ in the hypotheses, which means it still fails on the same examples. In particular it can't prove a ∣ b ∧ b ∣ c → a ∣ c, whereas it can prove a ∣ b → b ∣ c → a ∣ c. In effect this doesn't seem to change the strength of the ruleset at all since destructProducts only gets called when there is an ∧ in a hypothesis that it needs to prove the goal.

[Arend Mellendijk]

I guess if there is a way to disable only ∃ terms that would work

[Jannis Limperg]

Makes sense. There's currently no way to disable ∃ specifically, and anyway it would be a big hack.

Another possibly way to address the root problem (that . | . reducibly reduces to an existential):

• Define def MyDvd a b := a | b.
• Add a preprocessing step or Aesop rule which rewrites a | b to MyDvd a b.
• Formulate the Aesop rules in terms of MyDvd.

[Scott Morrison]

In the longer term changing the reducibility of | seems like a great idea.

[Gabriel Ebner]

I don't expect this to break much (or anything). #5603

[Gabriel Ebner]

I think this requires a larger refactoring, since we have a Dvd α instance for every semigroup, and that instance should be (reducibly!) defeq to the Nat/Int instances.

[Gabriel Ebner]

That is, a Nat.dvd definition doesn't cut it. We need some generic (semireducible) divides [Mul α] predicate (in std!), and then use that to define all three instances.

[Gabriel Ebner]

#5604

[Arend Mellendijk]

I've made a MyDvd definition, and now the tactic works when I make it irreducible, but when it's semireducible it still gets unfolded by destructProducts, even with an explicit destructProductsTransparency := .reducible.
I'm frankly not sure if this is me misunderstanding transparency settings or if this is a bug in aesop.

MWE

import Aesop
import <FolderName>.Init
import Mathlib.NumberTheory.ArithmeticFunction

open Finset

namespace MWE
@[semireducible]
protected def MyDvd (a b :ℕ) : Prop := a ∣ b

@[simp]
theorem myDvd_iff (a b : ℕ) : MWE.MyDvd a b ↔ a ∣ b := by
  unfold MWE.MyDvd
  exact Iff.rfl

macro (name := aesop_div) "aesop_div" c:Aesop.tactic_clause* : tactic =>
`(tactic|
  {try simp_rw [←myDvd_iff] at *; aesop $c* (options :=
  { destructProductsTransparency := .reducible, introsTransparency? := some .reducible, terminal := false } )
  (simp_options := { enabled := false})
  (rule_sets [$(Lean.mkIdent `Divisibility):ident])})

@[aesop unsafe forward 60% (rule_sets [Divisibility])]
theorem myDvd_trans {a b c : ℕ} : MWE.MyDvd a b → MWE.MyDvd b c → MWE.MyDvd a c := by
  simp; exact Nat.dvd_trans
--set_option trace.aesop true

example {a b c : ℕ} : a ∣ b ∧ b ∣ c → a ∣ c := by
  simp_rw [←myDvd_iff] at *
  /-
  ⊢ MyDvd a b ∧ MyDvd b c → MyDvd a c
  -/
  aesop_div
  /-
  unsolved goals

  aww_1: ℕ
  ⊢ MWE.MyDvd a (a * w * w_1)
  -/
end MWE

[Jannis Limperg]

Could well be a bug. I'll look at it later.

[Jannis Limperg]

This was indeed an Aesop bug: destructProducts would use destructProductsTransparency when first matching a hyp, but would then use default for recursive matching. Now fixed in Aesop. No breakage in mathlib, but the PR must wait for #5409.