Zulip Chat Archive

Stream: new members

Topic: Creating definitions in Lean


view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 10:47):

I am trying to define an equivalence class in Lean, where I already have a binary relation, defined as a variable variable (r : S → S → Prop) -- how would I insert the requirement of binary_relation satisfying equivalence while defining an equivalence class?

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 10:48):

I.e. surely just def class (a : S) : set S := { x | r x a } is not enough. Do I need some squiggly brackets here to impose the requirement equivalence binary_relation?

view this post on Zulip Kenny Lau (Oct 14 2018 at 10:52):

the philosophy is that we create the definition as general as possible, and only insert the hypothesis in the proofs

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 10:54):

Perhaps, but I just want to learn how definitions work. Can we make them specific in this way?

view this post on Zulip Kenny Lau (Oct 14 2018 at 10:55):

def equivalence_class (h : is_equivalence r) (a : S) : set S := { x | r x a }

view this post on Zulip Abhimanyu Pallavi Sudhir (Oct 14 2018 at 10:58):

Right, and then when using the definition we'd need to provide a proof of is_equivalence r as a parameter, right?

view this post on Zulip Kenny Lau (Oct 14 2018 at 10:59):

yes

view this post on Zulip Bryan Gin-ge Chen (Oct 14 2018 at 11:04):

Note that if you use that definition, the variable r becomes something lean can very easily infer. Thus it's convenient to make it implicit (by writing variable {r} immediately beforehand), so that when you use equivalence_class, you won't need to write equivalence_class r h a but only equivalence_class h a.

view this post on Zulip Kevin Buzzard (Oct 14 2018 at 13:25):

@Abhimanyu Pallavi Sudhir just to note that class is already a keyword in Lean so you might want to stick to Kenny's suggestion of equivalence_class in any experiments you try.


Last updated: May 10 2021 at 00:31 UTC