参数不同，但是功能的行为相同

如何解决参数不同，但是功能的行为相同

我想证明引理RnP_eq。

From mathcomp Require Import ssreflect.
Require Import Coq.Program.Equality.

Definition func {n m l o:nat}
     (I:t R 0 -> t R m -> t R l)(J:t R n -> t R l -> t R o):=
 (fun (x:t R n)(a:t R m) => J (snd (splitat 0 x)) (I (fst (splitat 0 x)) a)).

Lemma deriveP_eq (n m l o:nat)(v:t R (S n))
                 (I:t R 0 -> t R m -> t R l)(J:t R (S n) -> t R l -> t R o)
                 (a:t R m)(b:t R o):
 forall m:nat,deriveP m (func I J) v a b = deriveP m J v (I Vnil a) b.
Proof.
by [].
Qed.

Lemma RnP_eq (n m l o P:nat)
          (I:t R 0 -> t R m -> t R l)(J:t R (S n) -> t R l -> t R o)
          (p:t R (S n))(a:t R m)(b:t R o):
           updateRnP n (func I J) p a b = updateRnP n J p (I Vnil a) b.
Proof.
dependent induction p => //.
destruct n => //.
rewrite /=.
rewrite (deriveP_eq _ _ _ _ _ _ (J)).
f_equal.
Abort.

deriveP_eq成立，updateRnP只是deriveP的递归。因此，我认为RnP_eq必须成立。但是，我不知道如何证明。

我需要用n或p进行归纳，但这会改变函数J的类型，因此我无法将归纳假设应用于目标。

是否可以使用Coq证明RnP_eq？

Require Import Psatz.

Theorem arith_basic : forall (k P:nat),lt k P -> P = Nat.add k (S (P - (k + 1))).
  intros. lia.
Defined.

Definition kLess : forall (k P:nat),(P - k) < (S P).
intros. lia.
Defined.

Definition kLess2 : forall (k P:nat),(P - k) <= (S P).
intros. lia.
Defined.

Definition k1Less : forall (k P:nat),((S P)-((P-k)+1)) < (S P).
intros. lia.
Defined.

From mathcomp Require Import ssreflect.
Require Import Coq.Reals.Reals.
Require Import Coq.Vectors.Vector.
Require Import CoLoR.Util.Vector.VecUtil.
Require Import Coquelicot.Coquelicot.
Require Import Coq.Classes.RelationClasses.
Import VectorNotations.
Require Import Coq.Logic.FunctionalExtensionality.
Open Scope vector_scope.

Infix ":::" := (Vcons)(at level 60,right associativity).

Fixpoint lastk k n : t R n -> (lt k n) -> t R k :=
  match n with
    |0%nat => fun _ (H : lt k 0) => False_rect _ (@Lt.lt_n_O k H)
    |S n => match k with
              |S m => fun v H => shiftin (last v) (lastk m n (shiftout v) (@le_S_n _ _ H))
              |0%nat => fun _ H => Vnil
            end
  end.

Definition EucSum {A}(e:t R A) :R:= Vector.fold_right Rplus e 0.
Definition QE (r1 r2:R):R:= (r1 - r2)^2.
Definition QuadraticError {n : nat} (v1 v2: t R n) :t R n:= Vector.map2 QE v1 v2.

Definition deriveP {P A B}(k:nat)(I:t R (S P) -> t R A -> t R B)(p :t R (S P))(input:t R A)(train:t R B):R:=
let lk := lastk ((S P)-((P-k)+1)) (S P) p (k1Less k P) in
let fk := take (P-k) (kLess2 k P) p in
let pk := nth_order p (kLess k P) in
(nth_order p (kLess k P)) - 0.01*( Derive (fun PK => EucSum (QuadraticError 
   (I (Vcast (append fk (PK ::: lk)) (symmetry (arith_basic (P-k) (S P) (kLess k P)))) input) train)) pk ).

Fixpoint updateRnP {P A B} (k:nat)(I:t R (S P) -> t R A -> t R B)
                           (p :t R (S P))(input:t R A)(train:t R B):t R (S k):=
 match k in nat return t R (S k) with
   |S k' => (deriveP k I p input train) ::: updateRnP k' I p input train
   |0%nat => (deriveP k I p input train) ::: Vnil
   end.

解决方法

我们需要进行归纳以证明两个向量的相等性是由两个输出相同的函数的元素组成。

在我的问题中，我们需要对向量进行归纳，这是上下文函数的参数。但是，当我这样做时，函数的类型将会改变，并且我不能将归纳假设应用于目标。

因此，我们无法对类型为固定值的依赖类型的函数参数进行归纳。我们也不能对依赖类型的固定值进行归纳。