Help proving tautology

Stream: new members

[Mikaël Mayer]

I don't know how to prove this:

theorem beq_refl (T: Type) [BEq T] (x : T) : (x == x) = true := by
  simp

In general, as a new lean user, what do you use to find which tactics can apply on a given proof goal?

[Robin Arnez]

It's false, you need the ReflBEq assumption. Take for example Float where nan != nan

[Robin Arnez]

theorem beq_refl (T : Type u) [BEq T] [ReflBEq T] (x : T) : (x == x) = true :=
  BEq.refl x

[Mikaël Mayer]

Oh, so == is just a syntactic sugar for a non-interpreted operation?

[Mikaël Mayer]

Thank you very much for the insight !

[Robin Arnez]

Well, it's notation for the operation that's provided through [BEq T] and you can use anything for that

[Robin Arnez]

In constrast, x = x is actually mathematical equality

[Kenny Lau]

Mikaël Mayer said:

as a new lean user

could I ask for more context?

[Kenny Lau]

i'm asking because the code you typed doesn't look like a code i would type, so i'm wondering if you're interested in a different part of the library

[Robin Arnez]

Mikaël Mayer schrieb:

In general, as a new lean user, what do you use to find which tactics can apply on a given proof goal?

You can try try? or exact? or apply? or rw?

[Alfredo Moreira-Rosa]

also hint to find tactics (will suggest simp, aesop, ring, etc)

[Robin Arnez]

Yeah, hint is planned to be replaced by try?

[Alfredo Moreira-Rosa]

Robin Arnez said:

Yeah, hint is planned to be replaced by try?

but at the moment they give completely different results. sometimes try? don't find anything while hint does and vice versa. So some kind of unification is needed first ?

[Robin Arnez]

Yeah I suppose that will happen eventually

[Mikaël Mayer]

as a new lean user

could I ask for more context?
i'm asking because the code you typed doesn't look like a code i would type, so i'm wondering if you're interested in a different part of the library

It was a small reproduction of something I did not know how to prove. I'm working in the Strata open-source project.

You can try try? or exact? or apply? or rw?

Thank that was definitely useful advice ! For me "hint" returns "unknown tactic"

[Alfredo Moreira-Rosa]

to have hint available, you need to import Mathlib.Tactic i think