coq - 向量：关于分割和附加向量的定理

Question

我想证明下面的引理。

Require Import Coq.Vectors.Vector.

Lemma t (A:Type)(n:nat)(v:t A (n+0)): fst (splitat n v) ++ (nil A) = v.
Proof.
induction n.
refine (match v with (nil _) => _ end).
reflexivity.
remember (splitat (S n) v).
Abort.

我如何教 Coqfst (splitat n v)与 v 相同？

标签： coq

Answer 1

我找到了更简单的证据。

Lemma l (A:Type)(n:nat)(v:t A (n+0)): fst (splitat n v) ++ (nil A) = v.
Proof.
induction n.
refine (match v with Vector.nil _ => _ end).
reflexivity.
simpl.
rewrite (surjective_pairing (splitat n (Vector.tl v))).
simpl.
rewrite (IHn (tl v)).
rewrite <- eta.
reflexivity.
Qed.