Zulip Chat Archive

Stream: new members

Topic: 'Prop' in definitions


Holly Liu (Jul 21 2021 at 22:10):

why do set and equivalence relations map to a Prop in their definitions: def set (α : Type u) := α → Prop and constant quot : Π {α : Sort u}, (α → α → Prop) → Sort u where r : (α → α → Prop)?

Kevin Buzzard (Jul 21 2021 at 22:12):

What is your definition of an equivalence relation, if it doesn't involve true-false statements?

Kevin Buzzard (Jul 21 2021 at 22:13):

The answer to the set question is that lean identifies a subset S of X with the function that sends an element x of X to the true-false statement xSx\in S

Kevin Buzzard (Jul 21 2021 at 22:16):

Although it's probably worth remarking that using this fact is breaking the abstraction barrier

Holly Liu (Jul 21 2021 at 22:23):

Kevin Buzzard said:

breaking the abstraction barrier

is that like what the end-user is not supposed to see?

Holly Liu (Jul 21 2021 at 22:26):

Kevin Buzzard said:

What is your definition of an equivalence relation, if it doesn't involve true-false statements?

i think the (α → α → Prop) is a bit confusing. i'm not sure what the first two α's are for

Kevin Buzzard (Jul 21 2021 at 22:46):

I'm asking you what your definition of an equivalence relation on alpha is. It should be exactly the same, or obviously equivalent, to Lean's, but you're not saying what you think it is so it's difficult to make progress

Adam Topaz (Jul 21 2021 at 22:51):

If you identify set A with A -> Prop, then A -> A -> Prop (which really means A -> (A -> Prop) becomes A -> (set A), i.e. a function which associates to any element of A a subset of A. One way to think about this is by saying that this function sends a : A to the "set of all elements which are related to a"

Adam Topaz (Jul 21 2021 at 22:54):

There are other ways to grok this, but as Kevin said, it would be helpful to know how you usually define a relation

Nicholas (Jul 21 2021 at 23:22):

doesnt the equivalence relation rr take two α\alpha as arguments and return whether or not they are equivalent (which is a proposition)?

Holly Liu (Jul 22 2021 at 19:16):

Kevin Buzzard said:

I'm asking you what your definition of an equivalence relation on alpha is. It should be exactly the same, or obviously equivalent, to Lean's, but you're not saying what you think it is so it's difficult to make progress

sorry, my definition was that an equivalence relation on alpha is something that satisfies three properties, which are reflexivity, symmetry, and transitivity. i meant to say that i didn't understand why it was defined without these properties, but i see that it can be thought of as mapping each element of a set to "a set of all elements which are related to the element", and that it's checking for equivalence between two arguments.

Kevin Buzzard (Jul 22 2021 at 19:17):

Yes, that's correct: but your question was about the "something", not about the axioms. The thing you quoted above is not an equivalence relation, it's just a binary relation.

Eric Wieser (Jul 22 2021 at 19:17):

The other piece of the puzzle is that quot effectively takes the closure of the relation you pass it using docs#eqv_gen

Holly Liu (Jul 22 2021 at 19:19):

i didn't realize it was just a binary relation. i may have confused binary relation with equivalence relations

Eric Wieser (Jul 22 2021 at 19:20):

docs#quotient is the version that takes an equivalence relation to begin with

Holly Liu (Jul 22 2021 at 19:26):

oh, equivalence relations are setoids?

Eric Wieser (Jul 22 2021 at 19:28):

Well, strictly an equivalence relation is any relation that satisfies docs#equivalence

Holly Liu (Jul 22 2021 at 19:29):

ah ok

Esteban Estupinan (Oct 21 2021 at 17:11):

hi all, I m I am examining in more detail the creation of definitions in lean and I have seen small differences in the type here some examples

def upper_bounds (S : set ) : set  := { b | s  S, s  b }
def lower_bounds (S : set ) : set  := { b | s  S, b  s }
def is_least (S : set ) (l : ) : Prop := l  S  l  lower_bounds S
def is_lub (S : set ) (l : ) : Prop := is_least (upper_bounds S) l

def S (x y : A) := R x y  R y x

I ask you, when we should use the Prop type, when we should not use any type, how does each one vary, thank you very much for your time

Kyle Miller (Oct 21 2021 at 17:13):

When you leave off the type, Lean will infer it if it can (if it can't it will show an error). This should be exactly the same:

def S (x y : A) : Prop := R x y  R y x

Try doing

#check S

to see what type Lean has inferred.

Kyle Miller (Oct 21 2021 at 17:19):

(I personally think it's nicer to include the : Prop, but you don't have to.)


Last updated: Dec 20 2023 at 11:08 UTC