From 69bca3ad421f0a4038e8ea97a86818b63b319de7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 2 Aug 2019 13:01:49 -0700
Subject: [PATCH] feat(library/init/data/array/basic): add version of
 `Array.indexOf` with property about resulting size

---
 library/init/data/array/basic.lean | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index 973baf6a10..2697f9e30b 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -450,6 +450,31 @@ eraseIdxAux (i.val + 1) a
 def eraseIdx {α} (a : Array α) (i : Nat) : Array α :=
 if i < a.size then eraseIdxAux (i+1) a else a
 
+theorem szFSwapEq (a : Array α) (i j : Fin a.size) : (a.fswap i j).size = a.size :=
+rfl
+
+theorem szPopEq (a : Array α) : a.pop.size = a.size - 1 :=
+rfl
+
+section
+/- Instance for justifying `partial` declaration.
+   We should be able to delete it as soon as we restore support for well-founded recursion. -/
+instance eraseIdxSzAuxInstance (a : Array α) : Inhabited { r : Array α // r.size = a.size - 1 } :=
+⟨⟨a.pop, szPopEq a⟩⟩
+
+partial def eraseIdxSzAux {α} (a : Array α) : ∀ (i : Nat) (r : Array α), r.size = a.size → { r : Array α // r.size = a.size - 1 }
+| i r heq :=
+  if h : i < r.size then
+    let idx  : Fin r.size := ⟨i, h⟩;
+    let idx1 : Fin r.size := ⟨i - 1, Nat.ltOfLeOfLt (Nat.predLe i) h⟩;
+    eraseIdxSzAux (i+1) (r.fswap idx idx1) ((szFSwapEq r idx idx1).trans heq)
+  else
+    ⟨r.pop, (szPopEq r).trans (heq ▸ rfl)⟩
+end
+
+def eraseIdxSz {α} (a : Array α) (i : Nat) : { r : Array α // r.size = a.size - 1 } :=
+eraseIdxSzAux a i a rfl
+
 end Array
 
 export Array (mkArray)