Constructing and Proving Properties of Arrays

Stream: new members

[Kajani Kaunda]

Hello,

I am hoping I could get some help! Consider the following code:

import Mathlib.Data.Nat.Prime.Basic
import Mathlib.Data.List.Basic
import Mathlib.Tactic.Linarith
import Mathlib.Data.Int.Defs
import Mathlib.Tactic.Basic
import Mathlib.Tactic
import Mathlib.Data.Finset.Basic

open List Nat

-- DEFINITION 1. .
-- Construct the Cayley table T for a finite portion
def cayley_table (n : ℕ) : List (List ℤ) :=
  let primes := (List.range n).filter Nat.Prime |>.map (λ p => ↑p)
  let inverses := primes.map (λ p => -p)
  let first_row := 0 :: primes
  let table := inverses.map (λ inv => inv :: (primes.map (λ p => p + inv)))
  first_row :: table

-- Example of using the cayley_table with a finite portion
def T : List (List ℤ) := cayley_table 30

#eval T -- To visualize a portion of the table

-- DEFINITION 2. ..
-- Define a sub-array TTi of T, where v x w are its dimensions
def sub_array (T : List (List ℤ)) (r c v w : ℕ) : List (List ℤ) :=
  if v < 2 ∨ w < 2 then
    []  -- Return an empty list if dimensions are smaller than 2x2
  else
    (T.drop r).take v |>.map (λ row => (row.drop c).take w)

-- Example: Extract a 3x3 sub-array from T
def TT1 : List (List ℤ) := sub_array T 1 1 3 3

#eval TT1 -- Visualize the sub-array

-- DEFINITION 3. ...
-- Define the structure for the 4-tuple β
structure Beta where
  A : ℤ
  B : ℤ
  L : ℤ
  E : ℤ

-- Create a 4-tuple β from the vertices of a sub-array TTi
def create_beta (TTi : List (List ℤ)) : Beta :=
  ⟨TTi.head!.head!, TTi.head!.getLast!, TTi.getLast!.head!, TTi.getLast!.getLast!⟩

-- Example usage: Create β for TT1
def β1 : Beta := create_beta TT1

#eval β1.A -- Visualize β1
#eval β1.B -- Visualize β1
#eval β1.L -- Visualize β1
#eval β1.E -- Visualize β1

lemma lemma_mnck (m n c k : ℤ) :
  let int_A := m + n
  let int_B := m + (n + k)
  let int_L := (m + c) + n
  let int_E := (m + c) + (n + k)
  int_B + int_L = int_A + int_E :=  by
   linarith

theorem lemma_pqxy (h : ∃ (p q : ℤ), p < q) : ∃ (x y : ℤ), (p - x) + (q - y) = (q - x) + (p - y) := by
  obtain ⟨p, q, h_pq⟩ := h
  let x : ℤ := 0
  let y : ℤ := 0
  use x, y
  simp [add_comm, add_assoc]

It defines:

1. A 2-dimensional array T where each row is strictly increasing. For a row r, r[i]<r[j] for i<j.
   This is because every element in a row is defined by subtracting an element in the first column of T from
   an element in the first row of T.

2. A sub array TT of T with a minimum dimension of 2x2.

3. A 4-tuple beta (β) that can be defined from a sub array TT of T and whose elements β.A, β.B, β.L, β.E
   are the vertices of TT.
   β.A = top-left β.B = top-right β.L = bottom-left β.E = bottom_right

4. It also proves the following trivial results:
   lemma lemma_mnck (m n c k : ℤ) : let int_A := m + n let int_B := m + (n + k) let int_L := (m + c) + n let int_E := (m + c) + (n + k) int_B + int_L = int_A + int_E := by linarith
theorem lemma_pqxy (h : ∃ (p q : ℤ), p < q) : ∃ (x y : ℤ), (p - x) + (q - y) = (q - x) + (p - y) := by obtain ⟨p, q, h_pq⟩ := h let x : ℤ := 0 let y : ℤ := 0 use x, y simp [add_comm, add_assoc]
   How can I use these facts (and other things I dont know of!) to prove the following? (I have tried and failed!)

lemma beta_satisfies_mnck (T : List (List ℤ)) (r c v w : ℕ) (h : v ≥ 2 ∧ w ≥ 2) :
  let TT := sub_array T r c v w
  let β := create_beta TT
  β.B + β.L = β.A + β.E :=
  by sorry

lemma beta_satisfies_pqxy (T : List (List ℤ)) (r c v w : ℕ) (h : v ≥ 2 ∧ w ≥ 2) :
  let TT := sub_array T r c v w
  let β := create_beta TT
  ∃ (p q x y : ℤ), p < q ∧
    β.A = (p - x) ∧
    β.B = (q - x) ∧
    β.L = (p - y) ∧
    β.E = (q - y) :=
  by sorry

I hope the statements themselves are formalized correctly!