From a5040e9b84bdd0172e5c568e090d4d28561540a7 Mon Sep 17 00:00:00 2001
From: mehbark <terezi@pyrope.net>
Date: Mon, 13 Feb 2023 21:09:32 -0500
Subject: [PATCH] left-pad

---
 SizedArray.lean | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/SizedArray.lean b/SizedArray.lean
index 822b863..d85e1fc 100644
--- a/SizedArray.lean
+++ b/SizedArray.lean
@@ -492,3 +492,36 @@ def take {from_len : Nat} (n : Nat) (xs : SizedArray α from_len)
 -- example : SizedArray Nat 3 := take 3 (by simp) (from_list [1,2,3,4,5])
 
 #eval from_list [1,2,3,4,5,6,7,8,9,10] |> take 7 |> drop 2 |> reverse |> map (· * 2) |> (tail (by simp) ·)
+
+def left_pad' (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
+              (h : n ≤ to)
+  : SizedArray α to := by
+    let pad_amt := to - n
+    let (h₂ : pad_amt = to - n) := rfl
+    let padding := replicate pad_amt with'
+    let padded := append padding xs
+    rw [h₂] at padded
+    rw [Nat.sub_add_cancel] at padded
+    exact padded
+    exact h
+
+def left_pad (to : Nat) {n : Nat} (with' : α) (xs : SizedArray α n)
+  : SizedArray α (max to n) := by
+    cases hle : (decide (to ≤ n)) with
+    | true  => 
+      rw [max, Nat.instMaxNat, maxOfLe]
+      simp
+      let hle : to ≤ n := of_decide_eq_true hle
+      simp [hle]
+      exact xs
+    | false => 
+      let hle : ¬to ≤ n := of_decide_eq_false hle
+      let hnle := hle
+      rw [Nat.not_le_eq, ← Nat.succ_eq_add_one] at hnle
+      let hnle := Nat.le_of_succ_le hnle
+
+      rw [max, Nat.instMaxNat, maxOfLe]
+      simp
+      simp [hle]
+      
+      exact left_pad' to with' xs hnle