Automation and existentials

Stream: lean4

[Patrick Massot]

I have a question about the current status and near future of automation. In many talks I use as an example of a proof using no lemma the proof at https://github.com/PatrickMassot/GlimpseOfLean/blob/master/GlimpseOfLean/Introduction.lean that continuity implies sequential continuity. After the use line, solve_by_elim or tauto (or aesop) can finish the proof (but duper cannot). How far are we from having a tactic that does the full proof? Is is in scope for grind for instance (I have only a very vague idea of what grind is meant to do when it will be ready)?

[Josh Clune]

Not an answer to your question, but I'm surprised Duper doesn't get this after the use line. To confirm, is it duper [*] that fails at that line or just duper? The former tells Duper to use everything in the local context while the latter only looks at the target.

[Patrick Massot]

Indeed duper [*] works.

[Patrick Massot]

Funnily, it seems only tauto works before the use N line.

[Kim Morrison]

grind [Function.comp_def] works after the use N line. (And presumably when we annotate the library just grind will work there.) We'll have a look at what would be required to have it manage the use N, too.