Order diamond

Stream: general

[Yaël Dillies]

I don't know what to do to solve this.

import order.bounds

lemma monotone_fst' {α β : Type*} [preorder α] [preorder β] : monotone (@prod.fst α β) := sorry

lemma monotone_snd' {α β : Type*} [preorder α] [preorder β] : monotone (@prod.snd α β) := sorry

lemma mem_upper_bounds_image {α β : Type*} [preorder α] [preorder β] {f : α → β} (Hf : monotone f)
  {a : α} {s : set α} (Ha : a ∈ upper_bounds s) :
  f a ∈ upper_bounds (f '' s) := sorry

example {α β : Type*} [preorder α] [preorder β] {f : α → β} (Hf : monotone f) : true :=
begin
  have := @mem_upper_bounds_image _ _ (@prod.preorder α β _ _) _ _ monotone_fst', -- works
  have := @mem_upper_bounds_image _ _ _ _ _ monotone_fst', --fails
  have := mem_upper_bounds_image monotone_fst', --fails
end

[Yaël Dillies]

The problem seems to stem from (Hf : monotone f) taking in @preorder.to_has_le α and preorder.to_has_le β and not just any has_le.

[Yaël Dillies]

Note this is all already in mathlib, and somehow I've broken it in the past 6 commits I made to #7987 :sad:

[Reid Barton]

What do you mean by "works" and "fails"?
Surely, the last two can't infer α or β.

[Yaël Dillies]

Yeah but they should be left as metavariables. If you provide them using other arguments, that still doesn't work

[Reid Barton]

Well in the Lean playground, they all "work" then.

[Yaël Dillies]

Hmm...

[Yaël Dillies]

Well a non minimal really non working example is the branch locally_finite in order.bounds, if somebody could have a look.

[Yakov Pechersky]

prod orders are broken, lt and le don't agree.

[Yury G. Kudryashov]

@Yakov Pechersky Could you please point me to the pair of instances that create a diamond?

[Yakov Pechersky]

src#prod.has_lt, src#prod.has_le

[Yury G. Kudryashov]

What's wrong with these two instances? We never require lt_iff_le_not_le to be a definitional equality.

[Yury G. Kudryashov]

Probably some other instance up in the chain uses the default (<) instead of lt := (<).

[Yury G. Kudryashov]

Indeed, docs#prod.preorder is bad.

[Yakov Pechersky]

Specifically in src#prod.ordered_smul, I couldn't generalize it properly.

[Yury G. Kudryashov]

I'll try to fix it now.

[Yakov Pechersky]

Yes, what I meant is that. I just sent the actually conflicting definitions.

[Yury G. Kudryashov]

I'll fix prod.preorder, then the diamond should disappear.

[Yury G. Kudryashov]

OMG, prod.has_lt is not equivalent to le_and_not_le for a preorder.

[Yury G. Kudryashov]

We'll need to fix it in the core.

[Yury G. Kudryashov]

(or move prod.has_lt to mathlib)

[Mario Carneiro]

I don't think prod.has_lt should be an instance at all

[Mario Carneiro]

there should be a type alias for the total order

[Mario Carneiro]

or use prod.lex instead of <

[Yury G. Kudryashov]

I'm going to delete the old instance from core.

[Yury G. Kudryashov]

lean#620

[Yury G. Kudryashov]

We already have a type alias docs#lex for the lexicographical order.

[Yakov Pechersky]

Right, this is the issue I hit earlier. You're taking on the core change that I avoided :-) thank you

[Yury G. Kudryashov]

BTW, do we use the right definition for lex.has_le in case of a preorder? It looks like the map λ x, (x, a) is not monotone with our definition.

[Yury G. Kudryashov]

Because we don't have eq_or_lt_of_le.

[Yury G. Kudryashov]

