Work on Sudoku solving with Dedukti.

Sudoku/sudoku.dk

+
+
+
+
+ind : Type.
+1 : ind.
+2 : ind.
+3 : ind.
+4 : ind.
+5 : ind.
+6 : ind.
+7 : ind.
+8 : ind.
+9 : ind.
+X : ind.
+
+def P : ind -> ind.
+[] P 1 --> X.
+[] P 2 --> 1.
+[] P 3 --> 2.
+[] P 4 --> 3.
+[] P 5 --> 4.
+[] P 6 --> 5.
+[] P 7 --> 6.
+[] P 8 --> 7.
+[] P 9 --> 8.
+
+def S : ind -> ind.
+[] S 1 --> 2.
+[] S 2 --> 3.
+[] S 3 --> 4.
+[] S 4 --> 5.
+[] S 5 --> 6.
+[] S 6 --> 7.
+[] S 7 --> 8.
+[] S 8 --> 9.
+[] S 9 --> X.
+
+def trunc3 : ind -> ind.
+[]  trunc3 X --> X.
+[]  trunc3 1 --> 1.
+[]  trunc3 4 --> 1.
+[]  trunc3 7 --> 1.
+[i] trunc3 i --> P i.
+
+bool : Type.
+T : bool.
+F : bool.
+
+def and : bool -> bool -> bool.
+[x] and T x --> x
+[x] and F x --> F.
+
+def or : bool -> bool -> bool.
+[x] or T x --> T
+[x] or F x --> x.
+
+def not : bool -> bool.
+[] not T --> F
+[] not F --> T.
+
+def eq : ind -> ind -> bool.
+[x]   eq x x --> T
+[x,y] eq x y --> F.
+
+
+def ite : A : Type -> bool -> A -> A -> A.
+[A,x] ite A T x _ --> x
+[A,x] ite A F _ x --> x.
+
+
+ind_list : Type.
+Empty' : ind_list.
+Cons' : ind -> ind_list -> ind_list.
+
+sudo : Type.
+Empty : sudo.
+Cons : ind_list -> sudo -> sudo.
+
+def E : ind_list :=
+	Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X (Cons' X Empty')))))))).
+def empty_sudo : sudo :=
+	Cons  E (Cons  E (Cons  E (Cons  E (Cons  E (Cons  E (Cons  E (Cons  E (Cons  E Empty )))))))).
+	
+def set' : ind -> ind -> ind_list -> ind_list.
+[j,k,a,l] set' j k (Cons' a l) --> ite ind_list (eq j 1) (Cons' k l) (Cons' a (set' (P j) k l)).
+
+def set : ind -> ind -> ind -> sudo -> sudo.
+[i,j,k,a,l] set i j k (Cons a l) --> ite sudo (eq i 1) (Cons (set' j k a) l) (Cons a (set (P i) j k l)).
+
+
+def get' : ind -> ind_list -> ind.
+[j,a,l] get' j (Cons' a l) --> ite ind (eq j 1) a (get' (P j) l).
+
+def get : ind -> ind -> sudo -> ind.
+[i,j,a,l] get i j (Cons a l) --> ite ind (eq i 1) (get' j a) (get (P i) j l).
+
+
+
+def exists' : (ind -> bool) -> ind -> bool.
+[f  ] exists' f X --> F
+[f,i] exists' f i --> or (f i) (exists' f (S i)).
+
+def exists : (ind -> bool) -> bool := f => exists' f 1.
+
+
+def mem_line : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
+
+def mem_col  : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_col i j k s --> exists (j' => eq (get i j' s) k).
+
+def mem_squ  : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_squ i j k s -->
+  (i':ind =>
+   j':ind =>
+     or (or (eq (get i'         j'         s) k)
+        (or (eq (get (S i')     j'         s) k)
+	        (eq (get (S (S i')) j'         s) k)))
+    (or (or (eq (get i'         (S j')     s) k)
+	    (or (eq (get (S i')     (S j')     s) k)
+	        (eq (get (S (S i')) (S j')     s) k)))
+        (or (eq (get i'         (S (S j')) s) k)
+	    (or (eq (get (S i')     (S (S j')) s) k)
+	        (eq (get (S (S i')) (S (S j')) s) k))))
+  )
+  (trunc3 i) (trunc3 j).
+
+
+
+def check : ind -> ind -> ind -> sudo -> bool :=
+i => j => k => s =>
+     and (not (mem_line i j k s))
+   ( and (not (mem_col  i j k s))
+         (not (mem_squ  i j k s))).
+
+
+solution : Type.
+success : sudo -> solution.
+fail : solution.
+
+
+def iffail : solution -> solution -> solution.
+[x] iffail (success x) _ --> success x
+[d] iffail fail     d --> d.
+
+def solve : ind -> ind -> ind -> sudo -> solution.
+[i,s]     solve i X _ s --> solve (S i) 1 1 s.
+[  s]     solve X _ _ s --> success s.
+[i,j,s]   solve i j X s --> fail.
+[i,j,k,s] solve i j k s -->
+  ite solution
+    (eq (get i j s) X)
+    (ite solution
+      (check i j k s)
+      (iffail
+        (solve i (S j) 1 (set i j k s))
+        (solve i j (S k) s)
+      )
+      (solve i j (S k) s)
+    )
+    (solve i (S j) 1 s).
+
+
+def solve_sudo : sudo -> solution := s => solve 1 1 1 s.
+
+
+def extract_sol : solution -> sudo.
+[x] extract_sol (success x) --> x.
+
+
+
+def sol := solve_sudo empty_sudo.
+#EVAL sol.
+

Sudoku/sudoku2.dk

+ind : Type.
+1 : ind.
+2 : ind.
+3 : ind.
+4 : ind.
+5 : ind.
+6 : ind.
+7 : ind.
+8 : ind.
+9 : ind.
+X : ind.
+
+def P : ind -> ind.
+[] P 1 --> X.
+[] P 2 --> 1.
+[] P 3 --> 2.
+[] P 4 --> 3.
+[] P 5 --> 4.
+[] P 6 --> 5.
+[] P 7 --> 6.
+[] P 8 --> 7.
+[] P 9 --> 8.
+
+def S : ind -> ind.
+[] S 1 --> 2.
+[] S 2 --> 3.
+[] S 3 --> 4.
+[] S 4 --> 5.
+[] S 5 --> 6.
+[] S 6 --> 7.
+[] S 7 --> 8.
+[] S 8 --> 9.
+[] S 9 --> X.
+
+def trunc3 : ind -> ind.
+[]  trunc3 1 --> 1
+[]  trunc3 2 --> 1
+[]  trunc3 3 --> 1
+[]  trunc3 4 --> 4
+[]  trunc3 5 --> 4
+[]  trunc3 6 --> 4
+[]  trunc3 7 --> 7
+[]  trunc3 8 --> 7
+[]  trunc3 9 --> 7.
+
+bool : Type.
+T : bool.
+F : bool.
+
+def and : bool -> bool -> bool.
+[x] and T x --> x
+[x] and F x --> F.
+
+def or : bool -> bool -> bool.
+[x] or T x --> T
+[x] or F x --> x.
+
+def not : bool -> bool.
+[] not T --> F
+[] not F --> T.
+
+def eq : ind -> ind -> bool.
+[x]   eq x x --> T
+[x,y] eq x y --> F.
+
+
+def ite : A : Type -> bool -> A -> A -> A.
+[A,x] ite A T x _ --> x
+[A,x] ite A F _ x --> x.
+
+
+list : A : Type -> Type.
+l : A : Type -> A -> A -> A -> A -> A -> A -> A -> A -> A -> list A.
+
+def get' : A : Type -> ind -> list A -> A.
+[A,x] get' A 1 (l A x _ _ _ _ _ _ _ _) --> x
+[A,x] get' A 2 (l A _ x _ _ _ _ _ _ _) --> x
+[A,x] get' A 3 (l A _ _ x _ _ _ _ _ _) --> x
+[A,x] get' A 4 (l A _ _ _ x _ _ _ _ _) --> x
+[A,x] get' A 5 (l A _ _ _ _ x _ _ _ _) --> x
+[A,x] get' A 6 (l A _ _ _ _ _ x _ _ _) --> x
+[A,x] get' A 7 (l A _ _ _ _ _ _ x _ _) --> x
+[A,x] get' A 8 (l A _ _ _ _ _ _ _ x _) --> x
+[A,x] get' A 9 (l A _ _ _ _ _ _ _ _ x) --> x.
+
+def set' : A : Type -> ind -> (A -> A) -> list A -> list A.
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 1 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A (k x1) x2 x3 x4 x5 x6 x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 2 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 (k x2) x3 x4 x5 x6 x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 3 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 (k x3) x4 x5 x6 x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 4 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 (k x4) x5 x6 x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 5 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 (k x5) x6 x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 6 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 (k x6) x7 x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 7 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 (k x7) x8 x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 8 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 (k x8) x9)
+[A,k,x1,x2,x3,x4,x5,x6,x7,x8,x9] set' A 9 k (l A x1 x2 x3 x4 x5 x6 x7 x8 x9) --> (l A x1 x2 x3 x4 x5 x6 x7 x8 (k x9) ).
+
+
+def sudo : Type := list (list ind).
+
+def E : list ind := l ind X X X X X X X X X.
+def empty_sudo : sudo := l (list ind) E E E E E E E E E.
+
+
+def get : ind -> ind -> sudo -> ind.
+[i,j,s] get i j s --> (get' ind j (get' (list ind) i s)).
+
+def set : ind -> ind -> ind -> sudo -> sudo.
+[i,j,k,s] set i j k s --> set' (list ind) i (set' ind j (x => k)) s.
+
+
+def exists' : (ind -> bool) -> ind -> bool.
+[f  ] exists' f X --> F
+[f,i] exists' f i --> or (f i) (exists' f (S i)).
+
+def exists : (ind -> bool) -> bool := f => exists' f 1.
+
+
+
+def mem_line : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_line i j k s --> exists (i' => eq (get i' j s) k).
+
+def mem_col  : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_col i j k s --> exists (j' => eq (get i j' s) k).
+
+def mem_squ  : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_squ i j k s --> F.
+
+
+
+
+
+def mem_squ2  : ind -> ind -> ind -> sudo -> bool.
+[i,j,k,s] mem_squ2 i j k s -->
+  (i':ind =>
+   j':ind =>
+    (or (eq (get i'         j'         s) k)
+    (or (eq (get (S i')     j'         s) k)
+	(or (eq (get (S (S i')) j'         s) k)
+    (or (eq (get i'         (S j')     s) k)
+	(or (eq (get (S i')     (S j')     s) k)
+	(or (eq (get (S (S i')) (S j')     s) k)
+    (or (eq (get i'         (S (S j')) s) k)
+	(or (eq (get (S i')     (S (S j')) s) k)
+	    (eq (get (S (S i')) (S (S j')) s) k)))))))))
+  )
+  (trunc3 i) (trunc3 j).
+
+
+def check : ind -> ind -> ind -> sudo -> bool :=
+i => j => k => s =>
+     and (not (mem_line i j k s))
+   ( and (not (mem_col  i j k s))
+         (not (mem_squ  i j k s))).
+
+
+solution : Type.
+success : sudo -> solution.
+fail : solution.
+
+
+def iffail : solution -> solution -> solution.
+[x] iffail (success x) _ --> success x
+[d] iffail fail     d --> d.
+
+def solve : ind -> ind -> ind -> sudo -> solution.
+[i,s]     solve i X _ s --> solve (S i) 1 1 s.
+[  s]     solve X _ _ s --> success s.
+[i,j,s]   solve i j X s --> fail.
+[i,j,k,s] solve i j k s -->
+  ite solution
+    (eq (get i j s) X)
+    (ite solution
+      (check i j k s)
+      (iffail
+        (solve i (S j) 1 (set i j k s))
+        (solve i j (S k) s)
+      )
+      (solve i j (S k) s)
+    )
+    (solve i (S j) 1 s).
+
+
+def solve_sudo : sudo -> solution := s => solve 1 1 1 s.
+
+
+def extract_sol : solution -> sudo.
+[x] extract_sol (success x) --> x.
+
+
+
+def sol := solve_sudo empty_sudo.
+#EVAL sol.
+
+#EVAL[SNF,1] get 2 2 (extract_sol sol).
+#EVAL[SNF,2] get 2 2 (extract_sol sol).
+#EVAL[SNF,3] get 2 2 (extract_sol sol).
+
+#EVAL[WHNF,4] mem_squ2 2 2 3 (extract_sol sol).