coq - 合并匹配 Coq 中的重复案例

Question

这个问题我已经遇到过很多次了:我在 Coq 中有一个证明状态，它包括相等两边相同的匹配项。

是否有一种标准方法可以将多个匹配重写为一个？

例如。

match expression_evaling_to_Z with
    Zarith.Z0 => something
    Zartih.Pos _ => something_else
    Zarith.Neg _ => something_else
end = yet_another_thing.

如果我在 expresion_evaling_to_Z 上进行破坏，我会得到两个相同的目标。我想找到一种方法只获得一个目标。

Answer 1

标准解决方案是使用类型族定义数据类型的“ View ”，该类型族在析构时会引入适当的条件和情况。对于您的特定情况，您可以这样做:

Require Import Coq.ZArith.ZArith.

Inductive zero_view_spec : Z -> Type :=
| Z_zero  :                      zero_view_spec Z0
| Z_zeroN : forall z, z <> Z0 -> zero_view_spec z.

Lemma zero_viewP z : zero_view_spec z.
Proof. now destruct z; [constructor|constructor 2|constructor 2]. Qed.

Lemma U z : match z with
              Z0              => 0
            | Zpos _ | Zneg _ => 1
            end = 0.
Proof.
destruct (zero_viewP z).
Abort.

这是一些库(如 math-comp)中的常见习语，它为实例化类型族的 z 参数提供特殊支持。