Library CoLoR.Util.Vector.NaryFunction

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Sebastien Hinderer, 2004-04-02
basic definitions on functions taking Vector.ts as arguments

Set Implicit Arguments.

Section S.

Require Import RelUtil.

Variables A : Type.

Require Import VecUtil.

Notation vec := (Vector.t A).

Definition naryFunction n := vec nA.

Variables (n : nat) (f : naryFunction n).

Definition Vmonotone_i (R : relation A) i j (H : i + S j = n) :=
vi vj, monotone R (fun zf (Vcast (Vapp vi (Vector.cons z vj)) H)).

Implicit Arguments Vmonotone_i [i j].

Lemma Vmonotone_i_transp : R i j (H : i + S j = n),
Vmonotone_i R HVmonotone_i (transp R) H.

Proof.
unfold Vmonotone_i. intros R i j H H' vi vj. apply monotone_transp. apply H'.
Qed.

Definition Vmonotone R := i j (H : i + S j = n), Vmonotone_i R H.

Lemma Vmonotone_transp : R : relation A,
Vmonotone RVmonotone (transp R).

Proof.
unfold Vmonotone. intros R H i j H'. apply Vmonotone_i_transp. apply H.
Qed.

End S.

Implicit Arguments Vmonotone_i [A n i j].

Section preserv.

Variables (A : Type) (P : AProp) (n : nat) (f : naryFunction A n).

Definition preserv := v, Vforall P vP (f v).

Definition restrict (H : preserv) : naryFunction (sig P) n :=
fun vexist P (f (Vmap (@proj1_sig _ _) v)) (H _ (Vforall_of_vsig v)).

End preserv.