-- An index into a particular string s: a Nat together with a proof
-- that it is less than s's size. The type mentions the value s.

def s2ac (s : String) : Array Char := s.toList.toArray

def hello : Array Char := s2ac "hello"
def world : Array Char := s2ac "world"

structure Idx (s : Array Char) where
  i : Nat
  h : i < s.size

-- s[k.i]'k.h: index s at k.i, using the proof k.h
def safeGet (s : Array Char) (k : Idx s) : Char := s[k.i]'k.h

-- 'e'
#eval safeGet hello ⟨1, by decide⟩
-- error: 5 < hello.size is false
-- #eval safeGet hello ⟨5, by decide⟩

-- The string in the type can be any expression, including one
-- computed at run time; here the proof comes from a test.
def getCat (s t : Array Char) (i : Nat) : Option Char :=
  let u := s ++ t
  if h : i < u.size then some (safeGet u ⟨i, h⟩) else none

-- some 'w'
#eval getCat hello world 5

-- The proof can use facts about variables.
def first (s : Array Char) (nonempty : s.size > 0) : Char := safeGet s ⟨0, by omega⟩
def last (s : Array Char) (nonempty : s.size > 0) : Char := safeGet s ⟨s.size - 1, by omega⟩
-- error: s might be empty
-- def last' (s : Array Char) : Char := safeGet s ⟨s.size - 1, by omega⟩

-- 'h'
#eval first hello (by decide)
-- 'o'
#eval last hello (by decide)

-- An index into s is also an index into s ++ t...
-- def idxLonger' (s t : Array Char) (k : Idx s) : Idx (s ++ t) := ⟨k.i, k.h⟩
-- ... but only with a proof.
def idxLonger (s t : Array Char) (k : Idx s) : Idx (s ++ t) :=
  ⟨k.i, by have := k.h; simp; omega⟩
-- error: k.h is about s.size, not (s ++ t).size

-- 'e'
#eval safeGet (hello ++ world) (idxLonger hello world ⟨1, by decide⟩)

-- In a loop over the indices, each i comes with a proof h that it is
-- in the range [0, s.size); h.upper is the part that says i < s.size.
def count (s : Array Char) (c : Char) : Nat := Id.run do
  let mut n := 0
  for h : i in [:s.size] do
    if safeGet s ⟨i, h.upper⟩ == c then n := n + 1
  return n

-- 2
#eval count hello 'l'