我在 中使用标准向量类型Coq.Vectors。我想证明关于 的以下属性shiftin。
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.
<-很简单。
-> a0 = a1没问题。但我对 一无所知-> t0 = t1。
第 2 部分 （已添加）：
编辑：此部分现在作为单独的问题提出：
shiftin、shiftout 和 last
同时，如果向量长度至少为 1，是否有可能证明last和shiftout是的有效反转？shiftin
Lemma shiftin_last_shiftout:
forall A (n:nat) (x: t A (S n)),
x = shiftin (last x) (shiftout x).