Coq证明中如何将公共match表达式赋值给nat类型变量简化目标

前置说明 #

我对Coq的专业术语尚不熟悉，因此会宽泛使用“expression（表达式）”“variable（变量）”这类表述，这些说法可能并非Coq中的标准术语。

我在证明某定理时遇到如下子目标：

1 goal
b : bag
v, b' : nat
b'' : natlist
B : b = b' :: b''
IHb'' : b = b'' -> count v (add v b'') = count v b'' + 1
______________________________________(1/1)
S match v =? b' with
  | true => S (count v b'')
  | false => count v b''
  end = match v =? b' with
        | true => S (count v b'')
        | false => count v b''
        end + 1

可暂时忽略目标中的S和+ 1部分，核心诉求是：等式两侧均出现了如下match表达式：

match v =? b' with
  | true => S (count v b'')
  | false => count v b''
end

我希望将该表达式赋值给一个nat类型的变量以简化证明，请问该如何实现？还是说必须对v和b'执行destruct分情况讨论，逐一证明所有分支？

你不需要强制采用分情况讨论的证明路径，Coq提供了专门的战术可以给重复出现的子表达式命名，直接简化证明目标：

• 使用set战术快速命名替换
  执行如下命令即可：

  set (e := match v =? b' with | true => S (count v b'') | false => count v b'' end).
  

  执行后Coq会自动将目标中所有和该match结构一致的子表达式替换为你命名的e（变量名可自定义），目标会直接简化为S e = e + 1，后续基于自然数加法的基本性质即可完成证明，无需展开分支。
• 使用remember战术保留命名等式
  如果担心替换后丢失原表达式的结构，可以使用remember战术：

  remember (match v =? b' with | true => S (count v b'') | false => count v b'' end) as e.
  

  执行后上下文会新增一条等式Heqe : e = <原match表达式>，目标中的对应子表达式同样会被替换为e，后续如果需要展开原表达式结构，直接执行rewrite Heqe即可。

针对你当前的具体子目标补充两点：

1. 哪怕不做命名替换，直接调用自然数运算相关的化简定理配合simpl战术，也可以直接完成证明；
2. 如果选择分情况讨论，不需要同时对v和b'两个变量做destruct，只需要对布尔表达式v =? b'的结果做分支拆分destruct (v =? b') eqn:Eq，两个分支下的目标都会自动化简为显然成立的等式。

内容的提问来源于stack exchange，提问作者Mathieu Borderé