Does Lean list choices?

Stream: new members

[Daniel Donnelly]

Hi. Was wondering what kind of conclusions Lean can come to on its own, and thus if it can "list choices" when you're proving something. For instance if it knows f : A -> B is a function and I assert that there's an x in A, then can I "list choices" here one of which would be "there exists an element f(x) in B". I'm still learning Lean, so not sure how it all works. I can work with it either way for my app. For instance the suggested choices pane in the app could be constructed by user statistics or simply ordering the choices by "how many times did this choice appear in the steps of a successful proof". That should be easy enough and not require much on the server side to aggregate the usage stats and update each user's copy.

[Johan Commelin]

I think that what you would want is some sort of diagram chasing tactic. At the moment there is no such thing. But we are approaching additive/abelian categories in mathlib. Once we have those, such a tactic will be on several peoples wishlist.

[Daniel Donnelly]

So you have it for other things than diagram chasing?

[Johan Commelin]

There is tidy.

[Johan Commelin]

For a nice story of what it does (more or less), you should read the paper by Gowers and Ganesalingam.

[Johan Commelin]

I'm quite sure that you'll find it interesting.

[Johan Commelin]

https://arxiv.org/abs/1309.4501

[Daniel Donnelly]

Thanks! I will look at it