Omega with Field not working properly?

Stream: new members

[Jihoon Hyun]

I thought this would work well.
Is this the expected behavior of omega?

import Mathlib.Algebra.Order.Field.Defs
import Mathlib.Data.Set.Basic
variable (F : Type*) [Field F]

class A (S : Set F) where
  prop : ⦃x : F⦄ → x ∈ S → ⦃y : F⦄ → y ∈ S → x + y ∈ S

def P [LinearOrderedField F] : Set F := fun x => 0 ≤ x

instance [LinearOrderedField F] : A F (P F) where
  prop x h₁ y h₂ := by
    omega -- error: False

[Kyle Miller]

Yes, omega is for Nat and Int arithmetic only.

[Kyle Miller]

Here:

variable (F : Type*)

class A [Field F] (S : Set F) where
  prop : ⦃x : F⦄ → x ∈ S → ⦃y : F⦄ → y ∈ S → x + y ∈ S

def P [LinearOrderedField F] : Set F := {x | 0 ≤ x}

instance [LinearOrderedField F] : A F (P F) where
  prop x h₁ y h₂ := by
    simp [P] at *
    linarith

[Kyle Miller]

I needed to move the Field instance because it was causing trouble when there was both Field F and LinearOrderedField F in context.

[Kyle Miller]

(Note that the first line of the omega docstring, which you can see when you hover over omega, is "The omega tactic, for resolving integer and natural linear arithmetic problems.")

[Jihoon Hyun]

Thanks a lot! So the collision of Field and LinearOrderedField was the problem here.

[Patrick Massot]

Yes, those were equipping your type with two completely unrelated field structures, which was bound to confuse Lean a lot.