Modeling correct-by-construction Sudoku in Agda

Sudoku.agda

open import Data.Fin as Fin using (Fin ; #_ ; _≟_)
open import Data.Fin.Properties using (suc-injective)
open import Level as Level using (Level)
open import Data.Unit using (⊤ ; tt)
open import Data.Empty
open import Data.Product as Product
open import Data.Product.Properties as Product using (,-injective ; ≡-dec)
open import Data.Sum
open import Relation.Binary.PropositionalEquality
open import Data.Nat using (ℕ ; _+_)
open import Data.Nat.Literals as Nat
open import Data.Fin.Literals as Fin
open import Level.Literals as Lvl
open import Agda.Builtin.FromNat
open import Data.Vec as Vec using (Vec ; _∷_ ; [])
import Data.Vec.Properties as Vec
open import Relation.Nullary.Decidable
open import Function using (case_of_ ; _↔_ ; mk↔ₛ′)
open import Relation.Binary using (DecidableEquality)

instance
  NumFin : ∀ {n} → Number (Fin n)
  NumFin {n} = Fin.number n

  NumNat : Number ℕ
  NumNat = Nat.number

--   NumLvl : Number Level
--   NumLvl = Lvl.Levelℕ
-- 
-- variable ℓ : Level

Rel : Set → Set → Set₁
Rel A B = A → B → Set

Irrelevant : ∀{A B} → Rel A B → Set
Irrelevant R = ∀{a b} → (x y : R a b) → x ≡ y

Cell Num Row Col Blk : Set
Num = Fin 4
Row = Fin 4
Col = Fin 4
Blk = Fin 4
Cell = Row × Col

R : Rel Row Cell
R row (row′ , _) = row ≡ row′

C : Rel Col Cell
C col (_ , col′) = col ≡ col′

lookup2 : ∀ {A : Set} {n m} → Vec (Vec A n) m → Fin m × Fin n → A
lookup2 v (r , c) = Vec.lookup (Vec.lookup v r) c

B : Rel Blk Cell
B b (r , c) = b ≡ lookup2
  ((0 ∷ 0 ∷   1 ∷ 1 ∷ []) ∷
   (0 ∷ 0 ∷   1 ∷ 1 ∷ []) ∷

   (2 ∷ 2 ∷   3 ∷ 3 ∷ []) ∷
   (2 ∷ 2 ∷   3 ∷ 3 ∷ []) ∷ [])
  (r , c)

Cell′ : Set
Cell′ = Blk × Fin 4

B′ : Rel Blk Cell′
B′ b (b′ , _) = b ≡ b′

rel→ʳ : ∀{A B B′} → (B′ → B) → Rel A B → Rel A B′
rel→ʳ from R x y = R x (from y)

rel→ˡ : ∀{A A′ B} → (A′ → A) → Rel A B → Rel A′ B
rel→ˡ from R x y = R (from x) y 

_∘_ : ∀{A B C : Set} → Rel A B → Rel B C → Rel A C
(R ∘ S) x z = ∃[ y ] R x y × S y z

open Function.Inverse

∘→ : ∀{A B B′ C} {R : Rel A B} {S : Rel B C} → (f : B ↔ B′) → ∀ x y → (R ∘ S) x y → (rel→ʳ (f .from) R ∘ rel→ˡ (f .from) S) x y
∘→ {R = R} {S} f _ _ (x , r , s) = f .to x , subst (λ X → R _ X) (sym (proj₂ (f .inverse) refl)) r , subst (λ X → S X _) (sym (proj₂ (f .inverse) refl)) s
  
record Sudoku : Set₁ where
    field
      N : Rel Cell Num
      distinct-r : Irrelevant (R ∘ N)
      distinct-c : Irrelevant (C ∘ N)
      distinct-b : Irrelevant (B ∘ N)
open Sudoku

dec-fin : ∀ {n} {f : Fin n → Set} → (∀ x → Dec (f x)) → Dec (∀ x → f x) 
dec-fin {ℕ.zero} _ = yes (λ ())
dec-fin {ℕ.suc n} f with f Fin.zero | dec-fin (λ i → f (Fin.suc i))
... | yes x | yes y = yes λ where
  Fin.zero → x
  (Fin.suc i) → y i
... | yes x | no y = no λ f → y (λ i → f (Fin.suc i))
... | no x | _ = no (λ f → x (f Fin.zero))

dec-distinct₁ : ∀{A : Set} {n} (_ : DecidableEquality A) (x : A) (f : Fin n → A) → Dec (∀ i → x ≢ f i)
dec-distinct₁ {n = ℕ.zero} _≟_ x f = yes (λ ())
dec-distinct₁ {n = ℕ.suc n} _≟_ x f with x ≟ f Fin.zero | dec-distinct₁ {n = n} _≟_ x (λ i → f (Fin.suc i))
... | yes x | _ = no (λ f → f Fin.zero x)
... | no x | yes y = yes λ where
  Fin.zero x₂ → x x₂
  (Fin.suc i) x₂ → y i x₂
... | no x | no y = no (λ f → y λ i → f (Fin.suc i))

dec-distinct : ∀{A : Set} {n} (_ : DecidableEquality A) (f : Fin n → A) → Dec (∀ i j → (f i ≡ f j) → i ≡ j)
dec-distinct {n = ℕ.zero} _≟_ f = yes (λ _ ())
dec-distinct {n = ℕ.suc n} _≟_ f with dec-distinct₁ _≟_ (f Fin.zero) (λ i → f (Fin.suc i)) | dec-distinct _≟_ (λ i → f (Fin.suc i))
... | yes x | yes y = yes λ where
  Fin.zero Fin.zero _ → refl
  Fin.zero (Fin.suc j) z → case x j z of λ ()
  (Fin.suc i) Fin.zero z → case x i (sym z) of λ ()
  (Fin.suc i) (Fin.suc j) z → cong Fin.suc (y i j z)
... | yes _ | no y = no λ f → y (λ i j x → suc-injective (f (Fin.suc i) (Fin.suc j) x))
... | no x | _ = no λ f → x λ i x₁ → case f Fin.zero (Fin.suc i) x₁ of λ ()

-- Slower but simpler :)
-- dec-distinct _≟_ f = dec-fin (λ i → dec-fin λ j →
--   case i Fin.≟ j of λ where
--     (yes x) → yes (λ _ → x)
--     (no x) → case f i ≟ f j of λ where
--       (yes y) → no λ z → x (z y)
--       (no y) → yes (λ z → ⊥-elim (y z)))

