Order.Circular mathlib4#1489

Stream: mathlib4

[Ruben Van de Velde]

This has a tauto call that times out - would be great if someone could take a look

[David Renshaw]

I think part of the problem is that we should be calling casesMatching with (recursive := true).

[Thomas Murrills]

I already ported Order.Circular but was waiting on tauto—this was before we started immediately making PR’s for everything. I’m surprised it didn’t show up when running the port status script…

[Thomas Murrills]

Unless my branch was second somehow? But it was definitely clear on the port status script when I started it…it’s on the branch order.circular

[Thomas Murrills]

No, my port was almost a month ago

[Thomas Murrills]

But your port does clean up a couple comments mine missed... :)

[Thomas Murrills]

All I'll say is that the name should be SBtw, not Sbtw, as discussed here, since it's short for Strictly Between

[Thomas Murrills]

Also we can now fix the tauto issue by removing the set ...s and simply doing

    have := le_trans a b c
    have := le_trans b c a
    have := le_trans c a b
    tauto

I'm going to commit this on the current PR if that's alright @Ruben Van de Velde ?

[Thomas Murrills]

(I'll commit now, and we can always revert if necessary :) )

[Thomas Murrills]

(I'm also going to change Sbtw to SBtw and we can similarly revert if we want.)

[Thomas Murrills]

Actually, I'm curious—why did e.g. HasBtw become Btw? This leaves us with btw : α → α → α → Prop, which bucks the naming convention.

[Eric Wieser]

Is that different to how things are handled for docs4#Membership .mem or docs4#LE .le ?

[Yaël Dillies]

docs4#Membership.mem

[Ruben Van de Velde]

Bucks the naming convention how? (And sorry for stepping on your toes - I thought I checked the PRs before starting)

[Thomas Murrills]

Huh, all of these docs links give me 404 page not found.

[Eric Wieser]

Looks like you can't link to structure fields

[Yaël Dillies]

Weird. it's there: https://leanprover-community.github.io/mathlib4_docs/Init/Prelude.html#Membership.mem

[Eric Wieser]

I'm now confused; what is the naming rule that justifies these names?

[Thomas Murrills]

Ruben Van de Velde said:

Bucks the naming convention how? (And sorry for stepping on your toes - I thought I checked the PRs before starting)

Well, functions are meant to be named as though they were elements of their return type, and elements of Prop are meant to be UpperCamelCase

[Thomas Murrills]

(And no problem! Bound to happen in a project as big as this sooner or later :) )

[David Renshaw]

I think part of the problem is that we should be calling casesMatching with (recursive := true)

If I do this and also bump maxHeartbeats to 500000, then tauto does eventually succeed.

[Ruben Van de Velde]

Oh right, it's a Prop. I defer to anyone who's thought more about the naming convention :)

[Thomas Murrills]

There is something to be said for patterning it after mem and le though! Is there a general pattern where something that was has_foo, foo in mathlib3 becomes Foo, foo in mathlib4 despite types? Or is this just a quirk of mem and le in particular?

[Thomas Murrills]

What's the general rule?

[Thomas Murrills]

(btw (pun intended), just to avoid race conditions, I'm going to try to add the remaining docstrings now :) )

[David Renshaw]

I have some fixes that I think should make tauto work here, without needing to bump the timeout. I hope to have a PR ready later tonight.

[Thomas Murrills]

Neat! Just in case it got lost in the messages, though, tauto already works as-is with the new compactified version of the proof (which eliminates the sets)—just so you don’t feel rushed :)

[David Renshaw]

ah, I see your fix here: https://github.com/leanprover-community/mathlib4/pull/1489/commits/4ae95c0700bcf42a4ee7522625119e630e4a6050

[David Renshaw]

Performance improvements here: https://github.com/leanprover-community/mathlib4/pull/1507

[David Renshaw]

I also observe a rather dramatic performance improvement if I switch some of the ~q() matching to plain Expr pattern matching. (I think such a change would belong in a separate pull request.)

[Jannis Limperg]

This still seems strangely slow. Aesop dispatches the test case from your PR in negligible time:

import Aesop
import Mathlib.Tactic.Tauto

example {α : Type} [Preorder α] (a b c : α) (x₀ x₁ x₂ : Prop)
 (this1 : x₀ → x₁ → a ≤ c)
 (this2 : x₁ → x₂ → b ≤ a)
 (this3 : x₂ → x₀ → c ≤ b) :
    ((x₀ ∧ ¬b ≤ a) ∧ x₁ ∧ ¬c ≤ b ∨
         (x₁ ∧ ¬c ≤ b) ∧ x₂ ∧ ¬a ≤ c ∨ (x₂ ∧ ¬a ≤ c) ∧ x₀ ∧ ¬b ≤ a ↔
       (x₀ ∧ x₁ ∨ x₁ ∧ x₂ ∨ x₂ ∧ x₀) ∧
         ¬(c ≤ b ∧ b ≤ a ∨ b ≤ a ∧ a ≤ c ∨ a ≤ c ∧ c ≤ b)) :=
by aesop

[David Renshaw]

Yeah, I'm guessing aesop has better heuristics and doesn't waste as much time with inefficient pattern matching.

[David Renshaw]

My main objective here is to achieve parity with mathlib3 tauto, which takes about 3 seconds on this goal.

[David Renshaw]

[From PR]

When I try your example on this branch, I still get a large number of timeouts at isDefEq and then a failure. Same with maxHeartbeats 1000000.

@Jannis Limperg I just tried again, and it seems to work for me (but is slow). Maybe you need to clear some local state?

[Jannis Limperg]

Weird. I'll try again.

[Jannis Limperg]

lake clean fixed the issue with the example.

The Aesop proof relies heavily on simp_all to finish off goals after splitting disjunctions. Since this seems to be very fast, it could also be interesting for tauto.

[Jannis Limperg]

A potential culprit for tauto slowness could be the repeated calls to contradiction. I had this in the default Aesop rule set at some point and it took up a large percentage of overall execution time, so I threw it out again. This is probably not an option for tauto, but it may be a good place to look for optimisation opportunities.

[David Renshaw]

Yeah, using some of these aesop learnings to improve tauto is probably a good idea. Shorter term, though, I see no reason not to just use aesop in the proof (for Preoder.toCircularPreorder) that inspired this discussion, since that saves us several seconds, and it's already imported.