字节证明=> Nat 构建

Question

我有兴趣了解如何改进这个引理（这是更大证明的一部分，见下文），因为它对我来说仍然有点“冗长”。请注意，我没有使用 Mathlib，而是更喜欢坚持使用

Std4

（现在是电池？）：

-- A simple proof for "right shifting" bytes.  Suppose a value n which fits
-- within an array of k bytes.  We want to append a new byte in the leftmost
-- position.  This lemma then tells us that the resulting number fits within k+1
-- bytes.
def pow256_shr(n:Nat)(m:UInt8)(k:Nat)(p:n < 256^k) : (m.val * 256^k + n < 256^(k+1)) :=
by
  let l := m.toNat
  --
  have q : l ≤ 255 := by exact Nat.le_of_lt_succ m.val.isLt
  have r : l * 256^k ≤ 255*256^k := by exact Nat.mul_le_mul_right (256 ^ k) q
  have s : l * 256^k + 256^k ≤ 256^(k+1) := by omega
  have t : l * 256^k + n < l * 256^k + 256^k := by
    exact Nat.add_lt_add_left p (l * 256 ^ k)
  exact Nat.lt_of_lt_of_le t s

我认为

calc

风格的证明可能会更好，但没有成功。有什么想法吗？

附录

作为参考，我在证明中使用了上面的引理，该证明限制了从大端表示法的字节列表生成的数字的大小。这是生成函数：

def from_bytes_be(bytes:List UInt8) : Nat :=
  match bytes with
  | List.nil => 0
  | b::bs =>
      let n := bs.length
      (b.toNat * (256^n)) + (from_bytes_be bs)

这是边界证明：

-- Bound the number returned by `from_bytes_be`.  For example, if one byte is
-- passed into `from_bytes_be` then the return value is bounded by `256`;
-- likewise, if two bytes are passed into `from_bytes_be` then the return value
-- is bounded by `65536`, etc.
def from_bytes_be_bound(bytes:List UInt8) : (from_bytes_be bytes) < 256^bytes.length :=
by
  match bytes with
  | [] => simp_arith
  | b::bs =>
      apply pow256_shr
      apply (from_bytes_be_bound bs)

Answer 1

也许：

def pow256_shr (n : Nat) (m : UInt8) (k : Nat) (p : n < 256^k) :
    (m.val * 256^k + n < 256^(k+1)) := by
  have mLt : (m.val : Nat) < 256 := m.val.isLt
  calc
    _ ≤ 255 * 256^k + n := Nat.add_le_add_right (Nat.mul_le_mul_right (256^k) (by omega)) n
    _ < 255 * 256^k + 256^k := Nat.add_lt_add_left p (255 * 256^k)
    _ = 256^k * 256 := by rw [← Nat.succ_mul, Nat.mul_comm]

如果您使用 Mathlib 的

calc

策略，您可以使

gcongr

块中的证明变得更好（因此您不需要自己管理

Nat.add_le_add_right

等）。