inductive variable bindings

Stream: lean4

[Jad Ghalayini]

I've got a proof with a lot of cases that look like

case constructor_55 IA IB =>
   constructor;
   apply IA;
   simp only [some lemmas];
   assumption;
   apply IB;
   simp only [some lemmas];
   apply some_lemma;
   assumption;

I wanted to automate this with something like

induction I <;> {
   constructor;
   apply IA;
   simp only [some lemmas];
   assumption;
   apply IB;
   simp only [some lemmas];
   apply some_lemma;
   assumption;
}

The problem is, ofc, the variables IA and IB are not bound, and I do not know how to make them bound. Any help?

[Leonardo de Moura]

It is hard to tell without seeing the actual goals, but the following tactics may be relevant. They both have doc strings.
rename and rename_i.

[Jad Ghalayini]

Thanks for the quick reply! I'm away from my machine rn, but assuming it works like Coq or such, the problem is that I don't have the initial names for the inductive hypotheses; what I need is an apply * analogue to simp [*]

[Jad Ghalayini]

I see that rename_i doesn't have that problem now, but now I've got a new problem: try rename_i A B fails when there's less than two inaccessible variables. Is this a bug? If not, how can I count inaccessible variables (my cases have either 0, 1, 2, or 3; I can handle 0 first but the other ones I don't know how to distinguish)

[Jannis Limperg]

Would it help if you had a tactic that just tries to apply every hyp from the context, using the first that works? (So like assumption but the application doesn't have to close the goal.) I have something like that lying around.

More generally, this sounds like a problem that my Aesop tactic would be a good fit for. It's basically Coq/Isabelle's auto with bells and whistles. It's still unpolished and changing quickly, so I hesitate to recommend it, but if you'd like to try it, I'd be curious to hear whether it works for you.

[Jad Ghalayini]

@Jannis Limperg that would actually be perfect; as a Lean noob, how do I do this?

[Jad Ghalayini]

Also in general is there a nice page where I can see a list of tactics? Those rename tactics were also very helpful, but I don't know where I would have found them if not told about their existence

[Jannis Limperg]

Jad Ghalayini said:

Jannis Limperg that would actually be perfect; as a Lean noob, how do I do this?

This info should be in the readme in the Aesop repo. But it's a bit unfriendly right now, mixing implementation and usage, and doesn't have good examples. I'll write a better readme today or early next week. (I'm currently changing a part of the UI as well, so I'd like to wait for that.)

[Jannis Limperg]

Jad Ghalayini said:

Also in general is there a nice page where I can see a list of tactics? Those rename tactics were also very helpful, but I don't know where I would have found them if not told about their existence

Afaik no (and I regularly discover new stuff as well). For tactics defined in Core, Init/Notation.lean in the stdlib lists most (all?) tactics. Look for the Parser.Tactic namespace. For mathlib4, check Mathlib/Tactic/*.lean, particularly Basic.lean.

[Siddhartha Gadgil]

https://leanprover.github.io/theorem_proving_in_lean4/ is a very good reference.

[Arthur Paulino]

Wow!! #tpil4 is revamped!
It's looking great :octopus:

Edit: actually, looking at the commit history, I can't find a particularly big commit. But it has very few holes marked with "TODO: waiting for well-founded support in Lean 4". Those are the only ones I can find.

[Henrik Böving]

Leo fixed lots of those TODOs in quite a short time quite a bit ago.

[Jannis Limperg]

Jannis Limperg said:

This info should be in the readme in the Aesop repo. But it's a bit unfriendly right now, mixing implementation and usage, and doesn't have good examples. I'll write a better readme today or early next week. (I'm currently changing a part of the UI as well, so I'd like to wait for that.)

This took longer than I thought (nothing ever doesn't), but Aesop now has a more friendly README in case you'd like to try it.

[Patrick Massot]

https://github.com/JLimperg/aesop/blob/master/README.md

[Patrick Massot]

Jannis, did you try to make tests comparing aesop to more specialized tactics like tactic#continuity? This continuity tactic is potentially very useful but it is so slow that it is not used in practice. I guess it wouldn't take too much patience to build a fake topology library and test aesop here. Maybe with mathport oleans you could even test it on the real lemmas (adding aesop tags and some test in a Lean 4 file importing mathlib oleans).

[Patrick Massot]

I don't know how to properly use the linkifier here. I meant https://leanprover-community.github.io/mathlib_docs/tactics.html#continuity%20/%20continuity', which sounds to do a specialized subset of what aesop is meant to do.

[Jannis Limperg]

I haven't done it yet but this is definitely planned. Aesop should indeed be able to replace these tactics with relatively little additional effort.

[Patrick Massot]

Do you expect better performance? Or is aesop meant to be an expensive tactic (maybe also outputting a faster tactic call to be replaced with)?

[Jannis Limperg]

With continuity, I'd expect good performance because afaict there is not much choice (i.e. for each goal there tends to be at most one lemma that applies), so the search shouldn't branch much. I have a test that proves Even 1000 by counting down in increments of 2 and that takes about 1s. Of course there the rule set is very small and entirely deterministic, so not sure how this will translate.

In general, I'm not sure how Aesop will be used. I'd like to try whether it can be used to solve complex goals with big rule sets as well, and I'll implement a squeeze_simp-like mode to enable this. But maybe it'll turn out that the algorithm is too weak and the tactic always fails on complex goals, in which case it might get relegated to automating continuity-style problems.

[Sebastian Ullrich]

Do you see any fundamental reasons for why it might be (much) less effective or practical than auto in Isabelle?

[Sebastian Ullrich]

By the way, I'm planning to take a closer look at it next semester for the second edition our Lean 4 lab with @Jakob von Raumer, especially whether it might help students with the final projects

[Jannis Limperg]

No, auto level should be doable. It's a bit hard to tell what exactly auto does because there's no documentation and I've never seriously used Isabelle, but from what I can tell, the basic approach is very similar. Aesop will just need a ton of work setting up all the lemmas (and I'll need to fix a lot of bugs).

I'd be very curious whether you find it useful for teaching! Though whether it'll help the students or whether they'll be bug-hunting guinea pigs remains to be seen.

[Sebastian Ullrich]

I can at least tell you that the Isabelle example solution is completely dependent on auto (and a few similar ones like blast) :) . simp only gets you so far in program verification, you really want to do some forward reasoning steps etc. in between.

[Sebastian Ullrich]

This might already be the case for Aesop, but I should mention that perhaps auto's best feature is that despite its heuristics, it reports sensible intermediate goals on failure that usually give you a pretty good idea on what lemma to prove & include next

[Jannis Limperg]

Ah, interesting. Do you know whether it does anything smarter than dumping the unsolved goals? Right now I don't have any debugging beyond trace messages, which is not great. (I really need a good MSc student to visualise the traces and the final search tree. I think this could be really nice but I don't want to do it. :P)

[Sebastian Ullrich]

It might be reporting the furthest safe goal, but I'm not really sure to be honest

[Jannis Limperg]

Ah okay, makes some sense. That I can do as well.

[Simon Hudon]

I don't know if that's relevant but I have a prototype of Coq-style auto I've been working on, using discrimination tree to index lemmas and combining forward and backward reasoning. I'd be happy to polish it off if that helps

[Jannis Limperg]

Do publish please! I'm interested in your integration of forward reasoning in particular.

[Patrick Massot]

I'm curious about all this mystery surrounding Isabelle's auto. I understand there is no paper about it. Is this closed source? Or is it simply very hard to read the code and we don't have access to the author?