6

在 Coq 中，我经常发现自己在做以下事情：我有证明目标，例如：

some_constructor a c d = some_constructor b c d

而且我真的只需要证明a = b，因为无论如何其他一切都是相同的，所以我这样做：

assert (a = b).

然后证明那个子目标，然后

rewrite H.
reflexivity.

完成证明。

但是，让那些在我的证明底部徘徊似乎只是不必要的混乱。

Coq 中是否有一个通用策略来获取构造函数的相等性并将其拆分为构造函数参数的相等性，有点像 asplit但用于等式而不是连词。

4

2 回答 2

4

您可以使用 Coq 的搜索功能：

  Search (?X _ = ?X _).
  Search (_ _ = _ _).

在一些噪音中，它揭示了一个引理

f_equal: forall (A B : Type) (f : A -> B) (x y : A), x = y -> f x = f y

以及它的多参数等式的兄弟姐妹：f_equal2... f_equal5（从 Coq 版本 8.4 开始）。

这是一个例子：

Inductive silly : Set :=
  | some_constructor : nat -> nat -> nat -> silly
  | another_constructor : nat -> nat -> silly.

Goal forall x y,
    x = 42 ->
    y = 6 * 7 ->
    some_constructor x 0 1 = some_constructor y 0 1.
  intros x y Hx Hy.
  apply f_equal3; try reflexivity.

在这一点上，你需要证明的是x = y。

于 2016-05-27T19:52:36.927 回答
3

特别是，标准 Coq 提供了这种f_equal策略。

Inductive u : Type := U : nat -> nat -> nat -> u.

Lemma U1 x y z1 z2 : U x y z1 = U x y z2.
f_equal

此外，ssreflect 提供了一种通用的一致性策略congr。

于 2016-05-28T09:40:00.087 回答