linarith don't work as expect

Stream: mathlib4

[sinianluoye]

I implement my owned Field class, and implement instance CommRing, LinearOrder,IsStrictOrderedRing for it. the codes like:

-- Field.lean
class Field (α : Type u)  extends Add α, SMul Nat α, Mul α, Sub α, Neg α, Div α, Zero α, One α, Pow α Nat, Inv α where
 /- something -/

variable {α: Type u} [Field α]

instance (priority := default - 1) : CommRing α where
   /- something -/

-- Ordered.lean
class Ordered (α: Type u) extends LT α, LE α where
   /- something -/

variable {α} [Ordered α] {a b : α}

noncomputable instance (priority := default-1) : LinearOrder α where

-- OrderedField.lean
class OrderedField (α : Type u) extends Field α, Ordered α where
  /- something -/

variable {α: Type u} [OrderedField α] {a b c : α}

instance (priority := default-1) : IsStrictOrderedRing α where
  /- something -/

-- Bound.lean
class LeastUpperBoundProperty (α: Type u) extends Ordered α where
  /-something-/

and currentlyI I want to prove is

example {x s:α} (hx: 0 < x): s - x < s := by
  linarith --  linarith  failed here

I tried to add set_option trace.linarith true but can not find the reason.

[linarith] linarith is running on the following hypotheses: ▼
[Type u, OrderedField α, LeastUpperBoundProperty α, α, α, 0 < x, s ≤ s - x]
[linarith] ✅️ Running preprocessors ▼
  [] ✅️ Mathlib.Tactic.Linarith.splitConjunctions: split conjunctions ▼
    [] [Type u, OrderedField α, LeastUpperBoundProperty α, α, α, 0 < x, s ≤ s - x]
  [] ✅️ Mathlib.Tactic.Linarith.filterComparisons: filter terms that are not proofs of comparisons ▼
    [] [0 < x, s ≤ s - x]
  [] ✅️ Mathlib.Tactic.Linarith.removeNegations: replace negations of comparisons ▼
    [] [0 < x, s ≤ s - x]
  [] ✅️ Mathlib.Tactic.Linarith.natToInt: move nats to ints ▼
    [] [0 < x, s ≤ s - x]
  [] ✅️ Mathlib.Tactic.Linarith.strengthenStrictInt: strengthen strict inequalities over int ▼
    [] [0 < x, s ≤ s - x]
  [] ✅️ Mathlib.Tactic.Linarith.compWithZero: make comparisons with zero ▶
  [] ✅️ Mathlib.Tactic.Linarith.cancelDenoms: cancel denominators ▼
    [] []
[linarith] after preprocessing, linarith has 0 facts: ▼
[]
[linarith] hypotheses appear in 0 different types
[linarith] ❌️ running on preferred type α

anyone can help for it? thanks.

[Eric Wieser]

Can you give a #mwe with imports?

[Edward van de Meent]

(OrderedField seems to not exist in mathlib?)

[sinianluoye]

Eric Wieser said:

Can you give a #mwe with imports?

import Mathlib
import Rudin.Chapter1.Ordered
import Rudin.Chapter1.Field
import Rudin.Chapter1.OrderedField
import Rudin.Chapter1.Bound
import Rudin.Chapter1.Inequality

here , there are many lines codes to implement for these class, the test code is

variable {α: Type u} [OrderedField α] [LeastUpperBoundProperty α]

example {x s:α} (hx: 0 < x): s - x < s := by
  linarith

here, I tried to remove [LeastUpperBoundProperty α] and then linarith worked now.

LeastUpperBoundProperty defined as

variable {α : Type u} [Ordered α]

class LeastUpperBoundProperty (α: Type u) extends Ordered α where
  subset_sup_exist : ∀ (E : Set α), E ≠ ∅ ∧ BoundAbove E → ∃ a, ExistsSup E a

[sinianluoye]

Edward van de Meent said:

(OrderedField seems to not exist in mathlib?)

I wrote Field/Ordered/OrderedField for my codes... and I want to use some mathlib existed tactic for it, so I implement some instance for them

[sinianluoye]

after remove LeastUpperBoundProperty

the linarith log is:

