Zulip Chat Archive

Stream: Is there code for X?

Topic: Decision procedure for `(ℕ,+,-,≤)`

Geoffrey Irving (Dec 24 2023 at 07:37):

Do we have the decision procedure for ℕ with addition, subtraction, and ordering?

Yaël Dillies (Dec 24 2023 at 07:38):

The tactic omega that recently landed?

Geoffrey Irving (Dec 24 2023 at 07:39):

Perfect, thank you!

Kevin Buzzard (Dec 24 2023 at 08:41):

We've been waiting for this tactic in lean 4 for years and it just landed a few days ago to no fanfare at all, I was very surprised. Perhaps it was just that Scott was going on holiday and didn't have time to announce it, but I am over the moon!

Geoffrey Irving (Dec 24 2023 at 11:50):

Apparently you just have to ask if it exists!

Ruben Van de Velde (Dec 24 2023 at 12:17):

Is there a decision procedure for decision procedures?

Pedro Sánchez Terraf (Dec 24 2023 at 15:36):

Ruben Van de Velde said:

Is there a decision procedure for decision procedures?

Beware of the Haunting Problem :ghost:

Patrick Massot (Dec 24 2023 at 15:50):

Kevin Buzzard said:

We've been waiting for this tactic in lean 4 for years

It's really funny how it feels like we have been using Lean 4 for years. Kevin, we started six months ago.

Kevin Buzzard (Dec 24 2023 at 15:51):

We did, but lean 4 has existed for years and omega was deprecated in lean 3 quite some time ago

Yongyi Chen (Dec 24 2023 at 16:49):

I just grabbed the latest mathlib and I'm still getting tactic 'Mathlib.Tactic.omega' has not been implemented

Eric Rodriguez (Dec 24 2023 at 18:49):

Same, I was excited for this - can't seem to find a PR for it either?

Joachim Breitner (Dec 24 2023 at 21:46):

https://github.com/leanprover/std4/pull/463

Yongyi Chen (Dec 25 2023 at 06:46):

It's because of line 217 in Mathlib.Mathport.Syntax.lean. That file has stubs for tactics which override implemented tactics to claim to the user they are still unimplemented, if Mathlib is imported.