Lean4中while_true_nonterm定理证明遇阻，求解决思路

你已经完成了IMP语言的语法和状态转移关系ceval的实现，现在要证明当循环条件恒为真时，while循环永不终止的while_true_nonterm定理，当前卡在E_WhileTrue分支的推导上。下面是具体的解决思路和完整证明：

核心思路 #

由于ceval是归纳定义的状态转移关系，证明这类"永不终止"的否定性结论，需要利用归纳法拆解ceval的推导结构——递归的while循环推导会被归纳假设覆盖，从而导出矛盾。

完整证明代码 #

theorem while_true_nonterm:
  ∀ (b : Bool) (c : com) (st st' : state),
  b = true → ¬(ceval (com.while b c) st st') := by
  intros b c st st' htrue
  -- 引入要否定的ceval推导，对其做归纳
  intro hceval
  induction hceval with
  -- 以下分支对应ceval的构造器，前5种构造器不可能对应while命令，直接矛盾
  | E_Skip => contradiction
  | E_Assign => contradiction
  | E_Seq => contradiction
  | E_IfTrue => contradiction
  | E_IfFalse => contradiction
  -- while条件为假的情况：和b=true的前提矛盾
  | E_WhileFalse hfalse =>
    rw[hfalse] at htrue
    contradiction
  -- while条件为真的情况：利用归纳假设导出矛盾
  | E_WhileTrue st'' htrue' hc hw ih =>
    -- 归纳假设ih：当b=true时，¬ceval (while b c) st' st''
    -- 而hw正好是ceval (while b c) st' st''，与ih矛盾
    exact ih htrue hw

关键步骤解释 #

1. 对ceval推导做归纳：直接针对hceval（即ceval (while b c) st st'的证明项）执行归纳，Lean会自动生成对应每个构造器的分支，以及递归情况的归纳假设。
2. 排除不可能的构造器：前5个构造器（skip、assign等）对应非while命令的推导，与当前要证明的while命令矛盾，直接用contradiction收尾。
3. E_WhileFalse分支：用hfalse（循环条件为假）替换前提中的b=true，直接得到矛盾。
4. E_WhileTrue分支：
   • 归纳假设ih给出了"在状态st'下，该while循环同样不会终止到st''"的结论。
   • 而当前分支中的hw正好是ceval (while b c) st' st''，与ih结合b=true的前提，直接导出矛盾，完成证明。

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