mbk/sized-array
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

simplify left-pad a touch

Browse source
This commit is contained in:
mehbark 2023-02-13 21:33:33 -05:00
parent a5040e9b84
commit 1ae5d8eb46
1 changed files with 10 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
SizedArray.lean
View file

@ -498,10 +498,12 @@ def left_pad' (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
: SizedArray α to := by : SizedArray α to := by
let pad_amt := to - n let pad_amt := to - n
let (h₂ : pad_amt = to - n) := rfl let (h₂ : pad_amt = to - n) := rfl
let padding := replicate pad_amt with' let padding := replicate pad_amt with'
let padded := append padding xs let padded := append padding xs
rw [h₂] at padded
rw [Nat.sub_add_cancel] at padded rw [h₂, Nat.sub_add_cancel] at padded
exact padded exact padded
exact h exact h
@ -510,18 +512,19 @@ def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
cases hle : (decide (to ≤ n)) with cases hle : (decide (to ≤ n)) with
| true => | true =>
rw [max, Nat.instMaxNat, maxOfLe] rw [max, Nat.instMaxNat, maxOfLe]
simp
let hle : to ≤ n := of_decide_eq_true hle let hle : to ≤ n := of_decide_eq_true hle
simp [hle] simp [hle]
exact xs exact xs
| false => | false =>
let hle : ¬to ≤ n := of_decide_eq_false hle let hle : ¬to ≤ n := of_decide_eq_false hle
rw [max, Nat.instMaxNat, maxOfLe]
simp [hle]
let hnle := hle let hnle := hle
rw [Nat.not_le_eq, ← Nat.succ_eq_add_one] at hnle rw [Nat.not_le_eq, ← Nat.succ_eq_add_one] at hnle
let hnle := Nat.le_of_succ_le hnle let hnle := Nat.le_of_succ_le hnle
rw [max, Nat.instMaxNat, maxOfLe]
simp
simp [hle]
exact left_pad' to with' xs hnle exact left_pad' to with' xs hnle
#eval left_pad 10 413 (from_list [1,2,3,4,5,6,7])