Defeq with OrderDual and Multiplicative/Additive

Stream: mathlib4

[Daniel Weber]

Is the defeqness between αᵒᵈᵒᵈ = α and Multiplicative (Additive α) = α OK to use? In #18786 I'm trying to define an equivalence Valuation R Γ₀ ≃ AddValuation R (Additive Γ₀)ᵒᵈ where AddValuation is defined as Valuation R (Multiplicative Γ₀ᵒᵈ), but

import Mathlib

section
variable [LinearOrderedCommMonoidWithZero α]

instance instLinearOrderedAddCommMonoidWithTopOrderDualAdditive :
    LinearOrderedAddCommMonoidWithTop (Additive α)ᵒᵈ where
  top := OrderDual.toDual (Additive.ofMul 0)
  top_add' := fun a ↦ zero_mul (Additive.toMul (OrderDual.ofDual a))
  le_top := fun a ↦ @zero_le' _ _ (Additive.toMul (OrderDual.ofDual a))

end

variable {Γ₀ : Type*} [Ring R] [LinearOrderedCommMonoidWithZero Γ₀]

def toAddValuation : Valuation R Γ₀ ≃ AddValuation R (Additive Γ₀)ᵒᵈ := Equiv.refl _

doesn't work, as the two instances (on Γ₀ and Multiplicative (Additive Γ₀)ᵒᵈᵒᵈ) aren't defeq. What is the cause of this?

[Eric Wieser]

It would be better to write the definition out properly, since that way simps will generate the right lemmas, and people can't unfold it to get nonsense

[Yaël Dillies]

It would be interesting to find the culprit anyway. Can you use convert on the instances to find out which fields don't match?

[Daniel Weber]

It just reduces to

⊢ inst✝ =
  let __src := Multiplicative.orderedCommMonoid;
  let __src_1 := Multiplicative.linearOrder;
  LinearOrderedCommMonoidWithZero.mk ⋯ ⋯ ⋯

[Daniel Weber]

Using trace.Meta.isDefEq I found the problem: docs#OrderDual.instLinearOrder doesn't copy the docs#Ordering, and instead uses docs#compareOfLessAndEq

[Daniel Weber]

Is there a good way to define it? a = a.swap.swap isn't defeq

[Yaël Dillies]

Daniel Weber said:

a = a.swap.swap isn't defeq

Really? Can you provide a MWE?

[Daniel Weber]

import Mathlib

variable (a : Ordering)

/--

error: failed: a =~ a.swap.swap is not true
---
info: [Meta.isDefEq] ✅️ Sort ?u.3 =?= Type
---
info: [Meta.isDefEq] ✅️ Ordering =?= Ordering
[Meta.isDefEq] ❌️ a =?= a.swap.swap
  [Meta.isDefEq] ❌️ a =?= match a.swap with
      | Ordering.lt => Ordering.gt
      | Ordering.eq => Ordering.eq
      | Ordering.gt => Ordering.lt
    [Meta.isDefEq.onFailure] ❌️ a =?= match a.swap with
        | Ordering.lt => Ordering.gt
        | Ordering.eq => Ordering.eq
        | Ordering.gt => Ordering.lt
---
info: [Meta.isDefEq] ✅️ Ordering =?= Ordering
[Meta.isDefEq] ✅️ Ordering =?= Ordering
-/
#guard_msgs in
set_option trace.Meta.isDefEq true in
#guard_expr a =~ a.swap.swap

[Yaël Dillies]

Ah yes, because it's hidden behind a recursor :sad:

[Yaël Dillies]

Can we just remove the Ordering field from LinearOrder? It seems more suited as a mixin anyway

[Daniel Weber]

Ah, we could define it as compare b a

[Daniel Weber]

This seems to work. Any comments, or should I PR this?

import Mathlib

instance instOrd (α : Type*) [Ord α] : Ord αᵒᵈ where
  compare a b := compare b.ofDual a.ofDual

instance instLinearOrder (α : Type*) [LinearOrder α] : LinearOrder αᵒᵈ where
  __ := inferInstanceAs (PartialOrder αᵒᵈ)
  __ := inferInstanceAs (Ord αᵒᵈ)
  le_total := fun a b : α ↦ le_total b a
  max := fun a b ↦ (min a b : α)
  min := fun a b ↦ (max a b : α)
  min_def := fun a b ↦ show (max .. : α) = _ by rw [max_comm, max_def]; rfl
  max_def := fun a b ↦ show (min .. : α) = _ by rw [min_comm, min_def]; rfl
  decidableLE := (inferInstance : DecidableRel (fun a b : α ↦ b ≤ a))
  decidableLT := (inferInstance : DecidableRel (fun a b : α ↦ b < a))
  decidableEq := (inferInstance : DecidableEq α)
  compare_eq_compareOfLessAndEq a b := by simp [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]; congr

variable [LinearOrder α] in
#guard_expr (inferInstance : LinearOrder α) =~ (inferInstance : LinearOrder αᵒᵈᵒᵈ)

[Yaël Dillies]

Please PR!

[Daniel Weber]

#19776