Help with a basic proof about Vectors

Stream: Program verification

[Aiken Cairncross]

I'm writing a data structure for representing n-dimensional (rectangular) arrays using a single flat array to contain the elements and this is needing me to do some of my first non-trivial proofs.

My problem is with defining the GetElem instance for my type. Given a proof that a multi-dimensional index is in bounds of an arrays shape (e.g. the index [5, 50, 15] is in bounds of the shape [10, 100, 20] because each index value is smaller than its corresponding dimension in the shape), I need to prove that the flattening of the multi-dimensional index into a single integer is in the bounds of the size of the flat array. I think I should be able to do it with induction but I can't figure out how/it's not giving me the hypotheses I thought it would.

Thanks in advance!

import Mathlib.Data.Vector

namespace Nat
def product (l : List Nat) : Nat := l.foldr (· * ·) 1
end Nat

namespace RankNArray

structure RankNArray (α : Type) (n : Nat) where
  data : Array α
  shape : Vector Nat n
  property : data.size = Nat.product shape.val

-- flattenIndex [s₀, .. , sₙ] [i₀, .. , iₙ] = (s₁ * .. * sₙ) * i₀ + .. + sₙ * i_(n-1) + iₙ
def flattenIndex (shape : Vector Nat n) (idx : Vector Nat n) : Nat :=
  let strides := (List.scanr (· * ·) 1 shape.val).tail
  let flatIndex := List.foldr (fun (s, i) acc =>
    acc + (s * i)) 0 (strides.zip idx.val)
  flatIndex

-- A multi-dimensional index is in the bounds of a shape if each of the indices
-- is less than its respective dimension.
def inBounds (xs : RankNArray α n) (idx : Vector Nat n) : Prop :=
  (xs.shape.toList.zip idx.toList).all fun (x, i) => i < x

def flattenIndex_inBounds (xs : RankNArray α n) (idx : Vector Nat n) : Prop :=
  flattenIndex xs.shape idx < Nat.product xs.shape.val

instance : GetElem (RankNArray α n) (Vector Nat n) α inBounds where
  getElem (xs : RankNArray α n) (idx : Vector Nat n) ok :=
    let flatIdx := List.foldr (fun a b => b) 0 idx.val
    -- Can't do this without a proof of (flattenIndex_inBounds xs idx):
    -- xs.data[flatIdx]
    sorry
    -- Try and establish (flattenIndex_inBounds xs idx) by proving a theorem
    -- below

-- If a multi-dimensional index is in the bounds of a shape, the flattening of
-- the index is in the bounds of the flattened shape
theorem inBounds_implies_flattenIndex_inBounds (xs : RankNArray α n) (idx : Vector Nat n) :
  inBounds xs idx -> flattenIndex_inBounds xs idx := by
    induction xs.shape.val
    -- where are the hypotheses, e.g. xs.shape.val = nil?
    sorry

end RankNArray

[Thomas Murrills]

Hmm, yeah…where are the hypotheses? I think we might be a bit too eager to clear them.

[Mario Carneiro]

-- If a multi-dimensional index is in the bounds of a shape, the flattening of
-- the index is in the bounds of the flattened shape
theorem inBounds_implies_flattenIndex_inBounds :
  ∀ (shape : Vector ℕ n) (idx : Vector Nat n),
    (h : (shape.toList.zip idx.toList).all fun (x, i) => i < x) →
    flattenIndex shape idx < Nat.product shape.val
  | ⟨shape, hshape⟩, ⟨idx, hidx⟩ => by
    have H1 shape :
        (List.foldr (fun a x ↦ (a * x.1, x.1 :: x.2)) (1, []) shape).1 = Nat.product shape := by
      unfold Nat.product; induction shape <;> simp [*]
    simp only [Vector.toList_mk, List.all_eq_true, decide_eq_true_eq, Prod.forall, flattenIndex,
      List.scanr, List.tail_cons, Nat.product]
    subst n
    induction shape generalizing idx with simp | cons a shape IH => ?_
    cases idx with injection hidx | cons b idx => ?_
    simp
    intro h
    specialize IH idx ‹_› fun a b h' => h a b (.inr h')
    refine (add_lt_add_right IH _).trans_le ?_
    rw [H1, mul_comm a, add_comm, Nat.product, ← Nat.mul_succ]
    have := h _ _ (.inl ⟨rfl, rfl⟩)
    exact Nat.mul_le_mul_left _ (Nat.succ_le_of_lt this)

instance : GetElem (RankNArray α n) (Vector Nat n) α inBounds where
    getElem (xs : RankNArray α n) (idx : Vector Nat n) ok :=
  xs.data[flattenIndex xs.shape idx]'
    (xs.property ▸ inBounds_implies_flattenIndex_inBounds xs.shape idx ok)

[Aiken Cairncross]

Wow, I'll have a good study of that!

[Aiken Cairncross]

Hmm, yeah…where are the hypotheses? I think we might be a bit too eager to clear them.

I'm still interested in the answer to this though!

[Mario Carneiro]

doing induction xs.shape.val will only generalize xs.shape.val where it appears in the goal state, so all other facts about xs are lost (the variable xs is still around but it has no relation to the newly introduced variable being inducted over)

[Mario Carneiro]

That's why my proof works by pattern matching xs instead (or rather, calling a lemma with xs.shape, which itself pattern matches as ⟨shape, hshape⟩). Note that the induction shape line does manage to change the type of hshape to match

[Mario Carneiro]

However, regarding:

    -- where are the hypotheses, e.g. xs.shape.val = nil?

You normally don't want to have something like xs.shape.val = nil in the context after induction, because the only way to get that in the context is to put xs.shape.val = x as part of the induction hypothesis, and this will make the induction hypothesis useless (you will have IH : xs.shape.val = a -> P a and h : xs.shape.val = a :: b in the context, so the hypothesis is not applicable because it has a false assumption), which is why only cases does this (with the syntax cases e : xs.shape.val to introduce e : xs.shape.val = nil in the subgoal), not induction.

[Thomas Murrills]

Shouldn’t these equations be there if we’re generalizing xs, at least, though?