Combining two order structures

Stream: new members

[Pieter Cuijpers]

I'm trying to combine Order.Frame and OrderedAddCommMonoid, but somehow Lean does not see that this should (I think) be working on the same order structure. How do I fix this? I seem to be overlooking somthing.

This is an example of a trivial proof that works:

variable {Time: Type*} [OrderedAddCommMonoid Time]

theorem add_le_left_time : ∀ (a b c : Time), a ≤ b → c + a ≤ c + b := by
  intros a b c h
  exact OrderedAddCommMonoid.add_le_add_left a b h c

But when I add [Order.Frame Time] (or [PartialOrder Time], or similar)

variable {Time: Type*} [OrderedAddCommMonoid Time] [Order.Frame Time]

theorem add_le_left_time : ∀ (a b c : Time), a ≤ b → c + a ≤ c + b := by
  intros a b c h
  exact OrderedAddCommMonoid.add_le_add_left a b h c

I get an error that h is of the wrong type. It seems that Lean get's confused about which ≤ I mean.

What is happening here?

[Kenny Lau]

@Pieter Cuijpers OrderedAddCommMonoid was removed for this very reason, and replaced with IsOrderedAddMonoid. Perhaps you are using an older version of Mathlib.

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/commit/1cd54028c4522f638c29d173737f831552055c15#diff-b7e2a9cad39a929d367ebafb50a8fee9a683847bfe6cf4965d26c8b73d938162
ah, it was removed last week (but deprecated in April)

[Kenny Lau]

Whenever you have assumptions like [OrderedAddCommMonoid Time] [Order.Frame Time], both classes carry a (different) definition of <=, and there is no guarantee that they are the same relation.

[Pieter Cuijpers]

Thanks, that clarifies things. Indeed, we have been working on an older version for a while for this work. I'll tell my student to update ;-)

[Kenny Lau]

@Pieter Cuijpers how old is the version? your student might want to update it slowly, since there is very little backwards compatibility

[Ruben Van de Velde]

That is, it's usually easier to bump update to lean/mathlib v4.n.0, 4.(n+1).0, 4.(n+2).0, ... rather than to the most recent version in one step