Set Implicit Arguments.

Section S.

Require Import RelUtil.

Variables A : Type.

Require Import VecUtil.

Notation vec := (Vector.t A).

Definition naryFunction n := vec n → A.

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

Definition Vmonotone_i (R : relation A) i j (H : i + S j = n) :=
  ∀ vi vj, monotone R (fun z ⇒ f (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 H → Vmonotone_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 R → Vmonotone (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 : A→Prop) (n : nat) (f : naryFunction A n).

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

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

End preserv.