Fixed size 2D Array

Stream: Is there code for X?

[shortc1rcuit]

I've been trying to make a fixed size 2D Array in Lean that I can write get/set functions for (for now I've hard coded the size to 4x4). My current solution uses the Array structure. I'm trying to provide proofs that the indexes are in bounds but I'm having issues with the second layer of indexing. For the example Grid I was able to get around this with aesop but that doesn't seem to work in the get function. My current proof for that should work but for some reason the proof terms don't match up. Is there something I can do to fix this or should I try a different structure instead?

import Mathlib.Order.Interval.Finset.Defs
import Mathlib.Order.Interval.Finset.Nat
import Mathlib.Tactic

class Grid where
  grid : Array (Array (Option (Fin 4)))
  hheight : grid.size = 4
  hwidth : ∀ row ∈ grid, row.size = 4

def g_test : Grid where
  grid := #[#[some 1, some 2, none,   some 4],
            #[some 3, some 4, some 1, some 2],
            #[some 2, some 1, some 4, some 3],
            #[some 4, some 3, some 2, some 1]]
  hheight := by decide
  hwidth := by aesop

def Grid.get (g : Grid) (row col : Fin 4) : Option (Fin 4) := (g.grid[row]'(by simp[g.hheight]))[col]'(by {
  convert Fin.is_lt col
  apply g.hwidth

  /-
  tactic 'apply' failed, failed to unify
    grid[?m.3886] ∈ grid
  with
    grid[row] ∈ grid
  -/
  --apply g.grid.getElem?_mem

  sorry
})

[Mario Carneiro]

The issue is that you are using a different instance for array membership than the one used in getElem?_mem. This works:

  exact ⟨List.get_mem ..⟩