Aesop safe apply not triggering

Stream: metaprogramming / tactics

[Geoffrey Irving]

I'm confused why this aesop call doesn't work. Am I using ofNat and AtLeastTwo wrong?

import Mathlib.Data.Real.Basic

structure A where
  x : ℝ

def approx (x : A) : Set ℝ := sorry
def convert (x : ℚ) : A := sorry

lemma mem_approx {a b : ℕ} [a.AtLeastTwo] [b.AtLeastTwo] :
    OfNat.ofNat a / OfNat.ofNat b ∈ approx (convert (OfNat.ofNat a / OfNat.ofNat b)) := sorry

set_option trace.aesop true in
example : 2 / 3 ∈ approx (convert (2 / 3)) := by
  --exact mem_approx  -- Works
  aesop (add safe apply mem_approx)  -- Fails

(This is minimized from a more complicated aesop tactic.)

[Geoffrey Irving]

add norm apply mem_approx also doesn't work.

[Geoffrey Irving]

Note that the OfNat.ofNats on the left of mem_approx are converting to ℝ, and those on the right are converting to ℚ, which is why I can't generalize mem_approx further.

[Jannis Limperg]

Further minimised:

import Aesop

structure ℝ : Type where
  r : Nat

instance : OfNat ℝ n :=
  ⟨⟨n⟩⟩

axiom P : ℝ → Prop
axiom mem_approx (a : Nat) : P (OfNat.ofNat a)

set_option pp.all true

#check mem_approx

-- Works
example (a : Nat) : P (OfNat.ofNat a) := by
  -- exact mem_approx a
  aesop (add safe apply mem_approx)

example : P 2 := by
  -- exact mem_approx 2 -- works
  aesop (add safe apply mem_approx) -- fails

Aesop doesn't even try mem_approx, so most likely the discrimination tree still has issues with number literals. I'll investigate further.

[Geoffrey Irving]

Thank you!

[Johan Commelin]

See also lean4#2867

[Geoffrey Irving]

It looks like https://github.com/leanprover/lean4/pull/3684 which fixes that issue has been stalled since April 11.