ignore telescopes

[ahuoguo]

Description

This will deprecate #211 and #598

IIUC, the proofmode use of bi.telescopes is all replaced by lean metaprogramming, and similar tricks can be done when porting logically atomic triples.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

Generative AI Guidelines

AI assistance is permitted when making contributions to Iris-Lean, however, generative AI systems tend to produce code which takes a long time to review.
Please carefully review your code to ensure it meets the following standards.

• Your PR should avoid duplicating constructions found in Iris-Lean or in the Lean standard library.
• have statements that do not aid readability or code reuse should be inlined.
• Your proofs should be shortened such that their overall structure is explicable to a human reader. As a goal, aim to express one idea per line.
• In general, proofs should not perform substantially more case splitting than their Rocq counterparts.

In our experience, a good place to begin refactoring is by re-arranging and combining independent tactic invocations.
We also find that pointing generative AI systems to the Mathlib code style guidelines can help them perform some of this refactoring work.

[markusdemedeiros]

I don't really understand how telescopes are used, but yeah, if they really are Rocq-specific then I think it would be better to ignore with a message describing the Lean way. #598 was a purely blind porting effort 😅

[MackieLoeffel]

I think telescopes might also be useful in Lean, as they are in Rocq. They are very useful when you have definitions that contain multiple binders and I know a few projects based on Iris that use them (often in the context of automation, e.g. Diaframe uses them and other automation). I think they might come in handy for Iris-Lean based projects as well at some point. So I would not ignore them. If we don't want to port them, we can just wait and see if someone needs them.

[ahuoguo]

Thanks for your input! So far, I don't think I really need them for logatom triples.

I think the proofmode ignores are still valid? as documented here: https://github.com/leanprover-community/iris-lean/pull/511/changes#diff-5a2723cddf35ed52cb237eb9d7f363ad47dd49d9711e52394972ab514d9825eaR455-R456 Though I can see if someone ported the telescope architecture they might also want to port all of the relevant proofmode infra.

[MackieLoeffel]

GatherEvarsEq is some specific part of the iframe machinery in Rocq, which does not appear in Lean. Its rocq_ignore just applies to the use of telescopes in iframe, not to telescopes in general.