board : Vec (Vec Num 4) 4
board = ((0 ∷ 1 ∷   2 ∷ 3 ∷ []) ∷
         (2 ∷ 3 ∷   0 ∷ 1 ∷ []) ∷

         (1 ∷ 0 ∷   3 ∷ 2 ∷ []) ∷
         (3 ∷ 2 ∷   1 ∷ 0 ∷ []) ∷ [])

blkBoard : Vec (Vec Cell 4) 4
blkBoard = (((0 , 0) ∷ (0 , 1) ∷   (1 , 0) ∷ (1 , 1) ∷ []) ∷
            ((0 , 2) ∷ (0 , 3) ∷   (1 , 2) ∷ (1 , 3) ∷ []) ∷

            ((2 , 0) ∷ (2 , 1) ∷   (3 , 0) ∷ (3 , 1) ∷ []) ∷
            ((2 , 2) ∷ (2 , 3) ∷   (3 , 2) ∷ (3 , 3) ∷ []) ∷ [])

cell↔cell′ : Cell ↔ Cell′
cell↔cell′ = mk↔ₛ′
  (lookup2 blkBoard)
  (lookup2 blkBoard)
  (λ where (x , y) → from-yes (dec-fin (λ x → dec-fin (λ y → ≡-dec _≟_ _≟_ (lookup2 blkBoard (lookup2 blkBoard (x , y))) (x , y)))) x y)
  (λ where (x , y) → from-yes (dec-fin (λ x → dec-fin (λ y → ≡-dec _≟_ _≟_ (lookup2 blkBoard (lookup2 blkBoard (x , y))) (x , y)))) x y)

-- blk-ix→cell : Blk × Fin 4 → Cell
-- blk-ix→cell = lookup2 blkBoard

