proved findFinIdx lemma

Author: FrederickPu

Pullback/UnquoteTy/SSA.lean

@@ -132,7 +132,14 @@ def DVector.get : {L : List Type} → (v : DVector L) → (i : Fin L.length) →
 | .cons _ _, (a, _), ⟨0, _⟩ => a
 | .cons _ _, (_, as), ⟨Nat.succ i, h⟩ => DVector.get as ⟨i, Nat.le_of_succ_le_succ h⟩
 
-theorem Array.find?_eq_getElem_findFinIdx? {α : Type u} (xs : Array α) (p : α → Bool): xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by sorry
+theorem Array.find?_eq_getElem_findFinIdx? {α : Type u} (xs : Array α) (p : α → Bool) :
+      xs.find? p = (xs.findFinIdx? p).map (xs[·]) := by
+    rcases xs with ⟨xs⟩; ext
+    simp [List.findFinIdx?_eq_pmap_findIdx?, List.findIdx?_eq_fst_find?_zipIdx,
+        List.find?_eq_some_iff_getElem]
+    constructor
+    · rintro ⟨_, _, _, rfl, _⟩; grind
+    · grind
 
 -- (a : α, true) means break (a : α, false) means continue
 def SSA.loop {α : Type u} [Inhabited α] (init : α) (step : α → α × Bool) : α := sorry