WIP: Fix Deep Recursion by Using Bitshift Repr

[dtumad]

Using e.g. 2^16 in place of 2 <<< 16 is what is causing most of the "(kernel) deep recursion detected" issues. This PR swaps to that form, and also tries to just unfold Word.toNat less in general. This happens in the kernel after Lean has unfolded the function calls, so just no opening up Word.toNat isn't enough, we need to actually change this.

import Mathlib

example (n : ℕ) :
    (match
      (match BitVec.ofNat 64 (n * 2^16) with
      | 0#64 => some false
      | _ => some true) with
    | none => ()
    | some _ => ()) =
    if 1 + 1 = 2 then () else () := by
  rw [one_add_one_eq_two] -- causes deep recursion error

example (n : ℕ) :
    (match
      (match BitVec.ofNat 64 (n <<< 16) with
      | 0#64 => some false
      | _ => some true) with
    | none => ()
    | some _ => ()) =
    if 1 + 1 = 2 then () else () := by
  rw [one_add_one_eq_two] -- no deep recursion error

[GZGavinZhao]

You can merge this if you want to. Don't worry about me.

[PetarMax]

Something is going wrong here. split_ands hangs, and then when I override that with [ skip; constructor; constructor; constructor; constructor ] the following split_ifs` hangs.

[dtumad]

Oh sorry, I was only searching for sorry to fix (no pun intended). Will look at this and why they are stalling

[PetarMax]

This congr hangs as well, it didn't before.

[dtumad]

This seems maybe related to the fact that ofNat was causing deep recursion issues when it wasn't already unfolded (and it isn't @[reducible]). Hadn't looked very closely when just refactoring the proof.

[PetarMax]

Possibly. I'm not sure how that would come up in this proof, given that the first change is here...

[dtumad]

My thought was that one side contains e.g. a x * 2^16 and the other a x <<< 16, and Lean is both somehow seeing that, and trying to unify them in congruence which is difficult. I'll investigate more when I get home. This is definitely not the getElem change (given the location of the macro), and none of the bit-shifts should be in scope IIRC (will check when I'm back home)

[dtumad]

This branch has grown too large and still isn't fully finished. Closing in favor of cherry picking individual commits to merge incrementally