分解Coq构造函数的相等性

Question

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

some_constructor a c d = some_constructor b c d

而实际上，我只需要证明a = b，因为其他所有东西都是相同的，因此我这样做：

assert (a = b).

那么证明子目标，然后。

rewrite H.
reflexivity.

完成证明。

但是，在我的证明底部留下那些东西似乎只是不必要的杂物。

在Coq中，是否有一般策略将构造函数的相等性分解为构造函数参数的相等性，有点像对等式进行split，而不是合取。

- k_g

---

相关链接：https://stackoverflow.com/q/50117934/1544337 - user1544337

Answer 1

您可以使用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即可。

- Anton Trunov

---

是的，构造函数是可逆函数，这就是为什么这种方法总是有效的原因。而且 f_equal 可以应用于每个可逆函数。还有一种名为 injection 的策略可以用于 假设。更多信息请参见此处。 - Anton Trunov

当然，f_equal 可以应用于任何相关形式的相等性。但是如果一个函数是单射的，它保证你不会丢失信息（这在后面可能会有用）。例如，Goal Z.abs 1 = Z.abs (-1). apply f_equal. "可以工作"，但是留下了 1 = -1 作为目标，因为 Z.abs 显然不是单射的。 - Anton Trunov

@ejgallego 是的，完全正确。如果 f（在 OP 中是 some_constructor）是单射的话，我们可以总是应用 f_equal 来证明目标，因为你上面提到的单射条件。但对于任意函数来说通常情况下并非如此（正如我在之前的评论中所示）。总之：我谈论的是一个充分条件，而不是必要条件。 - Anton Trunov

@AntonTrunov，嗯，我不确定这是正确的。例如，为了从适当的假设证明S 3 = S 4，应用f_equal是一个不必要的步骤。 - ejgallego

@ejgallego 很好的观点，但我并没有说我们总是必须这样做 ;) - Anton Trunov

Answer 2

特别地，标准的Coq提供了策略。

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。

- ejgallego

---

在我看来，策略“f_equal”通常会产生比仅使用“apply f_equal”更复杂的术语。 - eponier