我们可以禁止不符合条件的论点吗？

如何解决我们可以禁止不符合条件的论点吗？

我想部分派生输入为从属列表的函数。

deriveP出错，因为长度为EucAppend fk (pk ::: lk)的长度并不总是n，但是I总是期望长度为P的列表。

这是由于lastk和firstk的定义。 要解决此问题，lastk和firstk必须仅返回Euc k，而不返回Euc n。 我想禁止在k <= n和lastk中n和k不符合firstk的论点。

我不知道该怎么做。请告诉我。

这是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).

基本列表操作。

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部分派生功能。错误所在的地方是I (EucAppend fk (pk ::: lk))。

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).

解决方法

您可以如上所述处理订单关系。我的建议是避免在定义中使用证明（这会使证明更加复杂），例如：

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.

该定义是透明的，这使得在使用k n作为归纳点后易于证明。 vectodef库可与Fin types（有限序列）一起使用。您可以采取一种变通方法以使其轻松地提取定义：

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.

但是...，正如我所提到的，这在术语中有证明。

我认为您可能需要对deriveP的另一种证明，但我不知道Derive的定义，请考虑至少指定类型定义。