3

我多次遇到这个问题：我在 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我会得到两个相同的目标。我想找到一种方法来实现其中一个目标。

4

3 回答 3

3

标准解决方案是使用类型族定义数据类型的“视图”，该类型族将在被破坏时引入适当的条件和案例。对于您的特定情况，您可以执行以下操作：

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类型族的参数提供了特殊支持。

于 2016-05-29T23:26:43.377 回答
2

您可以更简洁地编写match表达式：

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

但这会给你 3 个子目标destruct。

在这种特殊情况下，我们可能会使用这样一个事实，即您实际上需要区分零和非零情况，这看起来像是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.将方程式放入上下文中。

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

于 2016-05-29T22:01:03.620 回答
0

如果您不介意打字，您可以使用replace目标的 LHS 替换 RHS，这样解决起来很简单，然后您只需证明重写确实可以。

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。

于 2016-05-30T08:20:34.573 回答