B→B′ : ∀ x y → rel→ʳ (cell↔cell′ .from) B x y → B′ x y
B→B′ x (Fin.zero , Fin.zero) refl = refl
B→B′ x (Fin.zero , Fin.suc Fin.zero) refl = refl
B→B′ x (Fin.zero , Fin.suc (Fin.suc Fin.zero)) refl = refl
B→B′ x (Fin.zero , Fin.suc (Fin.suc (Fin.suc Fin.zero))) refl = refl
B→B′ x (Fin.suc Fin.zero , Fin.zero) refl = refl
B→B′ x (Fin.suc Fin.zero , Fin.suc Fin.zero) refl = refl
B→B′ x (Fin.suc Fin.zero , Fin.suc (Fin.suc Fin.zero)) refl = refl
B→B′ x (Fin.suc Fin.zero , Fin.suc (Fin.suc (Fin.suc Fin.zero))) refl = refl
B→B′ x (Fin.suc (Fin.suc Fin.zero) , Fin.zero) refl = refl
B→B′ x (Fin.suc (Fin.suc Fin.zero) , Fin.suc Fin.zero) refl = refl
B→B′ x (Fin.suc (Fin.suc Fin.zero) , Fin.suc (Fin.suc Fin.zero)) refl = refl
B→B′ x (Fin.suc (Fin.suc Fin.zero) , Fin.suc (Fin.suc (Fin.suc Fin.zero))) refl = refl
B→B′ x (Fin.suc (Fin.suc (Fin.suc Fin.zero)) , Fin.zero) refl = refl
B→B′ x (Fin.suc (Fin.suc (Fin.suc Fin.zero)) , Fin.suc Fin.zero) refl = refl
B→B′ x (Fin.suc (Fin.suc (Fin.suc Fin.zero)) , Fin.suc (Fin.suc Fin.zero)) refl = refl
B→B′ x (Fin.suc (Fin.suc (Fin.suc Fin.zero)) , Fin.suc (Fin.suc (Fin.suc Fin.zero))) refl = refl

-- ∘→ : ∀{A B B′ C} {R : Rel A B} {S : Rel B C} → (f : B ↔ B′) → ∀{x y} → (R ∘ S) x y → (rel→ʳ (f .from) R ∘ rel→ˡ (f .from) S) x y

map2 : ∀{n m} {A B : Set} → (A → B) → Vec (Vec A m) n → Vec (Vec B m) n
map2 f v = Vec.map (Vec.map f) v

lookup2-map2 : ∀{m n A B} {f : A → B} {v : Vec (Vec A m) n} {i : Fin n × Fin m} → lookup2 (map2 f v) i ≡ f (lookup2 v i)
lookup2-map2 {f = f} {v = v} {i = r , c} = trans (cong (λ X → Vec.lookup X c) (Vec.lookup-map r (Vec.map f) v)) (Vec.lookup-map c f (Vec.lookup v r))

test : Sudoku
test .N (r , c) w = w ≡ lookup2 board (r , c)
test .distinct-r ((r , c₁) , refl , refl) ((.r , c₂) , refl , N) with from-yes (dec-fin (λ i → dec-distinct _≟_ (λ j → lookup2 board (i , j)))) r c₁ c₂ N | N
... | refl | refl = refl
test .distinct-c ((r₁ , c) , refl , refl) ((r₂ , .c) , refl , N) with from-yes (dec-fin (λ j → dec-distinct _≟_ (λ i → lookup2 board (i , j)))) c r₁ r₂ N | N
... | refl | refl = refl
test .distinct-b {a} {b} x y with ∘→ {A = Blk} {B = Cell} {B′ = Cell′} {C = Num} {R = B} {S = test .N} cell↔cell′ a b x | ∘→ {A = Blk} {B = Cell} {C = Num} {R = B} {S = test .N} cell↔cell′ a b y
test .distinct-b {a} {b} x y | ((b₁ , i₁) , B₁ , refl) | ((b₂ , i₂) , B₂ , N) with B→B′ a (b₁ , i₁) B₁ | B→B′ a (b₂ , i₂) B₂
test .distinct-b x y | ((b , i₁) , _ , refl) | ((.b , i₂) , _ , N) | refl | refl with from-yes (dec-fin (λ i → dec-distinct _≟_ (λ j → lookup2 board (i , j)))) b i₁ i₂ (trans (lookup2-map2 {f = lookup2 board} {v = blkBoard} {i = b , i₁}) (trans N (sym (lookup2-map2 {f = lookup2 board} {v = blkBoard} {i = b , i₂})))) | N
... | refl | refl = {!!}