Zulip Chat Archive

Stream: new members

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


view this post on Zulip Nam (Apr 11 2020 at 18:18):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:18):

exact id or intro H, exact H

view this post on Zulip Nam (Apr 11 2020 at 18:19):

nothing similar to refl?

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:19):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:20):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:20):

afterall -> is a partial order

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:21):

a total order if you believe in classical logic

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:21):

but I don't think Mario will like the instance

view this post on Zulip Nam (Apr 11 2020 at 18:21):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:22):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:22):

maybe -> is special

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:22):

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

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:22):

because sometimes you want extra hypotheses or something

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:22):

which will be ->

view this post on Zulip 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 ;-)

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:22):

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

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:23):

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

view this post on Zulip 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'

view this post on Zulip Kenny Lau (Apr 11 2020 at 18:24):

:P

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:24):

I'm not impressed

view this post on Zulip Kevin Buzzard (Apr 11 2020 at 18:25):

that's not actually refl

view this post on Zulip Scott Morrison (Apr 11 2020 at 23:03):

Does library_search find it?

view this post on Zulip Scott Morrison (Apr 11 2020 at 23:04):

Apparently not...

view this post on Zulip 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