合并匹配 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

你可以把match表达式写得更简洁：

match expression_evaling_to_Z with
  | Z0 => something
  | Zpos _ | Zneg _ => something_else
end = yet_another_thing.

但是在使用 destruct 时会给你 3 个子目标。

在这种特殊情况下，我们可能会使用这样一个事实，即您实际上需要区分零和非零情况，这看起来像是 Z.abs_nat : Z -> nat 函数的工作。

Require Import Coq.ZArith.BinIntDef.

match Z.abs_nat (expression_evaling_to_Z) with
  | O => something
  | S _ => something_else
end = yet_another_thing.

这只会让你得到两个子案例，但你需要在 Z.abs_nat (expression_evaling_to_Z) 上进行析构或引入一个新变量。如果您选择第一个变体，那么您可能需要 destruct (...) eqn:Heq. 将等式放入上下文中。

基本上，这种方法是关于寻找新的数据类型（或定义一个）和一个合适的函数来从旧类型映射到新类型。

Answer 2

标准解决方案是使用类型族定义数据类型的 "a 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 参数提供特殊支持。

Answer 3

如果您不介意打字，您可以使用 replace 将 RHS 替换为您目标的 LHS，这使得解决起来变得微不足道，然后您只需证明一次重写是确实可以。

Open Scope Z.
Lemma L a b :
  match a + b with
      Z0     => a + b
    | Zpos _ => b + a
    | Zneg _ => b + a
  end = a + b.
  replace (b+a) with (a+b). (* 1. replace the RHS with something trivially true *)
  destruct (a+b); auto.     (* 2. solve the branches in one fell swoop *)
  apply Z.add_comm.         (* 3. solve only once what is required for the two brances *)
Qed.

也许您可以使用一些 Ltac-fu 或其他引理来不必手动输入 RHS。

合并匹配 Coq 中的重复案例

Merge duplicate cases in match Coq

coq

coq-tactic