lattice tactics

Stream: mathlib4

[Kevin Buzzard]

What tactic do I need to make a lattice game?

import Mathlib

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  hint -- no suggestions available

This is a slightly terrifying start. None of aesop, tauto, linarith work.

[Kevin Buzzard]

ChatGPT tells me it's transitivity :-)

[Yaël Dillies]

aesop (add unsafe [le_trans, lt_trans, lt_of_le_of_lt, lt_of_lt_of_le, le_of_lt did me well last time I tried something similar

[Eric Wieser]

Does cc work?

[Richard Copley]

Kevin Buzzard said:

ChatGPT tells me it's transitivity :-)

Just trans now (but you're asking for more automation?)

[Edward van de Meent]

apparently transitivity does exist? it seems to work just like trans, but it doesn't seem to have a docstring.... I'm not sure if there are functional differences...

[Kevin Buzzard]

How about

import Mathlib

example (L : Type) [Lattice L] (a b c d e: L)
    (h1 : b ≤ c) (h2 : c ≤ d) : a ⊓ b ≤ d ⊔ e := by
  sorry

[Richard Copley]

Edward van de Meent said:

apparently transitivity does exist? it seems to work just like trans, but it doesn't seem to have a docstring.... I'm not sure if there are functional differences...

It was discussed here. I don't know if things have moved on since then.

[Eric Wieser]

Is this in scope for @Geoffrey Irving's bound?

[Kevin Buzzard]

I tried Yael's suggestion and added inf_le_right, le_sup_left to the end, and the aesop call failed. I then tried aesop (add unsafe [le_trans, inf_le_right, le_sup_left]) and it worked fine.

[Geoffrey Irving]

Eric Wieser said:

Is this in scope for Geoffrey Irving's bound?

I don’t think so: bound is only for when the structure of the proof is (mostly) immediate. This is closer to linarith, though that requires more structure.

[Kevin Buzzard]

OK so the question remains open, and is now something like: is there some kind of incantation (perhaps of the form aesop (add_unsafe...) which will solve all three of these goals:

import Mathlib

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  aesop (add unsafe [le_trans, lt_trans, lt_of_le_of_lt, lt_of_lt_of_le, le_of_lt]) -- fails

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
  aesop (add unsafe [le_trans, lt_trans, lt_of_le_of_lt, lt_of_lt_of_le, le_of_lt]) -- fails


example (L : Type) [Lattice L] (a b c d e: L)
    (h1 : b ≤ c) (h2 : c ≤ d) : a ⊓ b ≤ d ⊔ e := by
  aesop (add unsafe [le_trans, lt_trans, lt_of_le_of_lt, lt_of_lt_of_le, le_of_lt,
    inf_le_right, le_sup_left]) --fails

[Anand Rao Tadipatri]

Here's a more fine-grained aesop configuration that works:

import Mathlib

attribute [aesop unsafe apply 10%] le_trans
attribute [aesop unsafe apply 10%] lt_trans
attribute [aesop safe forward] le_of_lt
attribute [aesop safe forward] lt_of_le_of_lt
attribute [aesop safe forward] lt_of_lt_of_le
attribute [aesop unsafe apply 2%] lt_of_le_of_lt
attribute [aesop unsafe apply 2%] lt_of_lt_of_le
attribute [aesop unsafe forward 2%] inf_le_right
attribute [aesop unsafe forward 2%] le_sup_left

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  aesop

example (L : Type) [Lattice L] (a b c d e: L)
    (h1 : b ≤ c) (h2 : c ≤ d) : b ⊓ a ≤ d ⊔ e := by
  aesop

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
  aesop

[Kevin Buzzard]

How does one turn these ideas into a standalone tactic lattice_tac?

[Kevin Buzzard]

@Igor Pietrzak I'm wondering if we can use these ideas in the filter game.

[Igor Pietrzak]

Wouldn't you then need a lattice world where you prove these and that a filter is a lattice? Also for

example (L : Type) [Lattice L] (a b c d e: L)
    (h1 : b ≤ c) (h2 : c ≤ d) : b ⊓ a ≤ d ⊔ e := by
  aesop

Would be good to split b ⊓ a ≤ b and d ≤ d ⊔ e into theorems you can apply.

[Kevin Buzzard]

The question is whether one wants to solve levels like this by applying lots of theorems or applying one tactic. Those theorems you cite (inf_le_left etc) either need to be taught explicitly or subsumed by a tactic.

[Kim Morrison]

Kevin Buzzard said:

How does one turn these ideas into a standalone tactic lattice_tac?

For you, or anyone else who would like to package this as lattice_tac, there are a number of examples in Mathlib.

See e.g. file#CategoryTheory/Category/Basic for the setup of aesop_cat, with a specialized rule set.

[Anand Rao Tadipatri]

I realized that most of those percentages weren't actually needed -- what mattered was telling aesop how to use each lemma (i.e., whether to use the lemma in forward reasoning or to apply it to a goal).

To create a tactic out of this, one can define an aesop rule set in a separate file

import Mathlib

declare_aesop_rule_sets [Lattice]

and import that into another file that adds the specific lemmas to the rule set and defines a macro for the tactic.

attribute [aesop unsafe apply (rule_sets := [Lattice])] le_trans
attribute [aesop unsafe apply (rule_sets := [Lattice])] lt_trans
attribute [aesop safe forward (rule_sets := [Lattice])] le_of_lt
attribute [aesop safe forward (rule_sets := [Lattice])] lt_of_le_of_lt
attribute [aesop safe forward (rule_sets := [Lattice])] lt_of_lt_of_le
attribute [aesop unsafe apply (rule_sets := [Lattice])] lt_of_le_of_lt
attribute [aesop unsafe apply (rule_sets := [Lattice])] lt_of_lt_of_le
attribute [aesop unsafe forward (rule_sets := [Lattice])] inf_le_left
attribute [aesop unsafe forward (rule_sets := [Lattice])] inf_le_right
attribute [aesop unsafe forward (rule_sets := [Lattice])] le_sup_left
attribute [aesop unsafe forward (rule_sets := [Lattice])] le_sup_right

macro "aesop_lattice" c:Aesop.tactic_clause* : tactic =>
  `(tactic| aesop $c* (rule_sets := [Lattice]))

macro "aesop_lattice?" c:Aesop.tactic_clause* : tactic =>
  `(tactic| aesop? $c* (rule_sets := [Lattice]))

Here is the tactic in action:

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) : a ≤ e := by
  aesop_lattice

example (L : Type) [Lattice L] (a b c d e: L)
    (h1 : b ≤ c) (h2 : c ≤ d) : b ⊓ a ≤ d ⊔ e := by
  aesop_lattice

example (L : Type) [PartialOrder L] (a b c d e : L)
    (h1 : a < b) (h2 : b < c) (h3 : c < d) (h4 : d < e) : a < e := by
  aesop_lattice

[Joachim Breitner]

Kim Morrison said:

Kevin Buzzard said:

How does one turn these ideas into a standalone tactic lattice_tac?

For you, or anyone else who would like to package this as lattice_tac, there are a number of examples in Mathlib.

See e.g. file#CategoryTheory/Category/Basic for the setup of aesop_cat, with a specialized rule set.

Does having custom tactic for each of these scale and compose well? If all they do is add aesop rules, wouldn't it be nicer if it's not aesop_cat and aesop_order but aesop [cat] and aesop [order] so that one can write aesop [cat, order]?

(Right now aesop_cat also changes a setting, thats of course not modular, do maybe the question is hypothetical for now.)

[Anand Rao Tadipatri]

I agree, I think I would prefer to have that kind of composability. If the lemmas for each of these tactics are put into aesop rule sets, then your syntax could be a short-hand for invoking the specific rule sets.

open Aesop.Frontend.Parser

macro "aesop" "[" rule_sets:ruleSetSpec,+,? "]" c:Aesop.tactic_clause* : tactic =>
  `(tactic| aesop (rule_sets := [$rule_sets,*]) $c*)