Can we ban arguments that don't meet conditions?

I want to partially derive functions whose input is a dependent list.

deriveP has an error because EucAppend fk (pk ::: lk) of length is not always n, but I always expects a list whose length is P.

This is due to the definition of lastk and firstk. To solve this problem, lastk and firstk must return only Euc k, not Euc n. I want to ban arguments that n and k don't meet k <= n in lastk and firstk.

I don't know how to do it. Please tell me.

This is dependent list of R.

Require Import Coq.Reals.Reals.
Require Import Coquelicot.Coquelicot.

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).

Notation "[ ]" := RO.
Notation "[ r1 , .. , r2 ]" := (Rn r1 .. ( Rn r2 RO ) .. ).
Infix ":::" := Rn (at level 60, right associativity).

Basic list operation.

Definition head {n} (v : Euc (S n)) : R :=
  match v with
  | x ::: _ => x
  end.

Definition tail {n} (v : Euc (S n)) : Euc n :=
  match v with
  | _ ::: v => v
  end.

(* extract the last element *)   
Fixpoint last {n} : Euc (S n) -> R :=
  match n with
  | 0%nat => fun v => head v
  | S n => fun v => last (tail v)
  end.

(* eliminate last element from list *)
Fixpoint but_last {n} : Euc (S n) -> Euc n :=
  match n with
  | 0%nat => fun _ => []
  | S n => fun v => head v ::: but_last (tail v)
  end.
 
(* do the opposite of cons *)
Fixpoint snoc {n} (v : Euc n) (x : R) : Euc (S n) :=
  match v with
  | [] => [x]
  | y ::: v => y ::: snoc v x
  end.

(* extract last k elements *)
Fixpoint lastk k : forall n, Euc n -> Euc (Nat.min k n) := 
  match k with
  | 0%nat => fun _ _ => []
  | S k' => fun n =>
    match n return Euc n -> Euc (Nat.min (S k') n) with
    | 0%nat => fun _ => []
    | S n' => fun v =>
      snoc (lastk k' _ (but_last v)) (last v)
    end
  end.

(* extract first k elements *)
Fixpoint firstk k :forall n, Euc n -> Euc (Nat.min k n) :=
 match k with
 | 0%nat => fun _ _ => []
 | S k' => fun n =>
   match n return Euc n -> Euc (Nat.min (S k') n) with
   | 0%nat => fun _ => []
   | S n' => fun v => (head v) ::: firstk k' _ (tail v)
   end
 end.

(* extract nth element *)
(* 0 origine *)
Fixpoint EucNth (k:nat) :forall n, Euc (S n) -> R:=
 match k with
 | 0%nat => fun _ e => head e
 | S k' => fun n =>
   match n return Euc (S n) -> R with
   | 0%nat => fun e => head e
   | S n' => fun v => EucNth k' n' (tail v)
   end
 end.

Fixpoint EucAppend {n m} (e:Euc n) (f:Euc m) :Euc (n+m):=
 match e with
 |[] => f
 |e' ::: es => e' ::: (EucAppend es f)
 end.

deriveP partially derive fnctions. I (EucAppend fk (pk ::: lk)) is where the error is.

Definition deriveP {n A} (k:nat) (I:Euc n -> Euc A) (p :Euc n) :=
 let fk := firstk k P p in
 let lk := lastk (P-(k+1)) P p in
 (Derive (fun pk => I (EucAppend fk (pk ::: lk)) )) (EucNth k (P-1) p).

Solution

You can work with an order relation as you mentioned. My recommendation is to avoid proofs inside your definition (which makes proving after more complex), example :

Fixpoint lastk k n : Euc n -> k < n -> Euc k := 
  match n with
    |0 => fun _ (H : k < 0) => False_rect _ (Lt.lt_n_O _ H)
    |S n => match k with
              |S m => fun v H => snoc (lastk (but_last v) (le_S_n _ _ H)) (last v)
              |0 => fun _ H => []
            end
  end.


Fixpoint firstk k n : Euc n -> k < n -> Euc k := 
  match n with
    |0 => fun _ (H : k < 0) => False_rect _ (Lt.lt_n_O _ H)
    |S n => match k with
              |S m => fun v H => (head v) ::: firstk (tail v) (le_S_n _ _ H)
              |0 => fun _ H => []
            end
  end.

This definition is transparent which makes it easy to prove after using k n as inductions points. The vectodef library works with Fin types(finite sequences). You can do a workaround to make it comfortable to extract the definition :

Fixpoint of_nat {n} (x : t n) : nat := 
  match x with
     |@F1 _  => 0
     |@FS _ y => S (of_nat y)
  end.

Fixpoint lastk n (H : t n) (v : Euc n) : Euc (of_nat H) :=
 match H as t in (t n0) return (Euc n0 -> Euc (of_nat t)) with
   | @F1 n0 => fun=> [ ]
   | @FS n0 H1 =>
       fun H2 : Euc (S n0) => snoc (lastk H1 (but_last H2)) (last H2)
   end v.

Theorem of_nat_eq : forall y k (H : k < y), of_nat (of_nat_lt H) = k.
  intros y k.
  elim/@nat_double_ind : y/k.
  intros;inversion H.
  intros; auto.
  intros; simply.
  by rewrite -> (H (Lt.lt_S_n _ _ H0)).
Qed.
    
Definition last_leb n k (v : Euc n) : k < n -> Euc k.
 intros.
 rewrite <- (of_nat_eq H).
 exact (@lastk _ (of_nat_lt H) v).
 Show Proof.
Defined.

But..., as I mentioned this has proofs in the terms.

I think you probably will need another proof for deriveP, but I don't know the definition of Derive, please consider to specify at least the type definition.