如何处理Coq证明中的匹配项

Question

我想知道什么样的策略来应对比赛。例如，我有以下形式的东西：

F match something m' with
  | true => Y m'
  | false => Z m'
  end=Otherside m'

[感觉应该有很多方法来解决这个问题……我想可能可以在上游重构某些东西来避免，但也应该满足以下条件

match something m' with
| true => F (Y m')
| false => F (Z m')
end=Otherside m'

然后您应该能够执行将其分成两个子目标的操作，如果有的话

F (Y m')=Otherside m'
F (Z m')=Otherside m'

那你去就好。

这可能吗？还是我需要重构我的功能？

Answer 1

这没有经过您的中间步骤，但是您只需达到以下两个目标即可

destruct (something m').

如果该术语太大而无法写，我想您可以像这样将其拔出：

match goal with |- _ match S with _ => _ end = _ => destruct S end.