Definition of equality among vectors

user_10622059 0
Viewed 77

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.

coq
2 Answers

Apparently, there is a lemma missing about subtraction in the standard library. Here it is:

Lemma sub_sub_involutive n m : m <= n -> n - (n - m) = m.
Proof.
induction 1 as [ | n lemn Ih].
  now rewrite Nat.sub_diag, Nat.sub_0_r.
destruct m as [ | m].
  now rewrite Nat.sub_0_r, Nat.sub_diag.
rewrite (Nat.sub_succ_l (S m) n);[ | lia].
now rewrite Nat.sub_succ, Ih.
Qed.

With this lemma, you can follow the suggestion by @larsr in a comment. Here is my attempt.

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.
intros eqi; rewrite <- eq_nth_iff.
intros p1 p2 pp; rewrite <- pp; clear pp p2.
rewrite <- (Fin.of_nat_to_nat_inv p1).
destruct (Fin.to_nat p1) as [x lx]; cbn.
assert (xtosub : x = n - ( n - x)).
  now rewrite sub_sub_involutive;[ | lia]. 
revert lx; rewrite xtosub; intros lx.
rewrite (Fin.of_nat_ext lx (kLess _ _)).
apply eqi.
Qed.

An important trick happens at line 11 (revert lx). You need the rewrite on x to modify the comparison hypothesis too.

I believe you would be better off using the vectors and finite numbers as provided in the mathematical-components library.

user_18092110

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.
user_3042840
Related