Type mismatch creating instance of One α and using `1`

Stream: new members

[Shanghe Chen]

Hi I am continuing the topic Failed to write a*b on Group₁ but now with a smaller example for failed using the notations:

class One1 (α : Type u) where
  a : α

instance onehh {α : Type u} [One1 α] : One α := ⟨One1.a⟩

theorem one_1 [One1 α] : a = 1 := rfl

[Shanghe Chen]

But it gives an error:

error : type mismathced:
  rfl
has type
  a = a : Prop
but is expected to have type
  a = 1 : Prop
Group.{u} (G : Type u) : Type u

[Kevin Buzzard]

Have you got autoImplicit on and you're a beginner? This is a big footgun for beginners. I conjecture that that a is an autoImplicit.

[Shanghe Chen]

Yeah Kevin I just begin learning Lean. The same code on live lean lang: https://live.lean-lang.org/#code=import%20Mathlib.Tactic%0D%0Anamespace%20Ex4%0D%0Aclass%20One1%20(%CE%B1%20%3A%20Type%20u)%20where%0D%0A%20%20a%20%3A%20%CE%B1%0D%0A%0D%0Ainstance%20onehh%20%7B%CE%B1%20%3A%20Type%20u%7D%20%5BOne1%20%CE%B1%5D%20%3A%20One%20%CE%B1%20%3A%3D%20%E2%9F%A8One1.a%E2%9F%A9%0D%0A%0D%0Atheorem%20one_1%20%5BOne1%20%CE%B1%5D%20%3A%20a%20%3D%201%20%3A%3D%20rfl%0D%0A--%20rfl%20failed%3A%0D%0A--%20type%20mismatch%0D%0A--%20%20%20rfl%0D%0A--%20has%20type%0D%0A--%20%20%20one%20%3D%20one%20%3A%20Prop%0D%0A--%20but%20is%20expected%20to%20have%20type%0D%0A--%20%20%20one%20%3D%201%20%3A%20Prop%0D%0A%0D%0A--%20%23check%20one1%0D%0A--%20--%20result%3A%0D%0A--%20--%20Ex4.one1.%7Bu%7D%20%7B%CE%B1%20%3A%20Type%20u%7D%20%5Binst%E2%9C%9D%20%3A%20One1%20%CE%B1%5D%20%3A%20One%20%CE%B1%0D%0A%0D%0Avariable%20%5BOne1%20%CE%B1%5D%0D%0A%23check%20(1%3A%CE%B1)%0D%0A--%20%23check%20(inferInstance%20%3A%20One1%20%CE%B1).a%0D%0A--%20%23check%20one1.one%0D%0A%0D%0A%0D%0Aend%20Ex4%0D%0A%0D%0A

[Shanghe Chen]

Oh I did not turn any option about autoImplicit. Let me check how to turn it on.

[Kevin Buzzard]

Yeah I think that has autoImplicit on?

[Shanghe Chen]

image.png

[Kevin Buzzard]

I'm suggesting that you turn it and relaxedAutoImplicit off and then you'll see your error

[Shanghe Chen]

Yeah now I get the maybe right error:
image.png

[Shanghe Chen]

Still some werid error. Maybe I should read MIL chapter7 first where there are more content on the notations. I am still in MIL chapter 6:tada:

[Shanghe Chen]

Ah with the option

set_option relaxedAutoImplicit false
set_option autoImplicit false

Now I get it (at lest for the current topic): the a in the theorem is not the same a as in line 8 inside the class. It's in fact an argument created implicitly. Hence they are not the same.

[Shanghe Chen]

@Kevin Buzzard Thank you very much for for supplying the information of these options. :tada:

[Kevin Buzzard]

No worries!