beautifulTable
(This problem is autoformalized using FormalizeWithTest(https://github.com/GasStationManager/FormalizeWithTest), with a slight change in theorem signature noted below) Levko loves tables that consist of n rows and n columns very much. He especially loves beautiful tables. A table is beautiful to Levko if the sum of elements in each row and column of the table equals k. Unfortunately, he doesn't know any such table. Your task is to help him to find at least one of them. Input The single line contains two integers, n and k (1 ≤ n ≤ 100, 1 ≤ k ≤ 1000). Output Print any beautiful table. Levko doesn't like too big numbers, so all elements of the table mustn't exceed 1000 in their absolute value. If there are multiple suitable tables, you are allowed to print any of them. Examples Input 2 4 Output 1 3 3 1 Input 4 7 Output 2 1 0 4 4 0 2 1 1 3 3 0 0 3 2 2 Note In the first sample the sum in the first row is 1 + 3 = 4, in the second row — 3 + 1 = 4, in the first column — 1 + 3 = 4 and in the second column — 3 + 1 = 4. There are other beautiful tables for this sample. In the second sample the sum of elements in each row and each column equals 7. Besides, there are other tables that meet the statement requirements.
Function Signature
def beautifulTable (n k : Nat) : List (List Int)
Theorem Signature
def all_le (l : List Int) (bound : Int) : Bool :=
l.all (fun x => x.natAbs ≤ bound)
def list_sum (l : List Int) : Int :=
l.foldl (· + ·) 0
def all_lists_sum_to (lists : List (List Int)) (target : Int) : Bool :=
lists.all (fun l => list_sum l = target)
def get_column (matrix : List (List Int)) (j : Nat) : List Int :=
matrix.map (fun row => row[j]!)
def get_columns (matrix : List (List Int)) : List (List Int) :=
let n := matrix[0]!.length
List.range n |>.map (fun j => get_column matrix j)
def beautifulTable_prop (n k : Nat) (out : List (List Int)) : Prop :=
let k_int := Int.ofNat k
-- Matrix is n×n
out.length = n ∧
out.all (fun row => row.length = n) ∧
-- All elements ≤ 1000
out.all (fun row => all_le row 1000) ∧
-- All rows sum to k
all_lists_sum_to out k_int ∧
-- All columns sum to k
all_lists_sum_to (get_columns out) k_int
--CHANGED: added precondition that k<=1000 to make this provable
theorem beautifulTable_spec (n k : Nat) (h: k <= 1000): beautifulTable_prop n k (beautifulTable n k)
Please log in or register to submit a solution for this challenge.