dependent elimination failed when running `case heq`

Stream: new members

[One Happy Fellow]

Hi all,

I'm doing proofs on BitVecs and I want to state a correctness property equating two BitVecs which don't have definitionally equal type parameters, only equal ones.

On line 45 of the linked code, lean complains that "dependent elimination failed" - I'm completely lost here, what does that error mean? What's the best way to resolve it?

Thanks all!

#mwe:

open BitVec

structure ShaBlock where
  block : Array (BitVec 32)
  hlen : block.size = 16 := by grind

def ShaBlock.ofBits (b : BitVec 512) : ShaBlock :=
  let block : Array (BitVec 32) :=
    Array.range (512/32) |>.map fun i =>
      have heq : (((i+1)*32-1) - i*32 + 1) = 32 := by omega
      heq ▸ (b.extractLsb ((i+1)*32-1) (i*32))
  have hlen : block.size = 16 := by
    unfold block
    rw [Array.size_map, Array.size_range]
  { block, hlen := hlen }

def concatBitVecArray'
    {n : Nat}
    (a : Array (BitVec n))
    (i : Nat)
    (hlen : i ≤ a.size)
    (acc : BitVec (i * n)) : BitVec (a.size * n) :=
  if heq : i = a.size
  then by rw [←heq]; exact acc
  else
    have hlen : i < a.size := by omega
    have heq : (i + 1) * n = i * n + n := by
      rw [Nat.mul_comm, Nat.mul_add]; simp; rw [Nat.mul_comm]
    let acc : BitVec ((i + 1) * n) :=  by
      rw [heq]
      exact acc ++ a[i]
    have hlen : i + 1 ≤ a.size := by omega
    concatBitVecArray' a (i+1) hlen acc

def concatBitVecArray {n : Nat} (a : Array (BitVec n)) : BitVec (a.size * n) :=
  concatBitVecArray' a 0 (by simp) (by simp; exact BitVec.ofNat 0 0)

set_option diagnostics true

theorem ShaBlocks.ofBits_sound (b : BitVec 512) :
    have hlen : (ShaBlock.ofBits b).block.size * 32 = 512 := by
      rw [(ShaBlock.ofBits b).hlen]
    hlen ▸ concatBitVecArray (ShaBlock.ofBits b).block = b := by
  intro hlen
  cases hlen
  sorry

[Etienne Marion]

It's better to use #backticks to send code, it automatically puts a button to open the code in the web editor.

[One Happy Fellow]

Thank you, I edited the message!

[Kyle Miller]

With (ShaBlock.ofBits b).block.size * 32 = 512, the only way cases could succeed is if it can turn this into some equations where one side is a variable. In this case, neither side is obviously a variable.

[Kyle Miller]

Hint about working with parameterized types: using rewrite tactics and the triangle operator in definitions can lead to a lot of pain. You can use functions like docs#BitVec.cast to have finer-grained control of the rewrite, and there are simp lemmas about such functions.

open BitVec

structure ShaBlock where
  block : Array (BitVec 32)
  hlen : block.size = 16 := by grind

def ShaBlock.ofBits (b : BitVec 512) : ShaBlock :=
  let block : Array (BitVec 32) :=
    Array.range (512/32) |>.map fun i =>
      (b.extractLsb ((i+1)*32-1) (i*32)).cast (by omega)
  have hlen : block.size = 16 := by
    unfold block
    rw [Array.size_map, Array.size_range]
  { block, hlen := hlen }

def concatBitVecArray'
    {n : Nat}
    (a : Array (BitVec n))
    (i : Nat)
    (hlen : i ≤ a.size)
    (acc : BitVec (i * n)) : BitVec (a.size * n) :=
  if heq : i = a.size
  then acc.cast (by rw [heq])
  else
    have hlen : i < a.size := by omega
    have heq : (i + 1) * n = i * n + n := by
      rw [Nat.mul_comm, Nat.mul_add]; simp; rw [Nat.mul_comm]
    let acc : BitVec ((i + 1) * n) :=
      (acc ++ a[i]).cast heq.symm
    have hlen : i + 1 ≤ a.size := by omega
    concatBitVecArray' a (i+1) hlen acc

def concatBitVecArray {n : Nat} (a : Array (BitVec n)) : BitVec (a.size * n) :=
  concatBitVecArray' a 0 (by simp) ((BitVec.ofNat 0 0).cast (by simp))

set_option diagnostics true

theorem ShaBlocks.ofBits_sound (b : BitVec 512) :
    haveI hlen : (ShaBlock.ofBits b).block.size * 32 = 512 := by
      rw [(ShaBlock.ofBits b).hlen]
    (concatBitVecArray (ShaBlock.ofBits b).block).cast hlen = b := by
  sorry

[Kyle Miller]

That doesn't get you much closer to proving the goal — it will be some induction argument — but hopefully it helps avoid rewriting-data-induced problems.

[One Happy Fellow]

Thank you, I can handle proving the goal but I was stuck at getting rid of the triangle operator.

[One Happy Fellow]

using rewrite tactics and the triangle operator in definitions can lead to a lot of pain

How would I avoid using rewrite lemmas and triangle operator here?

[Kyle Miller]

The code I gave eliminated it.