如何在Coq中应用公理化简match匹配以完成证明？

结论 #

完全可以使用foo_is_valid公理消除match匹配完成证明，操作逻辑非常直接：你当前的证明目标是对foo x做模式匹配的分支结果，而公理已经明确给出了foo x的固定取值，只需要重写替换后即可自动化简目标。

具体操作步骤 #

• 第一步：执行rewrite foo_is_valid.
  该策略会用公理中的等式foo x = Some true，将目标中的foo x替换为Some true，Coq会自动化简match匹配，此时证明目标变为：

  x : nat
  
  ========================= (1 / 1)
  True
  

• 第二步：执行trivial或者constructor策略即可完成证明，这两个策略都可以直接证明恒真命题True。

完整证明脚本 #

Lemma foo_some_is_true_for_real : forall {x : nat}, foo_valid x.
  cbv.
  intros.
  rewrite foo_is_valid.
  trivial.
Qed.

也可以用精简写法一步完成重写加证明：

Lemma foo_some_is_true_for_real : forall {x : nat}, foo_valid x.
  cbv. intros. now rewrite foo_is_valid.
Qed.

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