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.