Help with aesop

Stream: new members

[john johnson]

I have this code and I wanted to prove the last theorem using aesop, and even though the proof consists of only succesive applications of Order.trans, aesop is only able to prove it after I insert the first apply manually and I'm not sure I understand why considering it's able to provide the remaining steps. What am I doing wrong?

import Mathlib.Tactic

def _xor (p q : Prop) := ¬(p ↔ q)

infix:50 " ∨+ " => _xor

class Order (X : Type) where
  S : X -> X -> Prop
  tri : ∀x y : X, (x = y) ∨+ (S x y) ∨+ (S y x)
  trans : ∀{x y z: X}, (S x y) -> (S y z) -> (S x z)

instance (X : Type) [Order X] : LT X where
  lt := fun x y => Order.S x y

instance (X : Type) [Order X] : LE X where
  le := fun x y => Order.S x y ∨ x = y

add_aesop_rules unsafe apply 50% [Order.trans]

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  apply Order.trans
  aesop
  aesop

[Kevin Buzzard]

Try add_aesop_rules safe forward Order.trans instead?

[john johnson]

It didn't work unfortunately, I still get
tactic 'aesop' failed, made no progress

[Kevin Buzzard]

OK now at a computer, I'll take a look. Your code doesn't compile for me (with set_option autoImplicit false) so you might want to think about fixing that first, this usually means that your code doesn't say what you think it says.

[Kevin Buzzard]

The autoimplicit issue is with Order.tri so it doesn't affect your question. I believe that the reason aesop isn't doing what you want it to do is that it can't see through < to get Order.S.

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  -- statement about `<`
  apply Order.trans
  -- statements about `S`, so `aesop` now works
  ...

Here's an example of how to fix it:

lemma Order.lt_trans (X : Type) [Order X] (x y z : X) (h1 : x < y) (h2 : y < z) : x < z :=
  Order.trans h1 h2

-- this is the lemma `aesop` actually needs
add_aesop_rules safe forward Order.lt_trans

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  aesop

Lean doesn't just unfold things willy-nilly, this would cause chaos in general. So although you taught Aesop about Order.trans, it still didn't know a thing about <.

[Kevin Buzzard]

With the set_option autoImplicit true footgun on (I have this off by default on all my projects), your Order.tri is

Order.tri {X : Type} [self : Order X] {y x : X} : (∀ (x y : X), (x = y) ∨+ Order.S x y) ∨+ Order.S y x

which is syntactically equivalent to

Order.tri {X : Type} [self : Order X] {y x : X} : (∀ (a b : X), (a = b) ∨+ Order.S a b) ∨+ Order.S y x

which I'm sure is not at all what you want.

[john johnson]

I see, I was thinking aesop would be able to find this proof since it only uses rules that it knows about

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  apply Order.trans
  apply Order.trans h1 h2
  exact h3

Could there still be a way to make it find this proof instead or any proof using Order.trans only?

[Kevin Buzzard]

Your proof is abusing definitional equality, so is not good style. I'm not an expert in this sort of thing, but my instinct is that if Lean sees a hypothesis x < y and it has a lemma which has hypothesis Order.S x y then no way will you get it to apply that lemma, because any system which allows the unfolding of x < y is a system which will immediately grind to a halt the moment it sees the kind of monstrosities which we've constructed in mathlib.

One approach if you're desperate to make this sort of thing work is to use notation x < y to mean Order.S x y, instead of a typeclass, because Lean will happily look through the definition of notation. It will also look through reducible definitions, but LT is not your definition so you don't get to set its reducibility level.

notation x "<" y => Order.S x y -- this might have unfortunate consequences elsewhere

add_aesop_rules unsafe apply 50% [Order.trans]

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  aesop -- works, because x < y is now *syntactically* Order.S x y

[Kevin Buzzard]

Another approach is to teach the system that x < y <-> S x y, like this:

instance (X : Type) [Order X] : LT X where
  lt := fun x y => Order.S x y

@[simp]
lemma Order.lt_def {X : Type} [Order X] (x y : X) : x < y ↔ Order.S x y := by rfl

add_aesop_rules safe forward Order.trans

theorem test (X : Type) [Order X] (x y z w: X) (h1 : x < y) (h2 : y < z) (h3 : z < w): x < w := by
  aesop

[Kevin Buzzard]

Be warned now though that the simplifier will constantly replace x < y with S x y, which may or may not be what you want.

[john johnson]

I like this second approach, my only problem is that so far it seemed harder to figure out what aesop wants to complete a proof than to just do the proof manually, and I was hoping I could use to spend less time proving "obvious" things. Or maybe I just don't know how to use it properly

[Kevin Buzzard]

My initial mental model of aesop was that it would just do everything automatically, but more recently I've come to understand that it needs training. Understanding that x < y is syntactically (i.e. notation for) LT.lt x y but only definitionally Order.S x y is I guess important for your situation here, and I guess tagging lt_def @[simp] is solving that problem. aesop is not going to use lemmas it's not been told about though. One approach used in mathlib is the aesop_cat approach, where a bespoke trained version of aesop is used to prove results in category theory.

[john johnson]

Maybe one last thing, is there a way to make aesop use lemmas without having to mention them explicitly? For example passing an entire file and having it look for things that could be useful?

[Kevin Buzzard]

I'm afraid that's beyond my pay grade, I'm but a lowly mathematician. Hopefully someone else will chime in.

[john johnson]

No problem, thanks for the help :smile:

[Mario Carneiro]

It depends on what you mean by "mentioning them explicitly". The proof above is a plain call to aesop that does not mention any lemmas, but you have to tag lemmas first before that will work

[Mario Carneiro]

it's similar to simp in that regard

[Mario Carneiro]

it does not crawl the library looking for lemmas

[Mario Carneiro]

the only tactics I'm aware of that do that are exact? and apply?

[john johnson]

I understand, I was wondering if there is a way to make it behave like exact? in that sense or maybe an alternative with that behaviour