refl for a = b -> a = b?

Stream: new members

[Nam]

hello, how do i discharge a = b -> a = b?

[Kenny Lau]

exact id or intro H, exact H

[Nam]

nothing similar to refl?

[Kevin Buzzard]

refl says x = x. You want x -> x

[Kenny Lau]

I mean, refl should work... (if we have the right instance)

[Kenny Lau]

afterall -> is a partial order

[Kenny Lau]

a total order if you believe in classical logic

[Kenny Lau]

but I don't think Mario will like the instance

[Nam]

i tried refl. that didn't work. simp worked.

[Kenny Lau]

@[refl] theorem testing {p : Prop} : p → p := id

invalid reflexivity rule, result type must be an operator application

[Kenny Lau]

so I can't tag it with refl, but I don't understand why

[Kenny Lau]

maybe -> is special

[Kevin Buzzard]

That's interesting! I was thinking along the same lines as you.

[Kenny Lau]

because sometimes you want extra hypotheses or something

[Kenny Lau]

which will be ->

[Kevin Buzzard]

But I'm still hung up in proving A x B = A x B in the other thread ;-)

[Kenny Lau]

so you don't want -> to ever have other properties

[Kevin Buzzard]

I guess -> isn't a binary relation. But it should be on Prop, right?

[Kenny Lau]

meta def refl' : tactic unit :=
`[exact id]

theorem test {a b : nat} : a = b → a = b :=
by refl'

[Kenny Lau]

:P

[Kevin Buzzard]

I'm not impressed

[Kevin Buzzard]

that's not actually refl

[Scott Morrison]

Does library_search find it?

[Scott Morrison]

Apparently not...

[Chris B]

Thanks Zulip for making this thread look recent.

The CS people call this id.