这个问题我已经遇到过很多次了:我在 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
上进行破坏,我会得到两个相同的目标。我想找到一种方法只获得一个目标。
最佳答案
标准解决方案是使用类型族定义数据类型的“ 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
参数提供特殊支持。
关于coq - 合并匹配 Coq 中的重复案例,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/37514976/