Lean 4中如何证明数组索引合法？规避非安全索引方式

针对你遇到的问题，这里提供两种简洁且安全的实现方案，无需使用arr[1]!或arr[1]?这类非安全索引操作：

方案一：用linarith自动推导不等式证明 #

Lean 4的linarith策略可以自动处理简单的数值不等式推导。在你排除arr.size < 64的分支后，上下文会自动携带arr.size ≥ 64的信息，linarith能直接利用这个条件证明索引合法性：

def test (arr : ByteArray) : Except Unit UInt8 := do
  if arr.size < 64 then throw ()
  -- 自动推导1 < arr.size和10 < arr.size
  have hx : 1 < arr.size := by linarith
  have hy : 10 < arr.size := by linarith
  let x := arr[1]'hx
  let y := arr[10]'hy
  return x + y

方案二：利用自然数传递性减少重复证明 #

如果需要多个索引的合法性证明，可以先推导最大索引的合法性，再通过自然数的小于传递性Nat.lt_trans推导更小索引的合法性，避免重复调用linarith：

def test (arr : ByteArray) : Except Unit UInt8 := do
  if arr.size < 64 then throw ()
  -- 先证明最大的索引10 < arr.size
  have h10 : 10 < arr.size := by linarith
  -- 利用1 < 10和10 < arr.size，推导1 < arr.size
  have h1 : 1 < arr.size := Nat.lt_trans (by norm_num) h10
  let x := arr[1]'h1
  let y := arr[10]'h10
  return x + y

补充说明 #

Lean 4不会自动隐式推导数值范围的合法性，这是因为它的类型系统依赖构造性证明，但linarith策略已经封装了处理这类简单数值不等式的逻辑，足以覆盖你的场景。norm_num则用于证明固定数值的大小关系（比如1 < 10）。

内容的提问来源于stack exchange，提问作者Timmmm