Zulip Chat Archive

Stream: general

Topic: trouble with function as set


view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:12):

Hi! Is this a proper channel for asking (elementary) questions?

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:12):

I'm stuck trying to prove the following trivial statement:

def func_as_set {α β} (f : α  β) : set (α × β) := { x | x.2 = f(x.1) }

example {α β} (a : α) (f : α  β) : (a, f a)  func_as_set f := sorry

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:13):

Refl and Simp tactics don't seem to work, unfortunately

view this post on Zulip Chris Hughes (Dec 01 2018 at 23:17):

Did you try rfl?

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:18):

I don't think so. I will do it now.

view this post on Zulip Chris Hughes (Dec 01 2018 at 23:18):

refl works for any reflexive relation, and I guess the elaborator looks for a proof that is reflexive. rfl is only for equality.

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:19):

omg that worked. Thanks for the elaboration too. Very useful to know!!

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:31):

PS

Hi! Is this a proper channel for asking (elementary) questions?

Here is fine, although most of the elementary questions get asked in #new members . There are no hard and fast rules though.

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:36):

Cool, thanks

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:38):

In that case, I have another trivial follow up ;-) How does one go from a hypothesis in this form

x { y | P y }

to

P x

?

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:39):

Again isn't that rfl?

view this post on Zulip Chris Hughes (Dec 01 2018 at 23:40):

rw set.mem_set_of_eq also works. That lemma does not have a good name.

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:40):

but you can't use that when it's a hypothesis, right?

view this post on Zulip Chris Hughes (Dec 01 2018 at 23:40):

rw _ at h

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:40):

right - trying now

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:40):

Are you in tactic mode or term mode?

view this post on Zulip Chris Hughes (Dec 01 2018 at 23:40):

if h is your hypothesis.

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:41):

tactic mode

view this post on Zulip Kenny Lau (Dec 01 2018 at 23:41):

you can just change it

view this post on Zulip Kenny Lau (Dec 01 2018 at 23:41):

or pretend that it's already in that form

view this post on Zulip Kenny Lau (Dec 01 2018 at 23:41):

depending on what you're trying to do

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:41):

You could do change P x at h as well

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:41):

oooh, that's useful
thanks folks!

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:41):

Because the two terms are definitionally equal you might not even need to change it

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:46):

@Kevin Buzzard my proposition is an equality in this case. i need it for a rewrite. doesnt seem to work without an explicit change

view this post on Zulip Marcus Klaas (Dec 01 2018 at 23:46):

with the change, it does! :-)

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:47):

Post some working code?

view this post on Zulip Kevin Buzzard (Dec 01 2018 at 23:47):

But yes, rw needs things to be unravelled explicitly.


Last updated: May 14 2021 at 14:20 UTC