aesop_graph vs aesop

Stream: mathlib4

[Damiano Testa]

Dear All,

this question arises from a discussion with a student -- I do not know my way around the SimpleGraph part of Mathlib, so this may be a known feature.

In the code below, the symm and loopless fields of SimpleGraph are "auto-solved" by aesop_graph. symm works, while loopless does not. So far, so good. However, aesop does prove loopless. Is this expected?

Thanks!

import Mathlib.Combinatorics.SimpleGraph.Basic

example : SimpleGraph (Fin 2) where
  Adj x y := x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0
--  loopless a b := by aesop  --  <--- uncomment and `aesop` actually succeeds
/-
tactic 'aesop' failed, failed to prove the goal after exhaustive search.

⊢ Irreflexive fun x y => x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0
-/

The error message is also kind of ironic: "aesop does not solve it", so you try with aesop and it does actually solve it!

[Kyle Miller]

I'm not sure how carefully aesop_graph has been reviewed -- it appeared during the port to replace the Lean 3 obviously tactic, and I don't know enough about aesop to know if it's been configured correctly!

[Damiano Testa]

Fair enough!

A simple way out could be to make the error message say tactic 'aesop_graph', rather than tactic 'aesop', to avoid similar oddities!

[Kyle Miller]

This doesn't seem good:

example : SimpleGraph (Fin 2) where
  Adj x y := x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0
  loopless := by
    aesop_graph_nonterminal
    /-
    aesop: error in norm unfold: maximum recursion depth has been reached
    (use `set_option maxRecDepth <num>` to increase limit)
    -/

[Kyle Miller]

Hmm, I'm not seeing that aesop can solve it:

import Mathlib.Combinatorics.SimpleGraph.Basic

example : SimpleGraph (Fin 2) where
  Adj x y := x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0
  loopless := by aesop -- error

[Damiano Testa]

aesop can solve it: it is aesop_graph that cannot.

[Damiano Testa]

But when aesop_graph fails, it reports that aesop could not solve it, which is not true.

[Kyle Miller]

@Damiano Testa I had an accidental double negative in what I said, check the code snippet, I don't see aesop working.

[Damiano Testa]

I used loopless x y := by aesop: note the introduced x y.

[Damiano Testa]

But aesop_graph fails also with x y.

[Damiano Testa]

Anyway, maybe the answer is simply: try aesop, if aesop_graph does not work!

[Damiano Testa]

After all, they are different algorithms, so they will perform differently.

[Damiano Testa]

I just found it a little ironic that aesop_graph fails to prove that the complete graph on two vertices is a graph! :upside_down:

[Anand Rao Tadipatri]

@Damiano Testa Thanks for bringing up this issue with aesop_graph. The culprit seems to be this line, which adds an aesop attribute to Ne.irrefl to show that a completeGraph is a graph.

Here is a snippet where aesop_graph works:

import Mathlib.Combinatorics.SimpleGraph.Basic

erase_aesop_rules [safe (rule_sets [SimpleGraph]) Ne.irrefl]

example : SimpleGraph (Fin 2) where
  Adj x y := x = 0 ∧ y = 1 ∨ x = 1 ∧ y = 0
  loopless := by aesop_graph -- now works

[Damiano Testa]

Anand, thank you very much!

[Damiano Testa]

In fact, now that it works, you can completely omit the field!