## Stream: new members

### Topic: diamond on order of prod

#### Yakov Pechersky (Aug 31 2021 at 01:43):

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)
(@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
(@preorder.to_has_lt.{w} N
(@prod.mk.{v w} M N a c)
(@prod.mk.{v w} M N b d) :=
begin
sorry,
end


#### Yakov Pechersky (Aug 31 2021 at 01:43):

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]
[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 (Aug 31 2021 at 01:52):

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 (Aug 31 2021 at 02:00):

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 (Aug 31 2021 at 05:27):

Makes an appearance in #8930

Last updated: Dec 20 2023 at 11:08 UTC