Switching from Rel to Relation

Stream: computer science

[Fabrizio Montesi]

@Chris Henson @Thomas Waring I've made a PR that removes our dependency from Rel. Let me know what you think. :)

https://github.com/cs-lean/cslib/pull/16

[Fabrizio Montesi]

(whoops, was missing a bunch of files, now fixed)

[Thomas Waring]

Looks good! I notice you've copied across my trans_of_subrelation etc results, which weren't compiling as instances, I believe because of "out param" issues that I didn't / don't understand — if you can probably cut them out, I don't think they are used anywhere

[Fabrizio Montesi]

Thomas Waring said:

Looks good! I notice you've copied across my trans_of_subrelation etc results, which weren't compiling as instances, I believe because of "out param" issues that I didn't / don't understand — if you can probably cut them out, I don't think they are used anywhere

Sometimes I encountered that problem and fixed it by writing the implicit parameters and giving them explicit universes (Type u, Type v, etc.).

[Chris Henson]

@Fabrizio Montesi I see you have merged already, did you see the few comments I had left? Nothing major, seems fine in general.

[Fabrizio Montesi]

No, I wasn't notified by GitHub, weird.. where do I find them?

[Chris Henson]

Oh my bad. Apparently I had to click the "submit review" button for them to be shared, I didn't realize... you should be able to see them now on the PR

[Fabrizio Montesi]

All done, thanks.
Re notation for Relation.inv and Relation.Comp: I searched for it and couldn't find it. The mathlib docs suggests there's a notation for Relation.Comp but it doesn't seem to work?
For Relation.inv, the natural notation would be a -1 superscript, but that's already used for something else (Inv). :\

[Chris Henson]

For composition, maybe that docstring is wrong? I see only a local infixr:80 " ∘r " => Relation.Comp and that's been unchanged since the Lean 3 port according to git blame.

[Fabrizio Montesi]

Update: @Eric Wieser pointed out that we can use \sup for union of relations (#Is there code for X? > Union of relations ). We can also use \inf for intersection. They work as expected. I've just applied this.