diamond on order of prod

Stream: new members

[Yakov Pechersky]

Here is another diamond I discovered today:

import algebra.module.ordered

universes u v w

variables {M : Type v} {N : Type w}

lemma fails [hM : ordered_add_comm_group M] [hN :ordered_add_comm_group N] (a b : M) (c d : N) :
  @has_lt.lt.{(max v w)} (prod.{v w} M N)
    (@preorder.to_has_lt.{(max v w)} (prod.{v w} M N)
       (@partial_order.to_preorder.{(max v w)} (prod.{v w} M N)
          (@ordered_add_comm_monoid.to_partial_order.{(max v w)} (prod.{v w} M N)
             (@ordered_cancel_add_comm_monoid.to_ordered_add_comm_monoid.{(max v w)} (prod.{v w} M N)
                (@prod.ordered_cancel_add_comm_monoid.{v w} M N
                   (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid.{v} M hM)
                   (@ordered_add_comm_group.to_ordered_cancel_add_comm_monoid.{w} N hN))))))
    (@prod.mk.{v w} M N a c)
    (@prod.mk.{v w} M N b d) ↔
  @has_lt.lt.{(max v w)} (prod.{v w} M N)
    (@prod.has_lt.{v w} M N
       (@preorder.to_has_lt.{v} M
          (@partial_order.to_preorder.{v} M (@ordered_add_comm_group.to_partial_order.{v} M hM)))
       (@preorder.to_has_lt.{w} N
          (@partial_order.to_preorder.{w} N (@ordered_add_comm_group.to_partial_order.{w} N hN))))
    (@prod.mk.{v w} M N a c)
    (@prod.mk.{v w} M N b d) :=
begin
  sorry,
end

[Yakov Pechersky]

That was in this context:

lemma prod.lt_ext_iff' [preorder M] [preorder N] {a b : M} {c d : N} :
  ((a, c) : M × N) < (b, d) ↔ a < b ∨ a = b ∧ c < d := iff.rfl

lemma prod.lt_ext_iff [preorder M] [preorder N] {a b : M × N} :
  (a : M × N) < b ↔ a.fst < b.fst ∨ a.fst = b.fst ∧ a.snd < b.snd := iff.rfl

variables {R : Type u} [linear_ordered_semiring R]
  [ordered_add_comm_group M] [ordered_add_comm_group N]
  [module R M] [module R N]
  [ordered_module R M] [ordered_module R N]

set_option pp.all true

instance prod.ordered_module' : ordered_module R (M × N) :=
begin
  split,
  { rintros ⟨a, c⟩ ⟨b, d⟩ k h kpos,
    rw @prod.lt_ext_iff M N _ _ (a, c) (b, d) at h, -- here
    sorry },
  { sorry },
end

[Yakov Pechersky]

Aha, the le and lt instances we have aren't compatible currently.

import order.basic

universes v w

variables {M : Type v} {N : Type w}

def prod.preorder_current [preorder M] [preorder N] : preorder (M × N) :=
{ le_refl  := λ ⟨a, b⟩, ⟨le_refl a, le_refl b⟩,
  le_trans := λ ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ ⟨hac, hbd⟩ ⟨hce, hdf⟩,
    ⟨le_trans hac hce, le_trans hbd hdf⟩,
  .. prod.has_le M N }

def prod.preorder_clash [preorder M] [preorder N] : preorder (M × N) :=
{ le_refl  := λ ⟨a, b⟩, ⟨le_refl a, le_refl b⟩,
  le_trans := λ ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ ⟨hac, hbd⟩ ⟨hce, hdf⟩,
    ⟨le_trans hac hce, le_trans hbd hdf⟩,
  .. prod.has_lt,
  .. prod.has_le M N }
/-
exact tactic failed, type mismatch, given expression has type
  ?m_1 ↔ ?m_1
but is expected to have type
  a < b ↔ a ≤ b ∧ ¬b ≤ a
state:
2 goals
M : Type v,
N : Type w,
_inst_1 : preorder M,
_inst_2 : preorder N,
a b : M × N
⊢ a < b ↔ a ≤ b ∧ ¬b ≤ a

M : Type v,
N : Type w,
_inst_1 : preorder M,
_inst_2 : preorder N,
a b : M × N
⊢ Prop
-/

[Yakov Pechersky]

I don't think this is provably true...

instance prod.preorder' [preorder M] [preorder N] : preorder (M × N) :=
{ le_refl  := λ ⟨a, b⟩, ⟨le_refl a, le_refl b⟩,
  le_trans := λ ⟨a, b⟩ ⟨c, d⟩ ⟨e, f⟩ ⟨hac, hbd⟩ ⟨hce, hdf⟩,
    ⟨le_trans hac hce, le_trans hbd hdf⟩,
  lt_iff_le_not_le := λ ⟨a, b⟩ ⟨c, d⟩, begin
    split,
    { rintro (h|h),
      { exact ⟨⟨h.le, sorry⟩, λ H, h.not_le H.left⟩ },
      { exact ⟨⟨h.left.le, h.right.le⟩, λ H, h.right.not_le H.right⟩ } },
    { rintro ⟨⟨hac, hbd⟩, h'⟩,
      sorry },
  end,
  .. prod.has_lt,
  .. prod.has_le M N }

[Yakov Pechersky]

Makes an appearance in #8930