Zulip Chat Archive

Stream: new members

Topic: symmetric function


view this post on Zulip Vaibhav Karve (Mar 22 2020 at 15:11):

I have the following setup:

example : (A B : Sort) (rel : A -> A -> B) : Prop := forall a b : A, f a b = f b a

In the special case of B being Prop, I know that I can restate the above as symmetric f. Is there a corresponding general version of symmetric that will work for any B?

I also discovered that for some reason, library search doesn't work:

example : (A : Sort) : (A -> A -> Prop) -> Prop := by suggest  -- doesn't work
example : (A : Sort) : (A -> A -> Prop) -> Prop := by library_search  -- doesn't work

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:14):

That looks like commutative

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:15):

but that might also be special cased to B = A

view this post on Zulip Mario Carneiro (Mar 22 2020 at 15:17):

I think that whole section of core is due for an update

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 15:30):

Yes, commutative is close but not quite right. I definitely want B ≠ A. Any idea why the suggest doesn't work?

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 16:00):

What is Sort by the way? Isn't it defeq to Prop or something?

view this post on Zulip Mario Carneiro (Mar 22 2020 at 16:17):

it is Prop

view this post on Zulip Mario Carneiro (Mar 22 2020 at 16:17):

#check Sort -- Prop : Type

view this post on Zulip Mario Carneiro (Mar 22 2020 at 16:18):

Technically Prop is a notation for Sort:

notation `Prop` := Sort 0

view this post on Zulip Kevin Buzzard (Mar 22 2020 at 16:37):

@Vaibhav Karve are you aware of this? You say "in the special case of B being Prop" but Prop is not allowed as a value for B in what you say, strictly speaking.

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 18:46):

Yes, Kevin, I was aware of this. In my attempt to write a MWE, I went too far. I was actually looking for a simple analogue of symmetric that would work for Sort u, not just Sort.

view this post on Zulip Mario Carneiro (Mar 22 2020 at 18:54):

You can just write Sort* if you don't want to declare the universe - or even nothing at all, that is:

example (A B) (rel : A -> A -> B) : Prop := forall a b : A, f a b = f b a

This is my favorite way to write theorems. It's compact, maximally general and there is nothing to mess up

view this post on Zulip Vaibhav Karve (Mar 22 2020 at 19:14):

Thanks for teaching me this new trick. I did not know that omitting the type is the same as writing Sort* (provided there aren't other type-inferences, ofcourse).


Last updated: May 11 2021 at 22:14 UTC