Zulip Chat Archive

Stream: maths

Topic: Explicit hypothesis vs implication hypothesis convention


view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 03:18):

Is there a convention for when to put the hypothesis to the left of the colon rather than in an implication?
For instance,

example (n : ) (h : n > 1) : n > 0 := by linarith

rather than

example (n : ) : (n > 1)  (n > 0) := λ h, (by linarith)

view this post on Zulip Bryan Gin-ge Chen (Dec 29 2020 at 05:41):

Between your two examples, I think we generally prefer the former, since it removes the need for the lambda after the :=. So I generally put as many hypotheses to the left of the colon as possible. Sometimes you have to leave some implications or foralls to the right of the colon, especially when using the equation compiler or if the proof uses tactic#induction.

view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 07:39):

Bryan Gin-ge Chen said:

Between your two examples, I think we generally prefer the former, since it removes the need for the lambda after the :=. So I generally put as many hypotheses to the left of the colon as possible. Sometimes you have to leave some implications or foralls to the right of the colon, especially when using the equation compiler or if the proof uses tactic#induction.

Would the former be preferred even if the proof didn't contain a lambda, but rather a begin-end block?

view this post on Zulip Johan Commelin (Dec 29 2020 at 07:52):

if the begin .. end-block starts with intros you might as well put those assumptions left of the colon.

view this post on Zulip Johan Commelin (Dec 29 2020 at 07:53):

It's mostly just about which version uses the least amount of characters to type...

view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 07:55):

So generally speaking, it is better to put hypotheses to the left of the colon as much as possible.

view this post on Zulip Kenny Lau (Dec 29 2020 at 07:58):

Yes.

view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 08:03):

I see. I can make a pull request to add this convention to Style Guidelines https://leanprover-community.github.io/contribute/style.html, since it seems useful.

view this post on Zulip Kenny Lau (Dec 29 2020 at 08:04):

Go ahead.

view this post on Zulip Mohamed Al-Fahim (Dec 29 2020 at 08:35):

https://github.com/leanprover-community/leanprover-community.github.io/pull/154


Last updated: May 10 2021 at 08:14 UTC