tfae formatting

Stream: general

[Johan Commelin]

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.

[Yury G. Kudryashov]

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 -/ :=

[Johan Commelin]

Yes, exactly

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Johan Commelin]

I guess that should be fixed

[Yury G. Kudryashov]

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` -/ :=

[Johan Commelin]

I think I would put := before comment 4

[Johan Commelin]

But that's minor nitpicking

[Sebastien Gouezel]

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

[Johan Commelin]

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

[Sebastien Gouezel]

Yes. I was implicitly seconding your comment :)

[Yury G. Kudryashov]

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`

[Johan Commelin]

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

[Johan Commelin]

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.

[Yury G. Kudryashov]

I'll copy them to the docstring.

[Rob Lewis]

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

[Rob Lewis]

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. ...

[Rob Lewis]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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?

[Mario Carneiro]

if by tfae.out you mean the term, no

[Mario Carneiro]

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

[Mario Carneiro]

adding extra layers in the actual terms is a bad idea

[Johan Commelin]

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

[Junyan Xu]

Rob Lewis said:

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

As of now they're still inconsistent, and I spent 30min figuring out what the problem was 3 days ago until I found this thread :)
proving it vs. using it

[Junyan Xu]

Adding notes at https://leanprover-community.github.io/mathlib_docs/data/list/tfae.html#list.tfae.out, https://leanprover-community.github.io/mathlib_docs/tactic/tfae.html#tactic.interactive.tfae_have or https://leanprover-community.github.io/mathlib_docs/tactics.html#tfae would be helpful, at least in my case.

[Yury G. Kudryashov]

A PR with better docstrings would be very welcome!