在Coq中及通用场景下，证明数独、Takuzu解谜函数正确性的步骤

通用证明流程 #

不管是数独、Takuzu还是其他逻辑解谜问题，在Coq中证明求解函数的正确性都遵循以下核心步骤：

1. 形式化问题的约束与合法解 #

首先必须用Coq的类型系统精确定义什么是合法解，以及谜题（部分填充状态）和解之间的一致性：

• 用归纳类型表示单个格子的状态（空、数字/符号）。
• 用记录类型定义合法解的所有约束（比如数独的行/列/宫无重复，Takuzu的0/1数量相等、无三连相同元素）。
• 定义一致性谓词：确保解的已填格子完全匹配原谜题的对应位置。

2. 明确求解函数的类型与实现 #

• 求解函数的输入是谜题，输出建议用option类型（Some sol表示找到解，None表示无解）；如果要返回所有解则用列表类型。
• 实现逻辑要清晰：比如回溯法、约束传播+回溯，递归结构要便于后续用归纳法证明。

3. 拆分核心性质并逐一证明 #

正确性（Soundness）

证明：如果函数返回Some sol，那么sol一定是合法解，且与原谜题一致。

• 针对递归实现，用结构归纳法或基于空单元格数量的归纳法。
• 递归基：当谜题无空单元格时，验证函数的正确性要单独证明（即验证通过的状态确实满足所有约束）。
• 递归步骤：证明每一步填充/传播操作都不会破坏合法性，且递归调用的正确性能推导出当前步骤的正确性。

完整性（Completeness）

证明：如果谜题存在合法解，函数必然能返回至少一个解（不会返回None）。

• 同样用归纳法，基于空单元格数量或解空间的大小。
• 核心是证明求解过程不会遗漏合法路径：比如回溯会尝试所有合法的填充值，约束传播不会排除任何合法解。

唯一性（可选）

如果问题保证唯一解，证明函数返回的解是唯一的合法解：

• 结合正确性和完整性，加上问题的唯一性约束，推导函数返回的解与所有合法解相等。

4. 复用引理简化证明 #

提取通用的辅助引理（比如“填充合法值后的谜题的解与原谜题解一致”），用rewrite、auto等策略减少重复劳动，提升证明效率。

数独的具体证明步骤 #

1. 形式化数独的数据结构与约束 #

Inductive Cell : Type := Empty | Num (n : nat) where "n" := (Num n) : nat_scope.
Definition SudokuPuzzle := array (array Cell) (9*9).

Record SudokuSolution : Type := {
  sol_cells : array (array nat) (9*9);
  sol_valid_rows : forall r, NoDup (row r sol_cells);  (* 行无重复 *)
  sol_valid_cols : forall c, NoDup (col c sol_cells);  (* 列无重复 *)
  sol_valid_boxes : forall b, NoDup (box b sol_cells); (* 3x3宫无重复 *)
  sol_filled : forall i j, sol_cells[i][j] <> 0        (* 无空单元格 *)
}.

Definition consistent (p : SudokuPuzzle) (sol : SudokuSolution) : Prop :=
  forall i j, match p[i][j] with
              | Empty => True
              | Num n => sol_cells sol i j = n
              end.

2. 实现回溯法求解函数 #

Fixpoint sudoku_backtrack (p : SudokuPuzzle) : option SudokuSolution :=
  match find_empty_cell p with
  | None => if verify_sudoku p then Some (build_solution p) else None
  | Some (i,j) => 
      fold_left (fun acc n => 
                   match acc with
                   | Some _ => acc
                   | None => sudoku_backtrack (fill_cell p i j (Num n))
                   end) (seq 1 9) None
  end.

其中find_empty_cell找第一个空单元格，fill_cell填充指定位置，verify_sudoku验证填满的谜题是否符合约束。

3. 证明核心性质 #

正确性证明

目标：forall p sol, sudoku_backtrack p = Some sol -> consistent p sol /\ valid_solution sol

• 归纳基：当无空单元格时，verify_sudoku返回true当且仅当谜题是合法解，直接引用verify_sudoku的正确性引理。
• 递归步骤：假设填充数字n后的谜题调用返回合法解，那么原谜题的解与填充后的谜题解一致（因为填充的是空单元格），且满足所有约束（填充的n符合行/列/宫的无重复要求）。

完整性证明

目标：forall p, (exists sol, consistent p sol /\ valid_solution sol) -> sudoku_backtrack p <> None

• 归纳基：如果谜题本身是合法解，verify_sudoku返回true，函数返回Some sol。
• 递归步骤：假设存在解sol，找到空单元格(i,j)，sol在该位置的数字n必然是1-9中的一个，填充后递归调用根据归纳假设返回Some sol，因此外层函数也返回该解。

Takuzu的具体证明步骤 #

1. 形式化Takuzu的数据结构与约束 #

Inductive TakuzuCell : Type := TEmpty | T0 | T1.
Definition TakuzuPuzzle (n : nat) := array (array TakuzuCell) (n*n).

Record TakuzuSolution (n : nat) : Type := {
  t_sol_cells : array (array bool) (n*n);
  t_eq_count : forall r, count_true (row r t_sol_cells) = n/2; (* 0/1数量相等 *)
  t_no_three_consec : forall r, no_three_consec (row r t_sol_cells); (* 无三连相同 *)
  t_no_dup_rows : NoDup (map row (all_rows t_sol_cells)); (* 无重复行 *)
  t_no_dup_cols : NoDup (map col (all_cols t_sol_cells)); (* 无重复列 *)
  t_filled : forall i j, t_sol_cells[i][j] <> TEmpty
}.

Definition t_consistent (n : nat) (p : TakuzuPuzzle n) (sol : TakuzuSolution n) : Prop :=
  forall i j, match p[i][j] with
              | TEmpty => True
              | T0 => t_sol_cells sol i j = false
              | T1 => t_sol_cells sol i j = true
              end.

2. 实现约束传播+回溯的求解函数 #

Fixpoint takuzu_solve (n : nat) (p : TakuzuPuzzle n) : option (TakuzuSolution n) :=
  let p' := propagate_takuzu_constraints n p in
  match find_empty_cell p' with
  | None => if verify_takuzu n p' then Some (build_takuzu_solution n p') else None
  | Some (i,j) => 
      match get_possible_values n p' i j with
      | [] => None
      | vs => fold_left (fun acc v => 
                           match acc with
                           | Some _ => acc
                           | None => takuzu_solve n (fill_takuzu_cell p' i j v)
                           end) vs None
      end
  end.

propagate_takuzu_constraints会补全必须填充的格子（比如某行已有n/2个0，剩下填1；两个连续0旁必须填1），get_possible_values返回当前单元格的合法候选值。

3. 证明核心性质 #

正确性证明

目标：forall n p sol, takuzu_solve n p = Some sol -> t_consistent n p sol /\ valid_takuzu_solution n sol

• 先证明约束传播的正确性：propagate_takuzu_constraints不会引入矛盾，且传播后的谜题的解与原谜题解一致。
• 再用归纳法证明回溯步骤的正确性：填充的候选值都是符合约束的，递归调用的正确性推导当前步骤的正确性。

完整性证明

目标：forall n p, (exists sol, t_consistent n p sol /\ valid_takuzu_solution n sol) -> takuzu_solve n p <> None

• 证明约束传播是完备的：原谜题的解也是传播后谜题的解。
• 归纳步骤：存在解sol时，传播后的谜题的空单元格的候选值包含sol中的值，填充后递归调用返回解，因此外层函数返回该解。

内容的提问来源于stack exchange，提问作者Lepticed