Aesop? partial suggestion behavior

Stream: lean4

[Josh Clune]

Aesop's specification says that if Aesop fails to fully prove a goal, it reports the safe goals, i.e., the goals obtained by just applying Aesop's normalization and safe rules. Likewise, the suggestion given by aesop? on a goal that Aesop cannot fully prove is exactly the tactic script corresponding to the application of these normalization and safe rules. This makes sense and is ultimately, not a problem.

However, there are some circumstances where it seems Aesop could make a bit more progress, even when it can't fully close the original goal. Consider the following pair of examples:

axiom p : Prop
axiom q : Prop
axiom hp : p
axiom hq : q

example : p ↔ q := by
  -- `aesop? (add unsafe hp) (add unsafe hq)` succeeds and suggests the following proof:
  apply Iff.intro
  · intro a
    apply hq
  · intro a
    apply hp

example : p ↔ q := by
  -- `aesop? (add unsafe hp)` fails and suggests the following proof:
  apply Iff.intro
  · intro a
    sorry
  · intro a
    sorry

In the second example, even though Aesop could close the second sorry with apply hp (as it finds in the first example), it doesn't because hp is registered as an unsafe rule.

How difficult would it be to change aesop?'s behavior so that if an unsafe rule closes a Prop-typed goal and does not generate any new goals, it is included in the final aesop? recommendation (despite not being a "safe" rule application). My intuition is that this would still preserve provability (as only applying safe rules does) and it would yield strictly more complete suggestions, but I don't know how difficult this would be to implement or whether there are issues I'm failing to consider.

[Jannis Limperg]

This is a great suggestion; your behaviour is clearly better than what's currently implemented. It's not entirely trivial to implement, but shouldn't be too hard, either. Do you need it soon?

aesop#221

[Josh Clune]

The current behavior isn’t blocking for me, so there’s no urgency on this. Thanks for making an issue, I’m sure I’ll find this helpful whenever it gets implemented.