如果Coq中两个归纳类型的构造函数表达式相等，是否可以根据它们的对应参数进行重写？

如何解决如果Coq中两个归纳类型的构造函数表达式相等，是否可以根据它们的对应参数进行重写？

我确实有一个四元组归纳类型，如下所示：

Inductive my_tuple :=
  | abcd : byte -> nat -> byte -> nat -> my_tuple.

在我的上下文中，我确实有以下内容：

H : abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2'

鉴于所有归纳类型的构造函数都是内射的且不相交的（也讨论过here），我想知道是否可以得出相应的参数相等（即b1 = b1'，{{ 1}}，n1 = n1'和b2 = b2'），然后使用它们重写其他证明我的方程式。如果是这样，我该怎么做？我已经看过这些帖子（here和there），但仍然不知道该怎么做。

谢谢您的任何评论。

解决方法

通常，注入非常简单，只有Coq自动化才能解决大多数简单情况。例如，在您的情况下，注入策略非常简单。

Theorem Injective_tuple : forall b1 n1 b2 n2 b1' n1' b2' n2',abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2' -> b1 = b1' /\ n1 = n1' /\ b2 = b2' /\ n2 = n2'.
  intros.
  injection H.
  intros.
  subst.
  do 4! constructor.
  Show Proof (*what actually coq is doing ? *).
Qed.

但是我假设您想了解以上定理中发生的事情。在这种情况下，...仍然非常简单。您可以看一下Coq生成的定理，基本上是：

(* A not so beautiful proof *)
Definition Raw_Injective_tuple b1 n1 b2 n2 b1' n1' b2' n2' :
  abcd b1 n1 b2 n2 = abcd b1' n1' b2' n2' -> b1 = b1' /\ n1 = n1' /\ b2 = b2' /\ n2 = n2' :=
    fun H => 
      let first := (f_equal (fun x => match x with
                       |abcd x _ _ _ => x
                    end) H) in
       let second := (f_equal (fun x => match x with
                       |abcd _ x _ _ => x
                     end) H) in
       let three := (f_equal (fun x => match x with
                       |abcd _ _ x _ => x
                     end) H) in
       let four := (f_equal (fun x => match x with
                       |abcd _ _ _ x => x
                     end) H) in conj first (conj second (conj three four)).

f_equal或全等式（如Agda）是一个定理，它说如果您有一个函数，则可以在等式两边应用，并且它将保留等式（x = y-> f x = f y）。好吧，如果您能够提取方程式两边的值，那么值相等并且函数为单射，在这种情况下，通过模式匹配就足够了。