getMsbD_ushiftRight

Stream: lean4

[Luisa Cicolini]

I am proving this theorem:

namespace BitVec

theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
    getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
  simp only [getMsbD, Bool.if_false_left]
  by_cases h : i < w
  <;> by_cases h₁ : i < n
  <;> by_cases h₂ : i - n < w
  all_goals (simp [h, h₁, h₂]; try congr; try omega)
  rw [BitVec.getLsbD_ge]
  omega

It currently works, however, I am trying to make it better. In fact, congr and omega are only required in a few of the cases resulting from the by_cases, and unfolding simp to simp only introduces quite a lot of theorems.
Is there any other strategy I could use?
Thanks :)

[Notification Bot]

A message was moved here from #lean4 > Proper way to define an algebra for a catamorphism? by Luisa Cicolini.

[Yann Herklotz]

My one suggestion is the following maybe, but I feel like the proof is already quite compact:

open BitVec
theorem getMsbD_ushiftRight {w} {x : BitVec w} {i n : Nat} :
    getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
  simp only [getMsbD, Bool.if_false_left]
  by_cases h : i < w
  <;> by_cases h₁ : i < n
  <;> by_cases h₂ : i - n < w
  <;> simp (discharger := omega) [h, h₁, h₂]
  congr; omega

This makes the proof significantly faster too, likely because simp can discharge side conditions of simp lemmas in the BitVec library.

[Luisa Cicolini]

thanks a lot!