fix: reducing out-of-bounds swap! should return a, not default

[nomeata]

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

Also adds docstrings.

Fixes #3196

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3197 has successfully built against this PR. (2024-01-18 23:33:46) View Log
• ✅ Mathlib branch lean-pr-testing-3197 has successfully built against this PR. (2024-01-19 00:08:56) View Log

[somombo]

@nomeata just curious .. why wasn't the fix for this inconsistency to change the implementation of Array.set! so as to make it panic instead of changing Array.swap! to make it no-longer panic

[nomeata]

Both set! and swap! do panic when run as compiled funcitons (note the export attribute), and kernel evaluation has no concept of panic, so there now both return the argument array unchanged.