I think that we should use (a, b) ≤ (c, d) ↔ a ≤ c ∧ (c ≤ a → b ≤ d) (or don't claim to support preorders).

[Yury G. Kudryashov]

@Scott Morrison @Minchao Wu According to the header, you're the authors of order.lexicographic.

[Scott Morrison]

We'll need another statement that still says (a, b) ≤ (c, d) ↔ a < c \or (a = c ∧ b ≤ d) with [partial_order].

[Yury G. Kudryashov]

Yes, sure. We need a partial order on α and a preorder on β for this statement.

[Yury G. Kudryashov]

There should be an iff with lex as well if we want to reuse the fact that it's well-founded.

[Yaël Dillies]

Oh duh, I didn't notice prod.has_lt existed.

[Eric Wieser]

(docs#prod.has_lt)

[Yaël Dillies]

Thansk for correcting this! What's puzzling me is that all this was working before and I somehow broke it. Maybe it was just fragile.

[Yakov Pechersky]

As you can see with src#prod.ordered_smul, if you're at a complex enough structure, then it takes only one "canonical" path through the TCs. But generalizing, it has more options to branch. That's probably what's going on in your generalization branch.

[Yaël Dillies]

Okay, I've made an actual MWE. This is the most minimizing I've ever done.

import tactic.interactive_expr

instance (α β : Type*) [has_le α] [has_le β] : has_le (α × β) :=
⟨λ p q, p.1 ≤ q.1 ∧ p.2 ≤ q.2⟩

instance (α β : Type*) [preorder α] [preorder β] : preorder (α × β) :=
{ le_refl  := sorry,
  le_trans := sorry,
  .. prod.has_le α β }

variables {α β : Type*}

def monotone [has_le α] [has_le β] (f : α → β) : Prop := ∀ ⦃a b⦄, a ≤ b → f a ≤ f b

variables [preorder α] [preorder β]

lemma monotone_fst : monotone (@prod.fst α β) :=
sorry

infix ` '' `:80 := set.image

def upper_bounds (s : set α) : set α := {x | ∀ ⦃a⦄, a ∈ s → a ≤ x}

lemma monotone.mem_upper_bounds_image {f : α → β} (hf : monotone f) {a : α} {s : set α}
  (ha : a ∈ upper_bounds s) :
  f a ∈ upper_bounds (f '' s) :=
sorry

lemma mwe_works {s : set (α × β)} {a : α × β} (ha : a ∈ upper_bounds s) :
  a.1 ∈ upper_bounds (prod.fst '' s) :=
begin
  exact monotone.mem_upper_bounds_image monotone_fst ha, -- works
end

lemma mwe_fails {s : set (α × β)} {a : α × β} (ha : a ∈ upper_bounds s) :
  a.1 ∈ upper_bounds (prod.fst '' s) :=
begin
  exact monotone_fst.mem_upper_bounds_image ha, -- fails
end

[Yaël Dillies]

I think this is clearly(?) an elaboration issue.

[Yaël Dillies]

If I replace the definition of monotone by def monotone [preorder α] [has_le β] (f : α → β) : Prop := ∀ ⦃a b⦄, a ≤ b → f a ≤ f b, then mwe_fails works.

[Eric Wieser]

This is because dot notation has different elaboration rules I guess

[Yaël Dillies]

I guess it does :frown:
Lean fails to unify @prod.has_le α β with @preorder.to_has_le α β _

[Yaël Dillies]

In current mathlib, this works because monotone assumes [preorder α] [preorder β]. What should I do? Remove the affected dot notation? Stick to preorder in the definition? Get someone to fix that elaboration issue?

[Eric Wieser]

Does putting a type annotation on monotone_fst before the dot notation help?

[Yaël Dillies]

Indeed this works:

lemma mwe_fails {s : set (α × β)} {a : α × β} (ha : a ∈ upper_bounds s) :
  a.1 ∈ upper_bounds (prod.fst '' s) :=
(monotone_fst : monotone (@prod.fst α β)).mem_upper_bounds_image ha

[Reid Barton]

(I put α and β in the same universe to make the errors a bit shorter.)
So here's something I don't understand. In a message like

Additional information:
/test.lean:40:8: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch at application
    @monotone.mem_upper_bounds_image.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5 ?m_6 (@monotone_fst.{?l_7} ?m_8 ?m_9 ?m_10 ?m_11)
  term
    @monotone_fst.{?l_1} ?m_2 ?m_3 ?m_4 ?m_5
  has type
    @monotone.{?l_1} (prod.{?l_1 ?l_1} ?m_2 ?m_3) ?m_2
      (@prod.has_le.{?l_1 ?l_1} ?m_2 ?m_3 (@preorder.to_has_le.{?l_1} ?m_2 ?m_4) (@preorder.to_has_le.{?l_1} ?m_3 ?m_5))
      (@preorder.to_has_le.{?l_1} ?m_2 ?m_4)
      (@prod.fst.{?l_1 ?l_1} ?m_2 ?m_3)
  but is expected to have type
    @monotone.{?l_1} ?m_2 ?m_3 (@preorder.to_has_le.{?l_1} ?m_2 ?m_4) (@preorder.to_has_le.{?l_1} ?m_3 ?m_5) ?m_6

are the ?m_2 and ?m_3 that appear in the actual and expected types the same metavariables in both, or are they independent?

[Reid Barton]

Ah I guess they are numbered independently, since in the first line monotone_fst is applied to things like ?m_8 and ?m_9

[Reid Barton]

I guess the story must be something like: We need to type check monotone_fst first, in order to even find out what definition monotone_fst.mem_upper_bounds_image refers to. At this point, we have no idea how the value monotone_fst will get used so we can't infer anything about its type arguments. So if we try to do instance search now, we can't make any progress. So we end up with monotone_fst applied to a slew of metavariables. But at least we know its type is of the form monotone _.
Then, we know the dot notation is referring to monotone.mem_upper_bounds_image. But monotone.mem_upper_bounds_image monotone_fst can only type check after we do another instance search and find that we mean prod.has_le. Apparently Lean doesn't do an instance search at this point.

[Reid Barton]

I think the reason it works with preorder in monotone but not has_le is that in the latter case, there's a potentially non-defeq instance issue. Of course if you actually look at the definition of prod.preorder you'll see that to_has_le of it is the same as prod.has_le, but you have to look at the instances to see this. If you only talk about preorder everywhere then this issue doesn't come up.

[Yaël Dillies]

For reference, what I did here in the end is to require preorder everywhere and it works fine.