I want to prove lemma 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 holds and updateRnP is just recursion of deriveP. So I think RnP_eq must holds. but, I don't know how to prove it.
I need to do induction in n or p, but that changes type of function J and I can't apply the induction assumption to the goal.
Is it impossible to prove RnP_eq using Coq ?
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.
We need to do induction to prove equality of two vectors consist of the elements of two functions whose outputs are same.
In my question, we need to do induction in the vector which is the argument of the function of context. But, when I do that, the type of the function will change and I can't apply the assumption of induction to the goal.
For that reason, we cannot do induction in arguments of function whose type includes dependent type for fixed value. we cannot also do induction in fixed value of the dependent type.