@@ -22,14 +22,8 @@ theorem getElem_eq_data_getElem (a : ByteArray) (h : i < a.size) : a[i] = a.data
2222
2323@[simp] theorem data_mkEmpty (cap) : (emptyWithCapacity cap).data = #[] := rfl
2424
25- @[simp] theorem data_empty : empty.data = #[] := rfl
26-
27- @[simp] theorem size_empty : empty.size = 0 := rfl
28-
2925/-! ### push -/
3026
31- @[simp] theorem data_push (a : ByteArray) (b : UInt8) : (a.push b).data = a.data.push b := rfl
32-
3327@[simp] theorem size_push (a : ByteArray) (b : UInt8) : (a.push b).size = a.size + 1 :=
3428 Array.size_push ..
3529
@@ -42,9 +36,6 @@ theorem get_push_lt (a : ByteArray) (x : UInt8) (i : Nat) (h : i < a.size) :
4236
4337/-! ### set -/
4438
45- @[simp] theorem data_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
46- (a.set i v).data = a.data.set i v i.isLt := rfl
47-
4839@[simp] theorem size_set (a : ByteArray) (i : Fin a.size) (v : UInt8) :
4940 (a.set i v).size = a.size :=
5041 Array.size_set ..
@@ -68,15 +59,6 @@ theorem set_set (a : ByteArray) (i : Fin a.size) (v v' : UInt8) :
6859
6960/-! ### append -/
7061
71- @[simp] theorem append_eq (a b) : ByteArray.append a b = a ++ b := rfl
72-
73- @[simp] theorem data_append (a b : ByteArray) : (a ++ b).data = a.data ++ b.data := by
74- rw [←append_eq]; simp [ByteArray.append, size]
75- rw [Array.extract_empty_of_stop_le_start (h:=Nat.le_add_right ..), Array.append_empty]
76-
77- theorem size_append (a b : ByteArray) : (a ++ b).size = a.size + b.size := by
78- simp only [size, append_eq, data_append]; exact Array.size_append ..
79-
8062theorem get_append_left {a b : ByteArray} (hlt : i < a.size)
8163 (h : i < (a ++ b).size := size_append .. ▸ Nat.lt_of_lt_of_le hlt (Nat.le_add_right ..)) :
8264 (a ++ b)[i] = a[i] := by
@@ -89,17 +71,6 @@ theorem get_append_right {a b : ByteArray} (hle : a.size ≤ i) (h : i < (a ++ b
8971
9072/-! ### extract -/
9173
92- @[simp] theorem data_extract (a : ByteArray) (start stop) :
93- (a.extract start stop).data = a.data.extract start stop := by
94- simp [extract]
95- match Nat.le_total start stop with
96- | .inl h => simp [h, Nat.add_sub_cancel']
97- | .inr h => simp [h, Nat.sub_eq_zero_of_le, Array.extract_empty_of_stop_le_start]
98-
99- @[simp] theorem size_extract (a : ByteArray) (start stop) :
100- (a.extract start stop).size = min stop a.size - start := by
101- simp [size]
102-
10374theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start stop).size) :
10475 start + i < a.size := by
10576 apply Nat.add_lt_of_lt_sub'; apply Nat.lt_of_lt_of_le h
@@ -115,15 +86,15 @@ theorem get_extract_aux {a : ByteArray} {start stop} (h : i < (a.extract start s
11586@[inline] def ofFn (f : Fin n → UInt8) : ByteArray :=
11687 Fin.foldl n (fun acc i => acc.push (f i)) (emptyWithCapacity n)
11788
118- @[simp] theorem ofFn_zero (f : Fin 0 → UInt8) : ofFn f = empty := rfl
89+ @[simp] theorem ofFn_zero (f : Fin 0 → UInt8) : ofFn f = empty := by simp [ofFn]
11990
12091theorem ofFn_succ (f : Fin (n+1 ) → UInt8) :
12192 ofFn f = (ofFn fun i => f i.castSucc).push (f (Fin.last n)) := by
12293 simp [ofFn, Fin.foldl_succ_last, emptyWithCapacity]
12394
12495@[simp] theorem data_ofFn (f : Fin n → UInt8) : (ofFn f).data = .ofFn f := by
12596 induction n with
126- | zero => rfl
97+ | zero => simp
12798 | succ n ih => simp [ofFn_succ, Array.ofFn_succ, ih, Fin.last]
12899
129100@[simp] theorem size_ofFn (f : Fin n → UInt8) : (ofFn f).size = n := by
0 commit comments