erasing `unfold` rules in `aesop`, and `traceScript := true`

Stream: mathlib4

[Jireh Loreaux]

@Jannis Limperg I'm facing two aesop issues that I assume is just my own ignorance:

1. I can't seem to erase an unfold rule from aesop. To be more specific, I can erase it (in the sense that aesop complains if I try to erase it twice), but I still see aesop_unfold ... and it still appears in the constants to unfold when using set_option trace.aesop.ruleSets true.
2. Here it seems to suggest that setting traceScript := true should output the proof that aesop produces when it closes the goal. Is it possible to also have it output a partial proof script (with sorry) when it fails to close the goal? Or at least, provide another option for it?

[Jannis Limperg]

The first sounds like a bug. (Erasing is not well tested.) Do you have an example?

[Jannis Limperg]

The second doesn't currently work, but it could certainly be made to work. Aesop would then report a partial proof corresponding to the safe rules it applied, just like it currently reports the goals produced by the safe rules. This needs some changes to the procedures that produce these tactic proofs, but I can prioritise those. (I'm away for conferences and summer schools all September, so progress won't be quick I'm afraid.)

[Jannis Limperg]

Btw, you can write aesop? instead of setting traceScript := true.

[Jireh Loreaux]

Here's an mwe for the first issue:

import Aesop

@[irreducible]
def bar : Nat := 37

example : bar = 37 := by aesop -- fails because it can't unfold `bar`

@[aesop unfold norm, irreducible]
def foo : Nat := 37

example : foo = 37 := by aesop -- works because it can unfold `foo`

attribute [-aesop] foo

-- errors with: 'foo' is not registered (with the given features) in any rule set.
attribute [-aesop] foo

example : foo = 37 := by aesop -- still works despite removing the `aesop` rules

[Jireh Loreaux]

As for the second issue: I'm not asking you to spend time working on it yet. I thought it could be a nice modification for the continuity? tactic where it produces a partial proof that the function is continuous, but I haven't yet asked the community if this is desired. My guess is it will be though.

[Jannis Limperg]

Jireh Loreaux said:

Here's an mwe for the first issue: [...]

Fixed in Aesop master. Thank you for the very nice MWE!

[Jannis Limperg]

Jireh Loreaux said:

As for the second issue: I'm not asking you to spend time working on it yet. I thought it could be a nice modification for the continuity? tactic where it produces a partial proof that the function is continuous, but I haven't yet asked the community if this is desired. My guess is it will be though.

Okay. I'll certainly implement this at some point, but if you need it sooner than later, let me know.