order beating grind

Stream: lean4

[Alex Meiburg]

I've seen Kim requesting a few times for things that maybe grind could/should do. Here's a simple problem I just ran into:

import Mathlib
example {α : Type*} [PartialOrder α] (a b : α) (h : a ≤ b) : a = b ↔ b ≤ a := by
  constructor <;> order

This works. But constructor <;> grind doesn't work. (Indeed, I would hope that just grind suffices.)

[Julia Scheaffer]

It can be solved by telling grind about docs#le_antisymm

import Mathlib
example {α : Type*} [PartialOrder α] (a b : α) (h : a ≤ b) : a = b ↔ b ≤ a := by
  grind [→ le_antisymm]

Perhaps le_antisymm should be marked with a grind annotation.

[Kim Morrison]

I suspect we'll just implement a custom order solver in grind at some point, so I've been holding off shiny such annotations.

[Kim Morrison]

(Update: hopefully this will arrive in v4.25.0-rc1)

[Asei Inoue]

nice!

[Jovan Gerbscheid]

What will be supported by the order module in grind? Will it support linear orders, partial orders and preorders? Will it support top/bottom and max/min/sup/inf?

[Henrik Böving]

At least linear, partial and pre orders as well as modules (i.e. linear combinations). Afaik we didn't talk about lattice theory yet.

[Alex Meiburg]

Is there a way for grind to speculatively use the density of a dense linear order? e.g. once we've derived a minimal set of LE relations, you can then also add an element between each minimal pair.

Obviously would make sense the same way as a @[grind] rule since it would immediately loop, but it could be a cool feature/option to have within a module. I think that would substantially improve grind's power in a lot of analysis stuff.

[Jovan Gerbscheid]

I noticed that due to the new order module the following gives a kernel error on the current nightly.

example (a b : Int) (h1 : ¬(a < b)) (h2 : ¬(b < a)) : a = b := by
  grind
/-
(kernel) application type mismatch
  Lean.Grind.Order.eq_of_le_of_le
    (Lean.Grind.Order.eq_mp
      (id
        (Lean.Grind.CommRing.le_norm_expr (Lean.RArray.branch 1 (Lean.RArray.leaf a) (Lean.RArray.leaf b))
          ((Lean.Grind.CommRing.Expr.var 0).add
            ((Lean.Grind.CommRing.Expr.num 1).neg.mul (Lean.Grind.CommRing.Expr.var 1)))
          (Lean.Grind.CommRing.Expr.num 0) (Lean.Grind.CommRing.Expr.var 0)
          ((Lean.Grind.CommRing.Expr.var 1).add (Lean.Grind.CommRing.Expr.intCast 0)) (eagerReduce (Eq.refl true))))
      h2)
argument has type
  a ≤ b + IntCast.intCast 0
but function has type
  a ≤ b → b ≤ a → a = b
-/

[Aaron Liu]

is adding zero not a defeq anymore

[Aaron Liu]

I guess with Int...

[Vasilii Nesterov]

Is grind meant to be complete for partial orders? This example fails on nightly:

example {α : Type} [LE α] [LT α] [Std.LawfulOrderLT α] [Std.IsPartialOrder α] (a b c d e : α) (h1 : a ≤ b) (h2 : b ≤ c) (h3 : c ≤ d) (h4 : d ≤ e) (h5 : b ≠ d) :
    a < e := by
  grind

[Henrik Böving]

This is going to be supported in the future