what do you prefer

Stream: general

[Huỳnh Trần Khanh]

what do you prefer, the equation compiler or the induction tactic? sometimes I find the equation compiler more flexible, like I can exploit well-founded recursion to prove theorems and I don't have to explicitly generalize variables

[Huỳnh Trần Khanh]

I used to say lemma, but now I have to say "theorem". Lean 4 is literally Newspeak.

[Eric Wieser]

For defs, the equation compiler produces helpful lemmas you wouldn't get if you used induction

[Eric Wieser]

However, there are lots of cases where the equation compiler picks brec and induction picks rec, and IIRC the later is computationally faster

[Eric Wieser]

Mario might be able to expand on that last point

[Horatiu Cheval]

I almost always use induction for proofs. I think the only situations where I found the equation compiler preferable are like this. Say you want to prove something by induction on both n m : nat and the only interesting case is the pattern n (n + 1), while the other cases are trivially impossible (and therefore trivially true by exfalso). Then using the equation compiler I could get away with just writing the interesting pattern, and it would just figure out the other cases by itself, without me having to write them.