weird clear behaviour?

Stream: new members

[Damiano Testa]

Dear All,

I do not normally use clear, but decided to try it. Should I be surprised by the beviour in the following example?

Thanks!

import algebra.order.monoid

variables {α : Type} [h : ordered_cancel_add_comm_monoid α] (n : ℕ)

--  works
example : n ≤ n :=
begin
  exact le_rfl,
end

include h

--  fails
example : n ≤ n :=
begin
  clear h,
  exact le_rfl,
end
/-
invalid type ascription, term has type
  ?m_3 ≤ ?m_3
but is expected to have type
  n ≤ n
state:
α : Type,
n : ℕ
⊢ n ≤ n
-/

[Eric Rodriguez]

not particularly; what it's complaining about is that le_rfl doesn't have a preorder instance

[Yaël Dillies]

How does it even let you clear h?

[Damiano Testa]

But don't naturals have it, like the earlier example shows?

[Damiano Testa]

Yaël, I included it

[Eric Rodriguez]

oh, I see that stuff is a bit different than expected!

[Eric Rodriguez]

a : N!

[Eric Rodriguez]

resetI after the clear works, but why that is necessary boggles the mind...

[Damiano Testa]

Right, the statement is the same, I only artificially included h (and \a), remove the artificial h and the same left-over proof fails.

[Eric Rodriguez]

maybe Lean detects that the instance cache has changed and so decides to shut down

[Damiano Testa]

Does this suggest that clear should do resetI after it is currently done?

[Eric Rodriguez]

that would be slow, but I feel like clearing a frozen instance should maybe not be possible

[Eric Rodriguez]

@Yaël Dillies what happened to your instance colour thing?

[Yaël Dillies]

It's still over at #15959

[Damiano Testa]

The same happens if you clear_except (and of course, a stays, but \a h disappear).

[Yaël Dillies]

Just something to fix in the HTML and that should be good to go?

[Eric Rodriguez]

so the instance that it usually grabs is nat.ordered_semiring and then precipitates that down to a preorder

[Eric Rodriguez]

for some reason, typeclass doesn't even bother checking that instance after the clear

[Damiano Testa]

Small disclosure: I found out about this after a clear_except .... I think that if you on purpose clear a typeclass assumption, then you should be ready for some weirdness. But I did not like that doing a clear_except ... removed instances for me and then made my goals harder to prove!

[Damiano Testa]

I reduced a little the imports in the example above and also changed the name of the nat to n.

It turns out that the instance that you clear should contain some order relation for the error to arise, but not any relation. [h : has_le α] can be cleared, but [h : preorder α] cannot.