算法分析与设计大作业报告：水排序拼图
  
王维境 519120910046
  

    格式说明：文中具有 绿色边框 的内容为引用（外部链接），波浪线为重点标记。
  
  
数学模型和代码实现
  

    代码见附录压缩包。
  
  

    本实现采用 Lean 4 编程语言。
    这里必须要种草一波 Lean 4，Lean 是 Microsoft Research 旗下一门实验性编程语言，核心团队由 Leonardo de Moura
      (Microsoft)、Sebastian Ullrich (KIT) 等组成，拥有一大批活跃的社区维护者（也包括我:D）。Lean 是一门具有依赖类型系统的函数式编程语言，起源于计算机辅助证明（Formal" rel="nofollow">https://en.wikipedia.org/wiki/Proof_assistant">计算机辅助证明（Formal Proof,
      FP）和程序验证（Formal Verification, FV）的研究。事实上，在 Lean 3 时期，Lean
      就已经占据了两个领域的半壁江山，并且已经有许多相关的研究论文和代码实践（其中最出色的" rel="nofollow">https://leanprover-community.github.io">研究论文和代码实践（其中最出色的
      mathlib 工作形式化了当代数学的几乎所有主流领域）；而目前还处在 nightly 阶段的 Lean 4 致力于走向一门通用编程语言
    
    对于本门课算法设计来讲，Lean
      具有以下优势：（一）数学模型和数据结构合一，让编程回归数学，更加自然；（二）证明和算法合一，能够实现算法正确性、可终止性、复杂度等性质的形式化证明；（三）支持 Unicode
    符号，语法整洁清晰。编程环境的安装配置可以参见安装文档，为了方便运行我提供了">https://github.com/leanprover/lean4/blob/master/doc/setup.md">安装文档，为了方便运行我提供了 Dockerfile（见附件）可以直接运行为
    Docker 镜像。
  
  
运行方式
  

    运行方式如下：
  
  

cd <附件文件夹>

# 使用 本地环境
lake build          # lake 是 Lean 的包管理器
./build/bin/wsp     # 运行程序，用 `-h` flag 查看更多功能

# 使用 Docker
docker build -t wsp .
docker run -p 8080:8080 wsp

# 随后可以在浏览器内访问 http://localhost:8080 访问可视化前端
  

  

  
问题定义
  

    注：由于 Lean 数学和编程合一的优异性质，在这里我们可以直接用代码来描述数学模型：
  

  

    问题中给定 m 种颜色，则颜色可以用有限整数集 Fin m 来表示。采用 newtype 编程习惯，我们定义一个颜色类型 Color m：
  
  

abbrev Color (m : Nat) := Fin m
  

  

    一根试管的容量为 h，其中可以放入不同的 m 种颜色，最多可以放入容量为 h 的颜色。我们可以在 List 的基础上添加限制（liquid
    type）构造试管类型 Tube m h：
  
  

structure Tube (m h : Nat) where
  val : List (Color m)
  hVolume : val.length ≤ h  -- 试管容量限制的假设（hypothesis)
  

  

    总共 n 支试管组合可以认为是一个列表，定义为类型 Tubes m h n。其中还需要满足颜色完全假设
    colorComplete，即所有试管的各颜色加和的数量都为 h 的整数倍：
  
  

def colorComplete (tubes : List (Tube m h)) : Prop :=
  -- 在 Lean 中需要区分布尔 `Bool` 与命题 `Prop`，两者通过 `Decidable` typeclass 联系在一起
  let flattened := tubes.map Tube.val |>.join
  ∀ i : Fin m, (count i flattened) % h = 0    
where
  /-- 统计所有试管内某种颜色的数量 -/
  count i flattened :=
    flattened.foldl (λ acc x => acc + if x = i then 1 else 0) 0

structure Tubes (m h n : Nat) where
  val : List (Tube m h)
  hNum : val.length = n   -- 共有 n 个试管
  hColorComplete : colorComplete val  -- 试管所有颜色数量都为 h 的整数倍
  

  

    从而整个问题的初始条件也就可以给出，即初始的试管组合以及全满/全空的约束（省略了 ∈ 和 length 的定义，详见代码）：
  
  

structure PuzzleConfig (m h n : Nat) where
  initial : Tubes m h n
  k : Nat := 0  -- 空试管数量
  hFull : ∀ t, t ∈ initial → t.length = h
  

  

    解决这个问题的方式就是倾倒试管。倾倒的过程可以分解为三个字段（从哪倒？倒到哪？倒多少？），定义为类型 PourStep：
  
  

structure PourStep (n : Nat) where
  amount : Nat
  source : Fin n
  sink : Fin n
  

  

    则问题的解 Solution 和求解函数 solve 的类型定义就是：
  
  

structure Solution (n : Nat) where
  steps : List (PourStep n)
  k : Nat   -- 需要的空试管数量
  
def solve (config : PuzzleConfig m h n) : Solution n :=
  sorry
  

  

  
求解思路

  

    接下来拆解求解思路。
  

  
逐步增加空试管
  

    在最外层的 solve 函数中直接给出了需要的空试管的数量。我们可以先将问题简化为给定 k 空试管，是否有解；如果无解，则增添空试管即可。我们给出新的
    solveAux 函数，而原有的 solve 可以进一步细化：
  
  

def solveAux (config : PuzzleConfig m h n) : Option (Solution n) :=
  sorry

partial def solve (config : PuzzleConfig m h n) : Solution n :=
  match solveAux config with
  | some solution => solution
  | none => solve { config with k := config.k + 1 }
  

  

    这里我们暂时使用了 partial，即求解函数可能不终止（因为自然数 k 递增可能无穷多）。为了证明函数终止，一个直观的想法是：当空试管的数量多于 n
    个时，我们必然可以通过直接倒入对应空试管的方式来解决问题。
  
  

theorem solveAux_k_ge_n : config.k ≥ n → (solveAux config).isSome :=
  sorry