Mistake in Recursion, Induction, and Rewriting notebook

[benbellick]

You can see here that the docs mark this particular inductive proof as a "success", though taking up the full max_induct depth of 3.

Yet the proof actually fails:

And when I try and actually run it in the separate notebook, it still fails:

[benbellick]

@grantpassmore Wanted to get your input because I'm not sure if the right fix is to either:
a) change the proof somehow so that it goes through, or
b) change the docs to say that that proof fails

I presume that that proof went through in an older version of imandra, but doesn't now. 🤷

[benbellick]

I actually tried it locally and it goes through with max_induct set to 4

[grantpassmore]

Wow, nice find! I believe we originally had a default of max_induct of 5, and we then changed it to a default of 3 later (which is a better default for sure):

Bizarre that we didn't notice the change in this notebook though (we have various things that look for failures in the doc notebooks). Probably the best move at the moment is to up the max_induct for that example to, e.g., 5, and update the text. This update could use the new local syntax for changing max_induct! That'd be super nice.

I am deep in some waterfall work (for imandrax mostly, but also relevant to imandra-nox) and I'll take a deeper look at this as part of that (it'd be very interesting if we did used to prove it with less inductions than we do now, for example!).