Stream: new members

Topic: symmetric function

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


Mario Carneiro (Mar 22 2020 at 15:14):

That looks like commutative

Mario Carneiro (Mar 22 2020 at 15:15):

but that might also be special cased to B = A

Mario Carneiro (Mar 22 2020 at 15:17):

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

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?

Kevin Buzzard (Mar 22 2020 at 16:00):

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

Mario Carneiro (Mar 22 2020 at 16:17):

it is Prop

Mario Carneiro (Mar 22 2020 at 16:17):

#check Sort -- Prop : Type


Mario Carneiro (Mar 22 2020 at 16:18):

Technically Prop is a notation for Sort:

notation Prop := Sort 0


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.

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.

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

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