How to compute something computable, when proving something?

Stream: new members

[Ilmārs Cīrulis]

I have something like this. I can post the definition of determinant too if necessary, but I wasn't sure that it is relevant here.

Is there some command/tactic that I can use when doing proof by tactics - in this case to "evaluate" determinant test to 12?

def test : Array (Array Int) := #[#[1, 1, 1, 1], #[1, 2, 4, 8], #[1, 3, 9, 27], #[1, 4, 16, 64]]

#eval determinant test
-- it is 12, as expected

theorem determinant_of_test_eq_12 : determinant test = 12 := by
  sorry

[Aaron Liu]

decide will do it

[Aaron Liu]

if your definition is transparent enough

[Ilmārs Cīrulis]

Maybe it isn't transparent enough. Here is all the code (I was learning how to do basic imperative programming in Lean).

def μ {α} [Inhabited α] [Zero α] [Add α] [Neg α] (M : Array (Array α)) : Array (Array α) := Id.run do
  let size := M.size
  let mut temp := Array.replicate size 0
  for i in (Array.range (size-1)).reverse do
    temp := temp.set! i (temp[i+1]! + M[i+1]![i+1]!)
  temp := temp.map (fun x => -x)
  let mut output := Array.replicate size (Array.replicate size 0)
  for i in (0...size) do
    let mut row := output[i]!
    row := row.set! i temp[i]!
    for j in ((i+1)...size) do
      row := row.set! j M[i]![j]!
    output := output.set! i row
  return output

def mul {α} [Inhabited α] [Zero α] [Add α] [Mul α] (M1 M2 : Array (Array α)) : Array (Array α) := Id.run do
  let number_of_rows := M1.size
  let number_of_cols := M2[0]!.size
  let mut output := Array.emptyWithCapacity number_of_rows
  let columns_of_M2 := Array.ofFn (fun (i : Fin number_of_cols) => M2.map (fun x => x[i.val]!))
  for r in (0...number_of_rows) do
    let mut row := Array.emptyWithCapacity number_of_cols
    for c in (0...number_of_cols) do
      let value := (Array.zipWith (fun x y => x * y) M1[r]! columns_of_M2[c]!).sum
      row := row.push value
    output := output.push row
  return output

def F {α} [Inhabited α] [Zero α] [Add α] [Neg α] [Mul α] (A : Array (Array α)) (n : Nat): Array (Array α) :=
  match n with
  | 0 => A
  | m + 1 => mul (μ (F A m)) A

def determinant {α} [Inhabited α] [Zero α] [Add α] [Neg α] [Mul α] (A : Array (Array α)) : α :=
  let result := (F A (A.size - 1))[0]![0]!
  if (A.size % 2 = 0) then -result else result


def test : Array (Array Int) := #[#[1, 1, 1, 1], #[1, 2, 4, 8], #[1, 3, 9, 27], #[1, 4, 16, 64]]

#eval determinant test

theorem determinant_of_test_eq_12 : determinant test = 12 := by
  decide
  sorry

[Weiyi Wang]

I am not sure why this doesn't work, but at least native_decide works so I guess at least the statement is likely correct...

[Aaron Liu]

looks like it got stuck at docs#Std.PRange.RangeIterator.instIteratorLoop.loop

[Kenny Lau]

so decide mirrors #reduce and native_decide mirrors #eval (and is not safe) so you can see that #reduce also fails

[Ilmārs Cīrulis]

So... is it not provable? :melt:

[Aaron Liu]

probably provable you just need to unfold that definition

[Ilmārs Cīrulis]

Removed those PRange and also the use of Array.reverse and now it works.

def μ {α} [Inhabited α] [Zero α] [Add α] [Neg α] (M : Array (Array α)) : Array (Array α) := Id.run do
  let size := M.size
  let mut temp := Array.replicate size 0
  for i in Array.range (size - 1) do
    temp := temp.set! (size - 2 - i) (temp[size - 1 - i]! + M[size - 1 - i]![size - 1 - i]!)
  temp := temp.map (fun x => -x)
  let mut output := Array.replicate size (Array.replicate size 0)
  for i in Array.range (size - 1) do
    let mut row := output[i]!
    row := row.set! i temp[i]!
    for j in Array.range' (i+1) (size-i-1) do
      row := row.set! j M[i]![j]!
    output := output.set! i row
  return output

def mul {α} [Inhabited α] [Zero α] [Add α] [Mul α] (M1 M2 : Array (Array α)) : Array (Array α) := Id.run do
  let number_of_rows := M1.size
  let number_of_cols := M2[0]!.size
  let mut output := Array.emptyWithCapacity number_of_rows
  let columns_of_M2 := Array.ofFn (fun (i : Fin number_of_cols) => M2.map (fun x => x[i.val]!))
  for r in Array.range number_of_rows do
    let mut row := Array.emptyWithCapacity number_of_cols
    for c in Array.range number_of_cols do
      let value := (Array.zipWith (fun x y => x * y) M1[r]! columns_of_M2[c]!).sum
      row := row.push value
    output := output.push row
  return output

def F {α} [Inhabited α] [Zero α] [Add α] [Neg α] [Mul α] (A : Array (Array α)) (n : Nat): Array (Array α) :=
  match n with
  | 0 => A
  | m + 1 => mul (μ (F A m)) A

def determinant {α} [Inhabited α] [Zero α] [Add α] [Neg α] [Mul α] (A : Array (Array α)) : α :=
  let result := (F A (A.size - 1))[0]![0]!
  if (A.size % 2 = 0) then -result else result


def test : Array (Array Int) := #[#[1, 1, 1, 1], #[1, 2, 4, 8], #[1, 3, 9, 27], #[1, 4, 16, 64]]

#eval determinant test
#reduce determinant test

theorem determinant_of_test_eq_12 : determinant test = 12 := by
  decide