Definition of equality among vectors

Question

I want to define equality among vectors.

The definition I thought of is that "two vectors are equal if and only if their types and all of their elements are equal".

So, I want to prove that my definition doesn't have a contradiction.

Require Import Psatz.
Require Import Coq.Vectors.Vector.

Definition kLess : forall (k P:nat), (P - k) < (S P).
intros. lia.
Defined.

Lemma aaa {n A}(v1 v2:t A (S n)): (forall k:nat, nth_order v1 (kLess k n) = nth_order v2 (kLess k n)) -> v1 = v2.
Proof.
intro IH.
induction n.
Abort.

I don't know what to do more.

Please tell me your methods.

Answer 1

Here is a proof.

Require Import Psatz.
Require Import Vectors.Vector.

Definition kLess : forall (k P:nat), (P - k) < (S P).
intros. lia.
Defined.

Lemma exists_kLess {n} (p: Fin.t (S n)):
  exists k : nat, p = Fin.of_nat_lt (kLess k n).
Proof.
  destruct (Fin.to_nat p) as [i Hi] eqn:Q.
  exists (n-i).
  apply Fin.to_nat_inj.
  rewrite Q.
  rewrite Fin.to_nat_of_nat.
  simpl.
  lia.
Qed.


Lemma aaa A: forall  n (v1 v2:t A (S n)), (forall k:nat, nth_order v1 (kLess k n) = nth_order v2 (kLess k n)) -> v1 = v2.
Proof.
  unfold nth_order.
  intros.
  apply Vector.eq_nth_iff.

  intros p p' Hp; subst p'.
  
  enough (exists k, p = Fin.of_nat_lt (kLess k n)) as [k  Hk].
  rewrite Hk. rewrite (H k). reflexivity.
  apply exists_kLess.
Qed.