Array access stuff from SF lean meet-up

arraybounds.lean

/-
Convenience definition that just calls `Array.modify` while keeping things within
the subtype; uses the lemma `Array.size_modify` to show that modifying an element
doesn't change the size.
-/
def subtypeModify {A : Type u} {n : Nat} (xs : { a : Array A // a.size = n }) (i : Nat) (f : A → A) : { a : Array A // a.size = n } :=
  let val := xs.val.modify i f
  ⟨val, (Array.size_modify xs.val i f) ▸ xs.property⟩


def rho (xs : {a : Array UInt8 // a.size = 25}) : {a : Array UInt8 // a.size = 25 } :=
  subtypeModify xs 2 (fun x => x+1)

def theta (xs : {a : Array UInt8 // a.size = 25}) : {a : Array UInt8 // a.size = 25 } :=
  -- Lean infers that 2 is in-bounds because `xs.property` is available in the context.
  -- Disclaimer: I have not read the source for the `get_elem_tactic` that does all of the magic here.
  let snd := xs.val[2]
  subtypeModify xs 12 (fun x => 2*x+snd)

def zeta (xs : {a : Array UInt8 // a.size = 25}) : {a : Array UInt8 // a.size = 25 } :=
  let zth := xs.val[0]
  subtypeModify xs 2 (fun _ => zth)

/-
The "check once and only once at runtime" approach
-/
def main_ (xs : Array UInt8) : Option { a : Array UInt8 // a.size = 25 } :=
  if h : xs.size = 25
  then some (zeta <| theta <| rho ⟨xs, h⟩)
  else none

def testArr : Array UInt8 :=
  #[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24]

#eval main_ testArr

/-
If you have static data and it's not enormous, you can construct the size proof at compile time
-/
def testArr' : { xs : Array UInt8 // xs.size = 25 } :=
  ⟨#[0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24], by decide⟩

#eval main_ testArr'.val


/-
The axiom approach
-/
private axiom arraySizeLt (xs: Array UInt8) : xs.size = 25

def main'_ (xs : Array UInt8) : { a : Array UInt8 // a.size = 25 } :=
  zeta <| theta <| rho ⟨xs, arraySizeLt xs⟩

/-
Can also take an extra hypothesis instead of using a subtype.
-/
def noSubtypeVer (xs : Array UInt8) (h : xs.size = 25) : Array UInt8 :=
  let zth := xs[0]
  xs.modify 7 (fun x => x + zth)

def main''_ (xs : Array UInt8) : Option (Array UInt8) :=
  if h : xs.size = 25
  then some (noSubtypeVer xs h)
  else none