## Stream: new members

### Topic: refl for a = b -> a = b?

#### Nam (Apr 11 2020 at 18:18):

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

#### Kenny Lau (Apr 11 2020 at 18:18):

exact id or intro H, exact H

#### Nam (Apr 11 2020 at 18:19):

nothing similar to refl?

#### Kevin Buzzard (Apr 11 2020 at 18:19):

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

#### Kenny Lau (Apr 11 2020 at 18:20):

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

#### Kenny Lau (Apr 11 2020 at 18:20):

afterall -> is a partial order

#### Kenny Lau (Apr 11 2020 at 18:21):

a total order if you believe in classical logic

#### Kenny Lau (Apr 11 2020 at 18:21):

but I don't think Mario will like the instance

#### Nam (Apr 11 2020 at 18:21):

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

#### Kenny Lau (Apr 11 2020 at 18:22):

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

invalid reflexivity rule, result type must be an operator application


#### Kenny Lau (Apr 11 2020 at 18:22):

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

#### Kenny Lau (Apr 11 2020 at 18:22):

maybe -> is special

#### Kevin Buzzard (Apr 11 2020 at 18:22):

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

#### Kenny Lau (Apr 11 2020 at 18:22):

because sometimes you want extra hypotheses or something

#### Kenny Lau (Apr 11 2020 at 18:22):

which will be ->

#### Kevin Buzzard (Apr 11 2020 at 18:22):

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

#### Kenny Lau (Apr 11 2020 at 18:22):

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

#### Kevin Buzzard (Apr 11 2020 at 18:23):

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

#### Kenny Lau (Apr 11 2020 at 18:24):

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

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


:P

#### Kevin Buzzard (Apr 11 2020 at 18:24):

I'm not impressed

#### Kevin Buzzard (Apr 11 2020 at 18:25):

that's not actually refl

#### Scott Morrison (Apr 11 2020 at 23:03):

Does library_search find it?

#### Scott Morrison (Apr 11 2020 at 23:04):

Apparently not...

#### Chris B (Nov 11 2020 at 05:04):

Thanks Zulip for making this thread look recent.

The CS people call this id`.

Last updated: May 06 2021 at 22:13 UTC