Lean 4 ByteArray/Array/List Proof Patterns

ByteArray/Array/List Indexing

• data.data[pos] = data[pos] (where data : ByteArray) is rfl
• For data.data.toList[pos] = data[pos]: simp only [Array.getElem_toList] suffices (as of v4.29.0-rc2; on rc1 a trailing ; rfl was also needed)
• When List.getElem_map is involved (e.g. (arr.toList.map f)[i] = f arr[i]): simp only [List.getElem_map, Array.getElem_toList] closes the goal

Length Conversions

• Array.length_toList: arr.toList.length = arr.size
• List.size_toArray: (l.toArray).size = l.length — bridges Array.size to List.length for array literals (#[a, b, c] elaborates as List.toArray [a, b, c])
• ByteArray.size_data: ba.data.size = ba.size
• Chain them for ba.data.toList.length

Concrete array size in simp only: To reduce #[a, b, ...].size to a number, use List.size_toArray + List.length_cons + List.length_nil:

lean
1simp only [myArray, List.size_toArray, List.length_cons, List.length_nil]
2-- Reduces #[a, b, c].size to 3

Note: Array.size_toArray does NOT exist — use List.size_toArray.

getElem?_pos/getElem!_pos for Array Lookups

To prove arr[i]? = some arr[i]!, use the two-step pattern:

lean
1rw [getElem!_pos arr i h]  -- rewrites arr[i]! to arr[i] (bounds-checked)
2exact getElem?_pos arr i h  -- proves arr[i]? = some arr[i]

getElem?_pos needs the explicit container argument (not _) to avoid GetElem? type class synthesis failures.

Fin Coercion Mismatch in omega

When a lemma over Fin n is applied as lemma ⟨k, hk⟩, omega treats arr[(⟨k, hk⟩ : Fin n).val]! and arr[k]! as different variables.

Fix by annotating the result type:

lean
1have : arr[k]! ≥ 1 := lemma ⟨k, hk⟩

Critical: have := lemma ⟨k, hk⟩ (without type annotation) does NOT work — the anonymous hypothesis retains the Fin.val form and omega still sees two distinct variables. Always use the annotated form.

Deeper mismatch — GetElem vs getInternal: After unfold f at h, the goal may use Array.getInternal (the raw internal accessor) while a helper lemma uses arr[i]'hi (the GetElem typeclass). Even with type annotation, omega treats these as distinct expressions. The fix is exact with Nat.le_trans (or similar) instead of omega, since exact does full definitional unification:

lean
1-- BAD: omega can't unify GetElem-based and getInternal-based array access
2have := helper_lemma code hlt  -- uses arr[code]'hlt via GetElem
3omega  -- fails: sees arr[code].fst and (arr.getInternal code hlt).fst as distinct
4
5-- GOOD: exact does definitional unification
6exact Nat.le_trans (helper_lemma code hlt) (Nat.le_add_right _ _)

decide_cbv on Fin-Bounded Array Properties

To verify a property holds for all entries of a concrete array, use decide_cbv on a Fin-bounded universal:

lean
1private theorem all_baselines_ge_three :
2    ∀ i : Fin myTable.size, (myTable[i.val]'i.isLt).1 ≥ 3 := by
3  decide_cbv

Then wrap in a Nat-indexed helper to avoid Fin coercion issues in callers:

lean
1private theorem baseline_ge_three (i : Nat) (hi : i < myTable.size) :
2    (myTable[i]'hi).1 ≥ 3 :=
3  all_baselines_ge_three ⟨i, hi⟩

Key constraints:

• The ∀ i : Fin n, P i form is needed for decide_cbv — it must be a closed proposition (no free Nat variables)
• decide (without _cbv) has the same constraint but may be slower
• The Nat wrapper eliminates the Fin coercion so callers can use exact or Nat.le_trans without the GetElem/getInternal mismatch

List.getElem_of_eq for Extracting from List Equality

When hih : l1 = l2 and you need l1[i] = l2[i], use List.getElem_of_eq hih hbound where hbound : i < l1.length. This avoids dependent-type rewriting issues with direct rw [hih] on getElem.

n + 0 Normalization Breaks rw Patterns

As of v4.29.0-rc2, Lean normalizes n + 0 to n earlier. If a lemma's conclusion contains arr[pfx.size + k] and you instantiate k = 0, the rewrite target arr[pfx.size + 0] won't match the goal's arr[pfx.size]. Fix: add a specialized _zero variant of the lemma that states the result with arr[pfx.size] directly.

take/drop ↔ Array.extract

To bridge List.take/List.drop (from spec) with Array.extract (from native):

lean
1simp only [Array.toList_extract, List.extract, Nat.sub_zero, List.drop_zero]

Then ← List.map_drop + List.drop_take for drop-inside-map-take.

Array.toArray_toList

a.toList.toArray = a for any Array. Use Array.toArray_toList. NOT Array.toList_toArray or List.toArray_toList — those don't exist.

readBitsLSB_bound for omega

readBitsLSB n bits = some (val, rest) implies val < 2^n. Essential for bounding UInt values (e.g., hlit_v.toNat < 32) before omega can prove ≤ UInt16.size.

List Nat ↔ Array UInt8 Roundtrip

To prove l = (l.toArray.map Nat.toUInt8).toList.map UInt8.toNat when all elements are ≤ 15 (from ValidLengths):

lean
1simp only [Array.toList_map, List.map_map]; symm
2rw [List.map_congr_left (fun n hn => by
3  show UInt8.toNat (Nat.toUInt8 n) = n
4  simp only [Nat.toUInt8, UInt8.toNat, UInt8.ofNat, BitVec.toNat_ofNat]
5  exact Nat.mod_eq_of_lt (by have := hv.1 n hn; omega))]
6simp  -- closes `List.map (fun n => n) l = l` (not `List.map id l`)

Note: List.map_congr_left produces fun n => n not id, so List.map_id won't match — use simp instead.

UInt8→Nat→UInt8 Roundtrip

To prove Nat.toUInt8 (UInt8.toNat u) = u:

lean
1unfold Nat.toUInt8 UInt8.ofNat UInt8.toNat
2rw [BitVec.ofNat_toNat, BitVec.setWidth_eq]

Do NOT use simp [Nat.toUInt8, UInt8.toNat, ...] — it loops via UInt8.toNat.eq_1 / UInt8.toNat_toBitVec. Do NOT try congr 1 (max recursion) or UInt8.ext / UInt8.eq_of_toNat_eq (don't exist).

For lists: l.map (Nat.toUInt8 ∘ UInt8.toNat) = l via List.map_congr_left with the above per-element proof, then simp.

ByteArray Concatenation Indexing

When proving properties about concatenated ByteArrays (e.g. header ++ payload ++ trailer), use the getElem!_append_left/getElem!_append_right chain. Key lemmas (in Zip/Spec/BinaryCorrect.lean):

Two-part concatenation:

lean
1getElem!_append_left  (a b : ByteArray) (i : Nat) (h : i < a.size) :
2    (a ++ b)[i]! = a[i]!
3getElem!_append_right (a b : ByteArray) (i : Nat) (h : i < b.size) :
4    (a ++ b)[a.size + i]! = b[i]!

Three-part concatenation (a ++ b ++ c):

lean
1getElem!_append3_left  (a b c) (i) (h : i < a.size) :
2    (a ++ b ++ c)[i]! = a[i]!
3getElem!_append3_mid   (a b c) (i) (h : i < b.size) :
4    (a ++ b ++ c)[a.size + i]! = b[i]!
5getElem!_append3_right (a b c) (i) (h : i < c.size) :
6    (a ++ b ++ c)[(a ++ b).size + i]! = c[i]!

Reading integers from concatenated arrays:

lean
1readUInt32LE_append_left   (a b) (offset) (h : offset + 4 ≤ a.size) :
2    readUInt32LE (a ++ b) offset = readUInt32LE a offset
3readUInt32LE_append_right  (a b) (offset) (h : offset + 4 ≤ b.size) :
4    readUInt32LE (a ++ b) (a.size + offset) = readUInt32LE b offset
5readUInt32LE_append3_mid   (a b c) (offset) (h : offset + 4 ≤ b.size) :
6    readUInt32LE (a ++ b ++ c) (a.size + offset) = readUInt32LE b offset

Pattern for three-part concat proofs (common in gzip/zlib framing):

1. Unfold the function to expose individual getElem! or readUInt32LE calls
2. Apply getElem!_append3_* or readUInt32LE_append3_* lemma for each byte/field
3. Resolve arithmetic offsets with show a.size + offset + k = a.size + (offset + k) from by omega
4. Close size bounds with by simp [ByteArray.size_append]; omega

Size of concatenation: ByteArray.size_append : (a ++ b).size = a.size + b.size

Build Missing API, Don't Work Around It

If a proof is blocked by missing lemmas for standard types (ByteArray, Array, List, UInt32, etc.), add the missing lemma to ZipForStd/ in the appropriate namespace. For example, if ByteArray.foldl_toList is missing, add it in ZipForStd/ByteArray.lean in the ByteArray namespace. These lemmas are candidates for upstreaming to Lean's standard library — write them as if they belonged there. Don't use workarounds like going through .data.data.foldl when the right fix is a proper API lemma.