Proof fails when instances are specified

Stream: new members

[Fingy Soupy]

Hello, I have a proof that only seems to work if the instances are not specified. E.g.:

-- This works
lemma le_sup_left  (a b : tv) : a <= a ⊔ b := begin
rw le_sup_iff,
simp,
end
-- So why shouldn't this?
lemma le_sup_left_2 [lo : linear_order tv] [sup : has_sup tv] (a b : tv) : a <= a ⊔ b := begin
rw le_sup_iff,
simp,
end

The message I get in the second lemma is

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_3 ≤ _
state:
lo : linear_order tv,
sup : has_sup tv,
a b : tv
⊢ a ≤ a ⊔ b

Which just looking at the pattern alone, that should match?

I'm very confused and I'm not sure what the upper proof is using if not linear_order tv and has_sup tv.
I've tried to trim down my code as much as possible
https://gist.github.com/sjkillen/0dadd10c867de3e0488a51461ac25e4b

[Yaël Dillies]

This is because [linear_order tv] [has_sup tv] is nonsense.

[Yaël Dillies]

A linear_order already has a sup, namely max (docs#sup_eq_max). So [linear_order tv] [has_sup tv] means "Assume tv is a linear order AND there is a totally unrelated ⊔ on it as well". Lean then picks one of the two possible ⊔ randomly and you eat your hat.

[Yaël Dillies]

Also, you haven't given me a #mwe, so maybe [linear_order tv] is nonsense on its own. Is tv a concrete type that you defined or a variable that you declared with something like variables {tv : Type*}?

[Kyle Miller]

Yaël Dillies said:

This is because [linear_order tv] [has_sup tv] is nonsense.

Seems incorrect to call it nonsense -- it means something very precise, just very much not what you'd want.

[Yaël Dillies]

Nonsense can be precise! And nobody ever declares two competing instances in square brackets. Eckmann-Hilton does declare two competing instances, but not this way.

[Reid Barton]

The first one works because of the way you have defined the linear_order and has_sup instances on tv. In the second one you consider arbitrary variable instances linear_order tv and has_sup tv, which may be unrelated.

[Fingy Soupy]

Ah thank you! I didn't actually realize that a type could have multiple instances defined on it

[Fingy Soupy]

How do I access the has_sup instance for linear_order tv?
I was to define

instance [lo : linear_order tv] : semilattice_sup tv := {
le_sup_left := le_sup_left,
le_sup_right := le_sup_right,
sup_le := sup_le,
-- sup := sorry,
..lo  }