I want to prove following lemma.
From mathcomp Require Import ssreflect.
Require Import Coquelicot.Coquelicot.
Lemma request_id {A}(a b:t R A): request a b = b.
Proof.
induction A.
refine (match b with nil => _ end) => //.
rewrite /request.
Abort.
The following processing is performed on all elements of a. I want to prove that it will be same as b when all processing is finished. a and b are vectors. i and k are indices. ∇a_i represents differentiation on a_i. ∑ represents sumation.
a_i - ∇a_i(∑(1/2)(a_k - b_k)^2)
k
How do you prove this with Coq?
Require Import Psatz.
Definition kLess : forall (k P:nat), (P - k) < (S P).
intros. lia.
Defined.
Theorem arith_basic : forall (k P:nat), lt k P -> P = Nat.add k (S (P - (k + 1))).
intros. lia.
Defined.
Definition k1Less : forall (k P:nat), ((S P)-((P-k)+1)) < (S P).
intros. lia.
Defined.
Definition kLess2 : forall (k P:nat), (P - k) <= (S P).
intros. lia.
Defined.
Require Import Coq.Reals.Reals.
Require Import Coq.Vectors.Vector.
Require Import Coquelicot.Coquelicot.
From mathcomp Require Import ssreflect.
Open Scope R_scope.
Open Scope vector_scope.
Notation "A ::: B" := (Vector.cons _ A _ B)(at level 60, right associativity).
Notation "[ r1 , .. , r2 ]" := (@cons R r1 _ .. ( @cons R r2 _ (@nil R) ) .. ).
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 (Vector.last v) (lastk m n (shiftout v) (@le_S_n _ _ H))
|0%nat => fun _ H => nil R
end
end.
Definition EucSum {A}(e:t R A) :R:= Vector.fold_right Rplus e 0.
Definition QE (r1 r2:R):R:= (1 / 2)*(r1 - r2)^2.
Definition QuadraticError {n : nat} (v1 v2: t R n) :t R n:= Vector.map2 QE v1 v2.
Definition deriveA {A}(k:nat)(a b:t R (S A)):R.
pose H := kLess k A.
apply arith_basic in H.
rewrite H in b.
pose lk := lastk ((S A)-((A-k)+1)) (S A) a (k1Less k A).
pose fk := take (A-k) (kLess2 k A) a.
pose ak := nth_order a (kLess k A).
exact ( Derive (fun AK => EucSum (QuadraticError (append fk (AK ::: lk)) b )) ak ).
Defined.
Fixpoint updateRnA {A} (k:nat)(a b:t R (S A)):t R (S k):=
match k in nat return t R (S k) with
|S k' => (nth_order a (kLess k A)) - (deriveA k a b) ::: updateRnA k' a b
|0%nat => [(Vector.last a) - (deriveA k a b)]
end.
Definition request {A} :t R A -> t R A -> t R A.
refine (match A with
| 0%nat => fun _ _ => nil R
| S A' => _
end).
intros a b.
exact (updateRnA A' a b).
Defined.