Different arguments, but behavior of function is same

Question

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.

Presumably, you mean that func v a = J v (I [] a). I am having trouble seeing why this lemma should hold. It would help if you could simplify your code a bit. For instance, you could replace the definition of QuadraticError with a call to map2. I also have the impression that the dependent types are doing more harm than good here... — Arthur Azevedo De Amorim
I have known that I can do mutual conversion between vectors and lists using to_list and of_list. So, I should calculate after transforming vectors to lists. — Daisuke Sugawara
This is already better. But it would be even better if you rewrote deriveP to use plain lists instead of vectors. Then you won't have to reason about casts, which will make your statements much simpler. — Arthur Azevedo De Amorim
I will use firstn and skipn if I decide to rewrite deriveP to use plain lists. It is a problem that firstn and skipn don't always return the specified number of elements of the list. — Daisuke Sugawara

Daisuke Sugawara Daisuke Sugawara · Accepted Answer · 2020-10-31T03:54:19

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.

Different arguments, but behavior of function is same

1 Answers