RFC: Array.swap! reduces differently than Array.set!

[nomeata]

Proposal

Array.set! and Array.swap! are fairly similar operations, both modify an array, both take an index that it out of bounds.

But they behave different; all of these return true

#eval #[1,2].set! 2 42 == #[1,2]    -- with panic
#reduce #[1,2].set! 2 42 == #[1,2]  -- no panic

#eval #[1,2].swap! 0 2 == #[1,2]    -- with panic
#reduce #[1,2].swap! 0 2 == default -- no panic

The implementations are

@[extern "lean_array_set"]
def Array.set! (a : Array α) (i : @& Nat) (v : α) : Array α :=
  Array.setD a i v

but

@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
  if h₁ : i < a.size then
  if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
  else panic! "index out of bounds"
  else panic! "index out of bounds"

It seems to be more consistent to unify the behaviors, and define

@[extern "lean_array_swap"]
def swap! (a : Array α) (i j : @& Nat) : Array α :=
  if h₁ : i < a.size then
  if h₂ : j < a.size then swap a ⟨i, h₁⟩ ⟨j, h₂⟩
  else a
  else a

which would also allow us to state lemma Array.size_swap! without the indexing preconditions (which is how I and @david-christiansen stumbled on this).

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.