Coq.Vectors中shiftin的等式性质证明及相关疑问

右向证明中，当你已得到shiftin a0 t0 = shiftin a1 t1且证得a0 = a1后，有两种常用方法证明t0 = t1：

方法一：利用injection tactic #

shiftin本质是向量的cons构造子，而Coq中构造子具备单射性。直接对等式shiftin a0 t0 = shiftin a1 t1使用injection tactic，会同时生成a0 = a1和t0 = t1两个等式，提取第二个即可完成证明。

对应证明片段：

intros H.
split.
(* 你已完成的a0 = a1证明 *)
injection H as H0. exact H0.
(* 证明t0 = t1 *)
injection H as _ H1. exact H1.

方法二：利用向量的tail函数 #

1. 先证明tail与shiftin的关联引理：对于任意元素a和向量t，tail (shiftin a t)就是t本身：

Lemma tail_shiftin : forall A n (a:A) (t:t A n), tail (shiftin a t) = t.
Proof. reflexivity. Qed.

2. 在已有a0 = a1（记为H0）和shiftin a0 t0 = shiftin a1 t1（记为H）的前提下：
   • 用rewrite H0 in H将等式中的a1替换为a0，得到shiftin a0 t0 = shiftin a0 t1；
   • 对等式两边应用tail函数（用f_equal tail），得到tail (shiftin a0 t0) = tail (shiftin a0 t1)；
   • 用tail_shiftin引理替换两边，即可得到t0 = t1。

对应证明片段：

intros H.
split.
(* 你已完成的a0 = a1证明 *)
injection H as H0. exact H0.
(* 证明t0 = t1 *)
rewrite H0 in H.
apply f_equal with (f := tail A n) in H.
rewrite !tail_shiftin in H.
exact H.

完整证明脚本 #

Require Import Vectors.Vector.

Lemma tail_shiftin : forall A n (a:A) (t:t A n), tail (shiftin a t) = t.
Proof. reflexivity. Qed.

Lemma vec_shiftin_eq:
  forall A (n:nat) (a0 a1: A) (t0 t1: t A n),
  shiftin a0 t0 = shiftin a1 t1 <-> a0 = a1 /\ t0 = t1.
Proof.
  split.
  - intros [H0 H1]. rewrite H0, H1. reflexivity.
  - intros H.
    split.
    + injection H as H0. exact H0.
    + injection H as _ H1. exact H1.
Qed.

内容的提问来源于stack exchange，提问作者KingsAlpaca