Canonicalizing constant Std.BitVec

Stream: lean4

[Juneyoung Lee]

Hi,
How can I canonicalize a constant Std.BitVec

{ toFin := { val := 3, isLt := ... } } -- assume that its bitwidth is 4

into 3#4?

This is some example that I am interested in:

import Std.Data.BitVec.Basic

open Std.BitVec

variable (α : Type)
variable (f : (Std.BitVec 4 × Std.BitVec 4) -> α -> (Std.BitVec 4 × Std.BitVec 4))
         (g : (Std.BitVec 4 × Std.BitVec 4) -> α -> α)
variable (f_g_same: ∀ (x y:Std.BitVec 4) (s:α), f (x,y) (g (x,y) s) = (x,y))

variable (s: α)

example (hyp1:3 < 2 ^ (5-1)) (hyp2:5 < 2 ^ (6-2)):
  f (3#4,5#4) (g
    ({ toFin := { val := 3, isLt := hyp1 } },
     { toFin := { val := 5, isLt := hyp2 } }) s)
  = (3#4,5#4)
  := by
  -- How can I change the goal to 'f (3#4,5#4) (g (3#4,5#4) s) = (3#4,5#4)?
  sorry

[Alex Keizer]

If your desired goal statement is def-eq to your current goal (which is the case in your example), you can use show

example (hyp1:3 < 2 ^ (5-1)) (hyp2:5 < 2 ^ (6-2)):
  f (3#4,5#4) (g
    ({ toFin := { val := 3, isLt := hyp1 } },
     { toFin := { val := 5, isLt := hyp2 } }) s)
  = (3#4,5#4)
  := by
  show f (3#4,5#4) (g (3#4,5#4) s) = (3#4,5#4)
  sorry

If you don't want to manually write out the desired goal statement, you could also prove the following lemma:

theorem ofFin_mk_eq_ofNat (x n : Nat) (h : x < 2^n) : ofFin ⟨x, h⟩ = x#n := by
  simp [Std.BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h]

example (hyp1:3 < 2 ^ (5-1)) (hyp2:5 < 2 ^ (6-2)):
  f (3#4,5#4) (g
    ({ toFin := { val := 3, isLt := hyp1 } },
     { toFin := { val := 5, isLt := hyp2 } }) s)
  = (3#4,5#4)
  := by
  simp [ofFin_mk_eq_ofNat]
  -- ⊢ f (3#4, 5#4) (g (3#4, 5#4) s) = (3#4, 5#4)
  sorry