nqueens.lean

namespace nqueens
open nat

class lt (n : out_param ℕ) (m : ℕ)
instance succ_lt_succ_of_lt (n m) [lt n m] : lt (succ n) (succ m) := by constructor
instance zero_lt_succ (m) : lt 0 (succ m) := by constructor

class ne (n m : ℕ)
instance ne_of_lt (n m) [lt n m] : ne n m := by constructor
instance ne_of_gt (n m) [lt m n] : ne n m := by constructor

class add (n m : ℕ) (r : out_param ℕ)
instance add_zero (n) : add n 0 n := by constructor
instance add_succ (n m r) [add n m r] : add n (succ m) (succ r) := by constructor

def queen := ℕ × ℕ

class nice (q : queen) (qs : list queen)
instance nice_nil (q) : nice q [] := by constructor
instance nice_cons (x y x' y' d1 d2 d1' d2' qs)
  [ne x x']
  [ne y y']
  [add x y' d1]
  [add x' y d1']
  [ne d1 d1']
  [add x y d2]
  [add x' y' d2']
  [ne d2 d2']
  [nice (x,y) qs]
  : nice (x,y) ((x',y')::qs) := by intros; constructor

meta def mk_unary_nat : ℕ → expr
| 0 := ```(0)
| (n+1) := ```(succ %%(mk_unary_nat n))

class queens (n : ℕ) (qs : out_param (list queen))
instance queens_0 : queens 0 [] := by constructor
instance queens_succ (n x qs)
  [queens n qs]
  [lt x (by tactic.apply (mk_unary_nat 8))]
  [nice (x,n) qs]
  : queens (succ n) ((x,n)::qs) := by intros; constructor

set_option class.instance_max_depth 2048
def sol (n) {qs} [queens n qs] : list (ℕ × ℕ) := qs
#eval sol 8
end nqueens