How to avoid rename_i

Stream: new members

[Tobias Grosser]

I am currently trying to proof this statement:

theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
    (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
  ext
  simp
  rename_i i
  -- Goal:
  -- (!decide (w ≤ ↑i) && if n + ↑i < w then xor (x.getLsb (n + ↑i))
  -- (y.getLsb (n + ↑i)) else xor x.msb y.msb) =
  -- xor (!decide (w ≤ ↑i) && if n + ↑i < w then x.getLsb (n + ↑i) else x.msb)
  -- (!decide (w ≤ ↑i) && if n + ↑i < w then y.getLsb (n + ↑i) else y.msb)
  by_cases h₁ : (w ≤ ↑i)
  · simp [h₁]
  · simp [h₁]
    by_cases h₂ : n + ↑i < w <;> simp [h₂]

My proof goes through, but I dislike the rename_i and even the explicit statement of the cases where I split. However, split does not apply to decide and by_cases needs the prices hypothesis (for which I need to name i). :confused:

I feel this can be polished, given some more lean expertise.

[Yaël Dillies]

Instead of

  ext
  simp
  rename_i i

you should be doing

  ext i
  simp

[Tobias Grosser]

Perfect. I knew I missed sth obvious.

[Tobias Grosser]

Thank you.

[Tobias Grosser]

I guess the other parts are harder to golf?

[Yaël Dillies]

Maybe split does the case split for you? I'm not sure it works with decide... but if it doesn't then I'm sure the core Lean developers can be convinced to extend its scope to include it

[Tobias Grosser]

This now is simplified to:

theorem sshiftRight_xor_distrib (x y : BitVec w) (n : Nat) :
    (x ^^^ y).sshiftRight n = (x.sshiftRight n) ^^^ (y.sshiftRight n) := by
  ext i
  simp
  split <;>
  by_cases h₁ : w ≤ i <;>
  simp [*]

[Tobias Grosser]

Thank you. Would be nice if split would work on decide too.

[Yaël Dillies]

Feel free to open an issue to the lean4 repo!