Teach `aesop` about inequalities

Stream: general

[Violeta Hernández]

Is it possible to teach aesop some basic facts about inequalities? In particular, I'd like if the following worked:

import Mathlib

example {α : Type _} [Preorder α] {a b : α} : a < b → b < a → False := by
  aesop

(for context: I'm trying to use aesop to solve a more tedious goal, and it succeeds completely, except that it's left with goals with contradictory hypotheses it can't then close)

[Violeta Hernández]

Oh nice, this does work

import Mathlib

example {α : Type _} [Preorder α] {a b : α} : a < b → b < a → False := by
  aesop (add simp lt_asymm)

Not sure if this is an intended solution though (how is lt_asymm getting applied through simp?)

[Michael Rothgang]

Did you try the bound tactic? It uses aesop; I don't have much experience using it yet, but perhaps it would also work?

[Kevin Buzzard]

Here's a cool approach: #mathlib4 > lattice tactics @ 💬

[Jannis Limperg]

Violeta Hernández said:

Not sure if this is an intended solution though (how is lt_asymm getting applied through simp?)

When simp sees a theorem of the form P -> Not Q, it rewrites Q to False, provided that a nested call to simp rewrites P to True. When you use simp_all (as Aesop does), hypotheses are taken into account, so if P is in the context, the nested simp call rewrites it to True.

A likely more performant solution would be use lt_asymm as a forward rule (@[aesop safe forward]). This will look for hypotheses a < b and b < a in the context and derive False from them.

Actually, for now you need to register a variant of lt_asymm where the Not is explicitly unfolded, i.e. lt_asymm' : a < b -> b < a -> False instead of a < b -> Not (b < a). I should fix this at some point.