coq - 分解构造函数的相等性 coq

Question

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

some_constructor a c d = some_constructor b c d

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

assert (a = b).

然后证明子目标，然后

rewrite H.
reflexivity.

完成证明。

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

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

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 .