Zulip Chat Archive

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)
             (@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 (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]
  [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 (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