symmetric function

Stream: new members

[Vaibhav Karve]

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

[Mario Carneiro]

That looks like commutative

[Mario Carneiro]

but that might also be special cased to B = A

[Mario Carneiro]

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

[Vaibhav Karve]

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

[Kevin Buzzard]

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

[Mario Carneiro]

it is Prop

[Mario Carneiro]

#check Sort -- Prop : Type

[Mario Carneiro]

Technically Prop is a notation for Sort:

notation `Prop` := Sort 0

[Kevin Buzzard]

@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.

[Vaibhav Karve]

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.

[Mario Carneiro]

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

[Vaibhav Karve]

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).