From 7117db1549794c91652e9b1a4db35f38d19e39d5 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 6 May 2024 09:51:51 +0200 Subject: [PATCH] refactors: Array.feraseIdx: avoid have in definition MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit otherwise it remains in the equational theorem and may cause the “unused have linter” to trigger. By moving the proof into `decreasing_by`, the equational theorems are unencumbered by termination arguments. see also https://github.com/leanprover/std4/pull/690#issuecomment-2095378609 --- src/Init/Data/Array/Basic.lean | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 98993600555a..eacc93235ef6 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -733,17 +733,15 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α := if h : i.val + 1 < a.size then let a' := a.swap ⟨i.val + 1, h⟩ i let i' : Fin a'.size := ⟨i.val + 1, by simp [a', h]⟩ - have : a'.size - i' < a.size - i := by - simp [a', Nat.sub_succ_lt_self _ _ i.isLt] a'.feraseIdx i' else a.pop termination_by a.size - i.val -decreasing_by simp_wf; decreasing_trivial_pre_omega +decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by induction a, i using Array.feraseIdx.induct with - | @case1 a i h a' _ _ ih => + | @case1 a i h a' _ ih => unfold feraseIdx simp [h, a', ih] | case2 a i h =>