aesop destruct side-conditions

Stream: mathlib4

[Joachim Breitner]

I am playing around with aesop; great so far, and in particular thanks for the high quality README at https://github.com/JLimperg/aesop.

I currently have this code

@[aesop safe (destruct (immediate := [h1])) (rule_sets [NatElim])]
lemma le_sub (h1 : i ≤ n - j) (h2 : j ≤ n) : i + j ≤ n :=
  Nat.add_le_of_le_sub h2 h1

What it does is it finds hyps of type i ≤ n - j and replaces them with j ≤ n → i + j ≤ n.
What I want it to do is to find hyps of type i ≤ n - j, have a new goal to prove j ≤ n (again using aesop), and finally replace the hyp with i + j ≤ n.
Is that possible somehow to tell aesop that h2 isn’t immediate (it’s not present in the goal, but needs to be proven), but also that it’s not just part of the replacement?
(I think in Isabelle this was possible using elimination-style rule, but my attempts at this didn’t work.)

[Joachim Breitner]

Here is a #mwe

import Aesop

axiom A : Prop
axiom B : Prop
axiom C : Prop
axiom D : Prop

@[aesop safe (destruct (immediate := [h1]))]
theorem foo (h1 : A) (h2 : B) : C := sorry

@[aesop safe apply]
theorem b : B := sorry

theorem test : A -> D := by
  aesop
  -- Goal has fwd : B → C
  -- Goal should have C

[Jannis Limperg]

This is not currently possible, but I can see that it could be useful. Do you want the side condition for h2 to become an additional goal (so the le_sub rule always succeeds when it sees a hypothesis that matches h1, but we may later discover that h2 cannot be discharged) or do you want h2 to be discharged immediately by a nested Aesop call (making le_sub a very expensive rule)?

Performance may suffer in any case since we don't currently remember that the side goal for h2 could or couldn't be proved.

[Joachim Breitner]

In this case I'd like the rule to always succeed and and the side condition to become an additional goal.

[Joachim Breitner]

What mechanisms are there to create new goals with the existing builders? I guess apply creates new goals, but besides that?

[Joachim Breitner]

Hmm, maybe I should use a destruct rule to create a disjunction instead of an implication, and let Aesop split that?

A -> (~ B \/ (B /\ C))

[Jannis Limperg]

Oh yeah, that might work as a stopgap measure.

[Joachim Breitner]

This may actually work reasonably well; here is the beginning of an aesop-based tactic that eliminates uses of Nat.sub around inequalities before handing the goal over to linarith, to hopefully handle the typical cases of array bounds calculations:

import Mathlib.Tactic.Linarith
import Mathlib.Tactic.LibrarySearch
import RerollingSixes.NatSubElimRuleSet

variable (n : ℕ)
variable (i : ℕ)
variable (j : ℕ)

structure SC (p q : Prop) : Prop :=
  imp : p → q

@[aesop norm simp (rule_sets [NatElim])]
lemma sc (p q : Prop) : SC p q ↔ (¬ p ∨ (p /\ q)) := sorry

@[aesop safe apply (rule_sets [NatElim])]
lemma le_intro : (i < n -> False) -> n ≤ i := sorry
@[aesop safe apply (rule_sets [NatElim])]
lemma lt_intro : (i ≤ n -> False) -> n < i := sorry

@[aesop safe (destruct (immediate := [h1])) (rule_sets [NatElim])]
lemma le_sub (h1 : i ≤ n - j) : SC (j ≤ n) (i + j ≤ n) :=
  .mk (fun h2 => Nat.add_le_of_le_sub h2 h1)
@[aesop safe (destruct (immediate := [h1])) (rule_sets [NatElim])]
lemma lt_sub (h1 : n - j < i) : SC (j ≤ n) (n < i + j) :=
  sorry

def linarithTactic := do
  Lean.Elab.Tactic.evalTactic (← `(tactic| linarith))

attribute [aesop safe tactic (rule_sets [NatElim])] linarithTactic

syntax "nat_intervals" : tactic
macro_rules
  | `(tactic| nat_intervals) => `(tactic|
    aesop (rule_sets [$(Lean.mkIdent `NatElim):ident])
  )

example : n ≠ 0 → n - 1 < n := by
  intros
  nat_intervals

example : ¬i = 0 → 0 < i := by
  intros
  nat_intervals

example : i ≤ n → j ≤ n - i → i ≤ n - j := by
  intros
  nat_intervals

[Joachim Breitner]

But it seems that aesop’s Aesop.BuiltinRules.applyHyps quickly loops when the goal is False, and there are hyps of the form ¬ … around, as it tries to apply them. I probably need to hide them somehow, maybe a norm simp rule?

[Joachim Breitner]

#mwe:

import Aesop
theorem P Q : ¬ P → ¬ Q → False := by
  aesop

says

aesop: maximum number of rule applications (200) reached. Set the 'maxRuleApplications' option to increase the limit.

[Joachim Breitner]

I can work around it by changing my goal not to False, but to a differnt MyFalse.

[Joachim Breitner]

Pretty neat; these examples are annoying boring proof obligations from a little project of mine:

example : 3 ≤ n → j ≤ n → ¬j = 0 → ¬j = n → ¬j = n - 1 → j < n - 1 := by
  intros
  nat_intervals

example : 0 < i → i < n - 1 → j < i → j ≤ n - 2 - 1 := by
  intros
  nat_intervals

[Kevin Buzzard]

Make sure that the False loop is opened as an issue if it's not solved during this thread, that's a great MWE you have.

[Joachim Breitner]

Against the aesop repo or the mathlib4 repo?

[Jannis Limperg]

Aesop. The loop happens because applyHyps transforms not P, not Q |- False into not P, not Q |- P and simp transforms this back into not P, not Q |- False. :upside_down: Negation in general is much more annoying to deal with than I thought.

Your nat_intervals tactic looks very nice btw. I've occasionally wanted something that deals with these annoying array index side conditions.

[Jannis Limperg]

JLimperg/aesop#54

[Joachim Breitner]

While we are at it:

import Aesop
import Mathlib

example (n : ℕ) : n > 0 → ¬ (n = n - 1) := by
  aesop

will print

aesop: error in norm simp: maximum recursion depth has been reached (use `set_option maxRecDepth <num>` to increase limit)

I assume this is because it gets n = n-1 into the goal state, and then keeps simplifying with it.

I believe the Isabelle simplifier, while generally tring to use hypotheses, has some code to recognize “obviously looping” ones like this one, and doesn't use that.

Not sure if that is a bug here, and if so, if it’s a bug with simp or aesop?

[Joachim Breitner]

Ah, certainly a problem with simp:

example (n : ℕ) : n > 0 → ¬ (n = n - 1) := by
  intros h1 h2
  simp [*] at *

but maybe aesop by default should somehow run simp in a way that avoids this?

[Jannis Limperg]

Aesop could heuristically exclude equations that will almost certainly loop from its simp call. I suspect that core wouldn't want to add functionality for this because it's not really relevant when simp is used interactively. JLimperg/aesop#55