Lean中使用cases tactic拆分归纳类型未生成等式假设如何解决

解决方案 #

你可以通过以下两种方式获取c = 对应构造子的等式假设：

• 为cases tactic添加显式的等式绑定：将cases c替换为cases h : c，执行后每个分支都会自动生成名为h的假设，内容就是当前分支下变量和对应构造子的等式。
  示例代码如下：

  inductive color | blue | red
  
  theorem exmpl (c : color) : true :=
  begin
      cases h : c,
      -- color.blue分支上下文：h : c = color.blue
      -- color.red分支上下文：h : c = color.red
      all_goals trivial
  end
  

• 使用cases' tactic（Lean 4原生支持，Lean 3需导入对应tactic扩展库），语法为cases' c with h，也会在对应分支自动生成绑定的等式假设。

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