# Library CoLoR.Util.Vector.VecOrd

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Frederic Blanqui, 2005-01-24

# Component-wise extension of a relation to vectors and product ordering

Set Implicit Arguments.

# Component-wise extension to vectors on A of a relation on A.

Fixpoint Vrel1 n A (R : relation A) : relation (vector A n) :=
match n with
| O => fun _ _ => False
| S n => fun v1 v2 => symprod R (Vrel1 R) (Vhead_tail v1) (Vhead_tail v2)
end.

Definition Vrel1_app n A (R : relation A) : relation (vector A n) :=
fun v1 v2 : vector A n =>
exists i (vi : vector A i) x j (vj : vector A j) h y,
v1 = Vcast (Vapp vi (Vcons x vj)) h
/\ v2 = Vcast (Vapp vi (Vcons y vj)) h /\ R x y.

Definition Vrel1_nth n A (R : relation A) : relation (vector A n) :=
fun v1 v2 : vector A n =>
exists i (hi : i<n), R (Vnth v1 hi) (Vnth v2 hi)
/\ forall j (hj : j<n), j <> i -> Vnth v1 hj = Vnth v2 hj.

Properties of Vrel1.

Section S.

Variables (A : Type) (R : relation A).

Lemma Vrel1_cons_intro : forall x1 x2 n (v1 v2 : vector A n),
(R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2)
-> Vrel1 R (Vcons x1 v1) (Vcons x2 v2).

Lemma Vrel1_cons_elim : forall x1 x2 n (v1 v2 : vector A n),
Vrel1 R (Vcons x1 v1) (Vcons x2 v2) ->
(R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2).

Lemma Vrel1_add_intro : forall x1 x2 n (v1 v2 : vector A n),
(R x1 x2 /\ v1 = v2) \/ (x1 = x2 /\ Vrel1 R v1 v2)
-> Vrel1 R (Vadd v1 x1) (Vadd v2 x2).

Lemma Vrel1_app_intro_l : forall n (v : vector A n) m (v1 v2 : vector A m),
Vrel1 R v1 v2 -> Vrel1 R (Vapp v v1) (Vapp v v2).

Lemma Vrel1_cast_intro : forall m n (h : m=n) (v1 v2 : vector A m),
Vrel1 R v1 v2 -> Vrel1 R (Vcast v1 h) (Vcast v2 h).

Lemma Vrel1_cast_elim : forall m n (h : m=n) (v1 v2 : vector A m),
Vrel1 R (Vcast v1 h) (Vcast v2 h) -> Vrel1 R v1 v2.

Equivalence between Vrel1 and Vrel1_app.

Lemma Vrel1_app_impl : forall n (v1 v2 : vector A n),
Vrel1 R v1 v2 -> Vrel1_app R v1 v2.

Lemma Vrel1_app_iff : forall n (v1 v2 : vector A n),
Vrel1 R v1 v2 <-> Vrel1_app R v1 v2.

Lemma Vrel1_app_eq n : @Vrel1 n _ R == @Vrel1_app n _ R.

Equivalence between Vrel1 and Vrel1_nth.

Lemma Vrel1_nth_iff : forall n (v1 v2 : vector A n),
Vrel1 R v1 v2 <-> Vrel1_nth R v1 v2.

Lemma Vrel1_sub : forall n (v1 v2 : vector A n) p q (h : p+q<=n),
Vrel1 R v1 v2 -> (Vrel1 R)% (Vsub v1 h) (Vsub v2 h).

Properties of Vrel1 wrt termination.

Lemma Vforall_SN_rel1 : forall n (v : vector A n),
Vforall (SN R) v -> SN (Vrel1 R) v.

Lemma SN_rel1_head : forall n (v : vector A (S n)),
SN (Vrel1 R) v -> SN R (Vhead v).

Lemma SN_rel1_cons_head : forall a n (v : vector A n),
SN (Vrel1 R) (Vcons a v) -> SN R a.

Lemma SN_rel1_tail : forall n (v : vector A (S n)),
SN (Vrel1 R) v -> SN (Vrel1 R) (Vtail v).

Lemma SN_rel1_cons_tail : forall a n (v : vector A n),
SN (Vrel1 R) (Vcons a v) -> SN (Vrel1 R) v.

Lemma SN_rel1_forall : forall n (v : vector A n),
SN (Vrel1 R) v -> Vforall (SN R) v.

End S.

Compatibility of Vrel1 with inclusion and same.

Instance Vrel1_app_incl n A :
Proper (inclusion ==> inclusion) (@Vrel1_app n A).

Instance Vrel1_incl n A : Proper (inclusion ==> inclusion) (@Vrel1 n A).

Instance Vrel1_app_same n A :
Proper (same ==> same) (@Vrel1_app n A).

Instance Vrel1_same n A : Proper (same ==> same) (@Vrel1 n A).

Distributivity of Vrel1 wrt union.

Lemma Vrel1_app_union n A (R S : relation A) :
@Vrel1_app n _ (R U S) == @Vrel1_app n _ R U @Vrel1_app n _ S.

Lemma Vrel1_union n A (R S : relation A) :
@Vrel1 n _ (R U S) == @Vrel1 n _ R U @Vrel1 n _ S.