时间戳

首页 > 解决方案 > 不同的参数，但函数的行为是相同的

coq - 不同的参数，但函数的行为是相同的

问题描述

我想证明 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成立并且updateRnP只是 的递归deriveP。所以我认为RnP_eq必须成立。但是，我不知道如何证明。

我需要在 n 或 p 中进行归纳，但这会改变函数的类型，J我不能将归纳假设应用于目标。

RnP_eq用 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.

标签： coq

解决方案

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

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

出于这个原因，我们不能对类型包括固定值的依赖类型的函数的参数进行归纳。我们也不能对依赖类型的固定值进行归纳。

推荐阅读