Zulip Chat Archive

Stream: general

Topic: tfae formatting


view this post on Zulip Johan Commelin (Dec 27 2019 at 16:16):

tfae is being used. Kudos to @Reid Barton and @Simon Hudon for making the tactic work, and to @Yury G. Kudryashov for using it.
Here's a question/proposal about formatting: shall we format tfae statements with one "item" per line?
Pinging @Mario Carneiro and @Rob Lewis for this style issue.

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 16:18):

Do you mean something like this?

lemma tfae_mem_nhds_within_Ioi {a u' : α} (hu' : a < u') (s : set α) :
  tfae [s  nhds_within a (Ioi a), /- 0 -/
    s  nhds_within a (Ioc a u'), /- 1 -/
    s  nhds_within a (Ioo a u'), /- 2 -/
     u  Ioc a u', Ioo a u  s, /- 3 -/
     u  Ioi a, Ioo a u  s] /- 4 -/ :=

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:18):

Yes, exactly

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 16:19):

Numbers help those writing (tfae_mem_nhds_within_Ioi h s).out 0 3

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:20):

Hmmm, I now realise that tfae_have uses 1-based indexing, but tfae.out uses 0-based indexing...

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:20):

I guess that should be fixed

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 16:21):

Or even

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
  tfae [s  nhds_within a (Ioi a), /- 0 : `s` is a neighborhood of `a` within `(a, +∞)` -/
    s  nhds_within a (Ioc a b), /- 1 : `s` is a neighborhood of `a` within `(a, b]` -/
    s  nhds_within a (Ioo a b), /- 2 : `s` is a neighborhood of `a` within `(a, b)` -/
     u  Ioc a b, Ioo a u  s, /- 3 : `s` includes `(a, u)` for some `u ∈ (a, b]` -/
     u  Ioi a, Ioo a u  s] /- 4 : `s` includes `(a, u)` for some `u > a` -/ :=

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:21):

I think I would put := before comment 4

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:21):

But that's minor nitpicking

view this post on Zulip Sebastien Gouezel (Dec 27 2019 at 16:22):

Also, for one-line comments you can use --.

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:22):

Only if you don't put := at the end of the line

view this post on Zulip Sebastien Gouezel (Dec 27 2019 at 16:23):

Yes. I was implicitly seconding your comment :)

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 16:23):

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
  tfae [s  nhds_within a (Ioi a), -- 0 : `s` is a neighborhood of `a` within `(a, +∞)`
    s  nhds_within a (Ioc a b),   -- 1 : `s` is a neighborhood of `a` within `(a, b]`
    s  nhds_within a (Ioo a b),   -- 2 : `s` is a neighborhood of `a` within `(a, b)`
     u  Ioc a b, Ioo a u  s,    -- 3 : `s` includes `(a, u)` for some `u ∈ (a, b]`
     u  Ioi a, Ioo a u  s] :=   -- 4 : `s` includes `(a, u)` for some `u > a`

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:24):

It's too bad that those comments won't end up in the docstring

view this post on Zulip Johan Commelin (Dec 27 2019 at 16:34):

In fact, I think it's quite important that these comments do end up in the docstring, because if the lemma gets used with tfae.out a person reading the code will probably want to hover over the lemma to see exactly which two equivalent statements are being used.

view this post on Zulip Yury G. Kudryashov (Dec 27 2019 at 16:40):

I'll copy them to the docstring.

view this post on Zulip Rob Lewis (Dec 27 2019 at 19:45):

I agree that the 0/1 indexing should be made consistent and that the numbers should appear in the docstring.

view this post on Zulip Rob Lewis (Dec 27 2019 at 19:46):

Note that (I think) markdown will format a numbered list starting with 1, even if the input starts with 0. i.e.

0. `s` is a neighborhood...
1. `s` is a neighborhood...

will get printed as

1. ...
2. ...

view this post on Zulip Rob Lewis (Dec 27 2019 at 19:47):

So maybe we should use 1-based indexing. Or unordered lists with indices added manually.

view this post on Zulip Mario Carneiro (Dec 27 2019 at 23:45):

Actually, I think we could use an annotation so that we can write:

lemma tfae_mem_nhds_within_Ioi {a b : α} (h : a < b) (s : set α) :
  by tfae [
    Ioi: s  nhds_within a (Ioi a),
    Ioc: s  nhds_within a (Ioc a b),
    Ioo: s  nhds_within a (Ioo a b),
    ex_Ioc:  u  Ioc a b, Ioo a u  s,
    ex_Ioi:  u  Ioi a, Ioo a u  s] :=

and then reference the names using tfae_have Ioi <-> Ioo := tfae_mem_nhds_within_Ioi or similar

view this post on Zulip Mario Carneiro (Dec 27 2019 at 23:47):

It could be syntax for tfae [(\lam Ioi, Ioi) s ∈ nhds_within a (Ioi a), ...

view this post on Zulip Johan Commelin (Dec 28 2019 at 07:40):

I think I could have made tfae_have use 0-based indexing. But these new suggestions go beyond my skill set. They do look fancy. @Mario Carneiro Would tfae.out be able to use those indices as well?

view this post on Zulip Mario Carneiro (Dec 28 2019 at 08:07):

if by tfae.out you mean the term, no

view this post on Zulip Mario Carneiro (Dec 28 2019 at 08:07):

I would also suggest keeping zero based indexing in tfae.out

view this post on Zulip Mario Carneiro (Dec 28 2019 at 08:07):

adding extra layers in the actual terms is a bad idea

view this post on Zulip Johan Commelin (Dec 28 2019 at 09:26):

Well, in that case I would just let everything be 0-based indexed stuff


Last updated: May 14 2021 at 00:42 UTC