lines_sudoku

import data.set.function
import data.fintype.basic
import data.finset.basic
import data.fin
import tactic

open finset function

@[derive fintype, derive decidable_eq]
structure cell := (r : fin 9) (c : fin 9)

def row (i : fin 9) : finset cell := filter (λ a, a.r = i) univ
def col (i : fin 9) : finset cell := filter (λ a, a.c = i) univ
def box (i : fin 9) : finset cell := filter (λ a, a.r / 3 = i / 3 ∧ a.c / 3 = i % 3) univ

lemma mem_row (a : cell) (i : fin 9) : a ∈ row i ↔ a.r = i := by simp [row]
lemma mem_col (a : cell) (i : fin 9) : a ∈ col i ↔ a.c = i := by simp [col]
lemma mem_box (a : cell) (i j : fin 3) :
  a ∈ box i ↔ a.r / 3 = i / 3 ∧ a.c / 3 = i % 3 := by simp [box]

def same_row (a : cell) (b : cell) := a.r = b.r
def same_col (a : cell) (b : cell) := a.c = b.c
def same_box (a : cell) (b : cell) := (a.r / 3) = (b.r / 3) ∧ (a.c / 3) = (b.c / 3)

def cell_row (a : cell) : finset cell := row (a.r)
def cell_col (a : cell) : finset cell := col (a.c)
def cell_box (a : cell) : finset cell := box (3*(a.r / 3) + a.c / 3)

def sudoku := cell → fin 9

def row_axiom (s : sudoku) : Prop := ∀ a b : cell, same_row a b → s a = s b → a = b
def col_axiom (s : sudoku) : Prop := ∀ a b : cell, same_col a b → s a = s b → a = b
def box_axiom (s : sudoku) : Prop := ∀ a b : cell, same_box a b → s a = s b → a = b

def normal_sudoku_rules (s : sudoku) : Prop := row_axiom s ∧ col_axiom s ∧ box_axiom s

@[simp] lemma card_row : ∀ (i : fin 9), finset.card (row i) = 9 := dec_trivial
@[simp] lemma card_col : ∀ (i : fin 9), finset.card (col i) = 9 := dec_trivial
@[simp] lemma card_box : ∀ (i : fin 9), finset.card (box i) = 9 := dec_trivial

lemma row_injective (s : sudoku) (h_row : row_axiom s) (i : fin 9) :
  ∀ a b ∈ row i, s a = s b → a = b :=
begin
  intros a b ha hb h_eq,
  have h_srow : same_row a b,
  { rw mem_row at ha hb,
    rw ← hb at ha,
    exact ha
  },
  apply h_row _ _ h_srow h_eq
end

lemma row_surjective (s : sudoku) (h_row : row_axiom s) (i v : fin 9) :
  ∃ c ∈ (row i), v = s c :=
finset.surj_on_of_inj_on_of_card_le 
  (λ c (hc : c ∈ row i), s c)
  (λ _ _, finset.mem_univ _)
  (row_injective s h_row i)
  (by simp)
  _
  (mem_univ _)