[linarith] linarith is running on the following hypotheses: ▼
[Type u, OrderedField α, α, α, x < y, 1 + 1 > 0, x + y ≤ x * (1 + 1)]
[linarith] ✅️ Running preprocessors ▼
  [] ✅️ Mathlib.Tactic.Linarith.splitConjunctions: split conjunctions ▼
    [] [Type u, OrderedField α, α, α, x < y, 1 + 1 > 0, x + y ≤ x * (1 + 1)]
  [] ✅️ Mathlib.Tactic.Linarith.filterComparisons: filter terms that are not proofs of comparisons ▼
    [] [x < y, 1 + 1 > 0, x + y ≤ x * (1 + 1)]
  [] ✅️ Mathlib.Tactic.Linarith.removeNegations: replace negations of comparisons ▶
  [] ✅️ Mathlib.Tactic.Linarith.natToInt: move nats to ints ▼
    [] [x < y, 1 + 1 > 0, x + y ≤ x * (1 + 1)]
  [] ✅️ Mathlib.Tactic.Linarith.strengthenStrictInt: strengthen strict inequalities over int ▼
    [] [x < y, 1 + 1 > 0, x + y ≤ x * (1 + 1)]
  [] ✅️ Mathlib.Tactic.Linarith.compWithZero: make comparisons with zero ▶
  [] ✅️ Mathlib.Tactic.Linarith.cancelDenoms: cancel denominators ▼
    [] [x - y < 0, 0 - (1 + 1) < 0, x + y - x * (1 + 1) ≤ 0]
[linarith] after preprocessing, linarith has 3 facts: ▼
[x - y < 0, 0 - (1 + 1) < 0, x + y - x * (1 + 1) ≤ 0]
[linarith] hypotheses appear in 1 different types
[linarith] ✅️ running on preferred type α ▼
  [] ✅️ Invoking oracle ▼
    [] found a contradiction: [(1, 1), (3, 1)]
  [] ✅️ Building final expression ▼
    []
          x - y + (x + y - x * (1 + 1))
        should be both 0 and negative

[Eric Wieser]

Please read #mwe, this isn't one because you haven't given me something I can run

[Eric Wieser]

Ideally you can replace your somethings with sorry to minimize

[sinianluoye]

Eric Wieser said:

Please read #mwe, this isn't one because you haven't given me something I can run

Hi @Eric Wieser Could you try clone from https://github.com/sinianluoye/LeanOfRudinAnalysis and the branch is chapter1. Because there are so many defs and theorems, It is hard to provide that.

the test code located at Rudin/Chapter1/PowRat.lean linbe 15

[Kyle Miller]

Do we need a #mwe? Doesn't linarith require you use mathlib's classes, so it would be surprising if it worked with a custom Field class?

[Eric Wieser]

I think the idea is that the instance (priority := default-1) : IsStrictOrderedRing α where translates things into the mathlib classes

[Eric Wieser]

the test code located at Rudin/Chapter1/PowRat.lean linbe 15

This file doesn't exist (it should be at https://github.com/sinianluoye/LeanOfRudinAnalysis/blob/chapter1/Rudin/Chapter1/PowRat.lean#L15)

[Eric Wieser]

My guess is that either @sinianluoye is missing an instance, has prouced an instance diamond, or linarith is looking for a syntactic instance instead of a defeq one.

[sinianluoye]

Eric Wieser said:

the test code located at Rudin/Chapter1/PowRat.lean linbe 15

This file doesn't exist

here, sorry to forget push
https://github.com/sinianluoye/LeanOfRudinAnalysis/blob/chapter1/Rudin/Chapter1/PowRat.lean

[sinianluoye]

What puzzles me is that when I update the variable from {α: Type u} [OrderedField α] [LeastUpperBoundProperty α] to {α: Type u} [OrderedField α], then linarith works. I didn't even implement any instance for LeastUpperBoundProperty. :rolling_on_the_floor_laughing:

[Eric Wieser]

I would guess you are defining two unrelated < operators

[Eric Wieser]

That says "let α have one < that is compatible with the field structure, and a different one with the LUB property"

[sinianluoye]

Can I use some codes to prove that? by code analysis, LeastUpperBoundProperty extends Rudin.Ordered α and OrderedField extends Rudin.Ordered α. seems they should be same

when I use #check @LT.lt α _ I can confirm that the LT is get from Ordered.toLT
image.png

[Aaron Liu]

sinianluoye said:

Can I use some codes to prove that? by code analysis, LeastUpperBoundProperty extends Rudin.Ordered α and OrderedField extends Rudin.Ordered α. seems they should be same

when I use #check @LT.lt α _ I can confirm that the LT is get from Ordered.toLT
image.png

So that means there's now two different ways to derive a Rudin.Ordered, the one coming from OrderedField and the one coming from LeastUpperBoundProperty, and nothing to say that the two ways get you the same result

[sinianluoye]

I'm still a little puzzled. What's a good way to implement the related code? Ordered is enough to define LeastUpperBoundProperty, but for some theorems, I need both LeastUpperBoundProperty and OrderedField to complete the proof. Does this mean I cannot use linarith in the related code?

[Aaron Liu]

It means you want to unbundle ordered algebra

[Eric Wieser]

Or you need to add

class LUBOrderedField extends LeastUpperBoundProperty X, OrderedField x

because extends deduplicates typeclass members

[sinianluoye]

Thanks for your patient answers.

I also asked Copilot, and it provided two suggestions: one is similar to Eric’s suggestion, and the other is to use the mixin pattern for the Property class, for example, class LeastUpperBoundProperty (α : Type*) [Ordered α] where. I tried both of them, and they both worked.