Chains of implications

Stream: general

[Victor Porton]

In my book, there are many theorems with a chain of implications (I even introduce a special term - implications tuple).

Example:

Theorem. The following is an implications tuple:

1. F is filters on a set
2. F is filters on a meet semilattice with a greatest element
3. F is filters on a poset with a greatest element
4. (Some statement about filters)

The latest implication in the tuple (3->4 in the example) is the statement to be proved. The preceding implications are intended to quickly induce special cases of the theorem. The "longest" implication (1->4 in the example) is the weakest statement for the theorem, that is useful to quickly grasp the "crux" of the theorem.

What should I do, when formalizing this in Lean? If I write (1)->(2)\and(2)->(3)\and(3)->(4), it would become very inconvenient to, for example, infer (1)->(4).

The best ideas that I came with:

1. Prove (1)->(2), (2)->(3), (3)->(4), then prove as consequences (2)->(4), (1)->(4).
2. Introduce a new tactic to handle implications tuples.

In the case 1., need to invent a naming convention or how to use a namespace for each theorem of that kind.

In the case 2., I may need help. Also, need to explain to the AI how to use the new tactic.

Any advice?

[Victor Porton]

Is it at all possible in Lean 4 to create a tactic that gets as input the tuple <(1), (2), (3), (4)> and adds to the list of proved theorems (1)->(4), (2)->(4), (3)->(4)? That is, can a tactic manipulate the (global) list of proved theorems?

[Aaron Liu]

there's docs#List.TFAE, and tactics tfae_have and tfae_finish for working with it

[Victor Porton]

Also, to note that implications (1)->(2), (2)->(3) are not valuable outside the proof of this theorem. I think, they should be lemmas in a namespace that is specifically for this theorem. Then export only important statements. Or indeed write a new tactic specifically for such chains of implications?

[Victor Porton]

@Aaron Liu I see a reference to tfae_have and tfae_finish in https://github.com/leanprover-community/mathlib4/blob/fe7639f2f685b4578335b1ca90f98fceae6b9b85/Mathlib/Data/List/TFAE.lean but can't find where those tactics are defined.

[Aaron Liu]

@loogle "tactic", "tfae"

[loogle]

:search: Mathlib.Tactic.TFAE.tfaeFinish, Mathlib.Tactic.TFAE.tfaeHave, and 11 more

[Aaron Liu]

I guess it's not really the same if you don't do (4) -> (1)

[Violeta Hernández]

Victor Porton ha dicho:

I think, they should be lemmas in a namespace that is specifically for this theorem.

If you have auxiliary lemmas not useful outside of a proof, I'd prefer to make them private altogether.

[Yury G. Kudryashov]

We have docs#List.IsChain

[Yury G. Kudryashov]

Then we have docs#List.IsChain.pairwise

[Yury G. Kudryashov]

Finally, if you want to deduce the last element from another one, you can use docs#List.Pairwise.rel_getLast