coq - 如何通过等式证明进行推理？

Question

假设我对加法的定义略有不同，对向量附加的定义也略有不同:

From Coq Require Import Vector.

Definition myAddNat a b := nat_rect _ b (fun _ p => S p) a.

Theorem rewrite_myAddNat a b : myAddNat a b = (a + b)%nat.
Proof.
  induction a.
  { reflexivity. }
  {
    simpl.
    congruence.
  }
Defined.

Definition myAppend T m n : Vector.t T m -> Vector.t T n -> Vector.t T (myAddNat m n).
  rewrite rewrite_myAddNat.
  apply Vector.append.
Defined.

我希望能够证明以下内容:

Theorem myAppend_cons_1 T m n h a b :
    myAppend T (S m) n (cons T h m a) b =
    cons T h (myAddNat m n) (myAppend T m n a b).
Proof.
  induction a.
  { reflexivity. }
  {
    simpl.
    unfold myAppend.
    (* stuck! *)
  }
Abort.

我最终陷入了两个非常接近的术语上，除了它们各自在不同的位置上有一个相等的转换，我不知道如何处理。

我考虑将定理陈述更改为:

Theorem myAppend_cons T m n h a b :
    existT _ _ (myAppend T (S m) n (cons T h m a) b) =
    existT _ _ (cons T h (myAddNat m n) (myAppend T m n a b)).

以便能够暂时让方程两边有不同的类型，但一直没能在证明上取得更大的进展。

所以:

1)有没有一个好方法来证明任一定理

或者，

2) 我应该以不同的方式编写 myAppend 以使我的生活更轻松吗？

Answer 1

这是一个快速回答:

Theorem myAppend_cons_1 T m n h a b :
    myAppend T (S m) n (cons T h m a) b =
    cons T h (myAddNat m n) (myAppend T m n a b).
Proof.
  unfold myAppend, eq_rect_r; simpl.
  rewrite !eq_trans_refl_l, !eq_sym_map_distr.
  now destruct (eq_sym _).
Qed.