在 Coq 上转换离开先前状态的引理

Question

我想部分派生输入为从属列表的函数。

我试图通过证明来定义deriveP。

Derive 是 Coquelicot.Derive.

中的函数

Definition deriveP {P A B}(k:nat)(I:Euc (S P) -> Euc A -> Euc B)
                             (input:Euc A)(train:Euc B)(p :Euc (S P)) 
                              :(lt k (S P)) -> (lt ((S P)-(k+1)) (S P)) -> R.
intros.
pose fk := firstk k (S P) p H.
pose lk := lastk ((S P)-(k+1)) (S P) p H0.
pose pk := EucNth k p.
apply arith_basic in H.
exact ( Derive (fun PK => EucSum (QuadraticError (I (fk +++ (PK ::: lk)) input) train )) pk ).

我不能应用arith_basic Tiago提出的，因为fk中使用了H。我可以在制作 fk 之前将 arith_basic 应用于 H，但之后我无法制作 fk，因为没有 k < P.+1.

我想在离开 k < P.+1 时将 arith_basic 应用到 H。

请帮帮我。

(******************************************** ***************)

这是R的依赖列表

Require Import Coq.Reals.Reals.
Require Import Coquelicot.Coquelicot.

Inductive Euc:nat -> Type:=
|RO : Euc 0
|Rn : forall {n:nat}, R -> Euc n -> Euc (S n).

Notation "[ ]" := RO.
Notation "[ r1 , .. , r2 ]" := (Rn r1 .. ( Rn r2 RO ) .. ).
Infix ":::" := Rn (at level 60, right associativity).

基本列表操作。

Definition head {n} (v : Euc (S n)) : R :=
  match v with
  | x ::: _ => x
  end.

Definition tail {n} (v : Euc (S n)) : Euc n :=
  match v with
  | _ ::: v => v
  end.

(* extract the last element *)   
Fixpoint last {n} : Euc (S n) -> R :=
  match n with
  | 0%nat => fun v => head v
  | S n => fun v => last (tail v)
  end.

(* eliminate last element from list *)
Fixpoint but_last {n} : Euc (S n) -> Euc n :=
  match n with
  | 0%nat => fun _ => []
  | S n => fun v => head v ::: but_last (tail v)
  end.
 
(* do the opposite of cons *)
Fixpoint snoc {n} (v : Euc n) (x : R) : Euc (S n) :=
  match v with
  | [] => [x]
  | y ::: v => y ::: snoc v x
  end.

(* extract last k elements *)
Fixpoint lastk k n : Euc n -> (lt k n) -> Euc k := 
  match n with
    |0%nat => fun _ (H : lt k 0) => False_rect _ (Lt.lt_n_O _ H)
    |S n => match k with
              |S m => fun v H => snoc (lastk m n (but_last v) (le_S_n _ _ H)) (last v)
              |0%nat => fun _ H => []
            end
  end.

(* extract first k elements *)
Fixpoint firstk k n : Euc n -> (lt k n) -> Euc k := 
  match n with
    |0%nat => fun _ (H :lt k 0) => False_rect _ (Lt.lt_n_O _ H)
    |S n => match k with
              |S m => fun v H => (head v) ::: firstk m n (tail v) (le_S_n _ _ H)
              |0%nat => fun _ _ => []
            end
  end.

(* extract nth element *)
(* 0 origine *)
Fixpoint EucNth (k:nat) :forall {n}, Euc (S n) -> R:=
 match k with
 | 0%nat => fun _ e => head e
 | S k' => fun n =>
   match n return Euc (S n) -> R with
   | 0%nat => fun e => head e
   | S n' => fun v => EucNth k' (tail v)
   end
 end.

Fixpoint EucAppend {n m} (e:Euc n) (f:Euc m) :Euc (n+m):=
 match e with
 |[] => f
 |e' ::: es => e' ::: (EucAppend es f)
 end.

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

Fixpoint QuadraticError {n : nat} (b : Euc n) : Euc n -> Euc n.
refine (match b in Euc n return Euc n -> Euc n with
    |@Rn m x xs => _    
    |@RO => fun H => []
 end).
remember (S m).
intro H; destruct H as [| k y ys].
inversion Heqn0.
inversion Heqn0.
subst; exact ((x - y)^2 ::: QuadraticError _ xs ys).
Defined.

Fixpoint EucSum {A}(e:Euc A) :R:=
 match e with
 | [] => 0%R
 | e' ::: es => e' + (EucSum es)
 end.

Answer 1

你的引理 k + S (P - (k + 1)) = P 可以用基本的代数运算来解决。特别是你只需要两个引理就可以使这更容易：

Theorem minus_assoc : forall y z, z < y -> z + (y - z) = y.
  intro y.
  induction y.
  intros;inversion H.
  intros.
  destruct z.
  trivial.
  rewrite PeanoNat.Nat.sub_succ.
  rewrite <- (IHy _ (le_S_n _ _ H)) at 2; trivial.
Qed.

Theorem minus_S : forall x y, y < x -> S (x - (S y)) = x - y.
  intro.
  induction x.
  intros.
  inversion H.
  intros.
  destruct y.
  simpl.
  rewrite PeanoNat.Nat.sub_0_r; trivial.
  rewrite PeanoNat.Nat.sub_succ.
  apply IHx.
  exact (le_S_n _ _ H).
Qed.

现在你只需要将你的目标重写为一个简单的介词:

Theorem arith_basic : forall k P, k < P -> k + S (P - (k + 1)) = P.
  intros.
  rewrite PeanoNat.Nat.add_1_r.
  rewrite minus_S.
  auto.
  rewrite minus_assoc.
  assumption.
  trivial.
Qed.

大多数这类目标都可以通过 lia tactic 解决，它会自动解决 Z、nat、positive 和 N 的算术目标。

Theorem arith_basic : forall k P, k < P -> k + S (P - (k + 1)) = P.
  intros;lia.
Qed

尽管我推荐自动化，但通过手证明可以帮助理解您的主要目标，这可能无法仅通过自动化来解决。

Answer 2

我自己解决了

我们可以使用 generalize 策略复制 sub-goal 中的引理。

Definition deriveP {P A B}(k:nat)(I:Euc (S P) -> Euc A -> Euc B)
                                 (input:Euc A)(train:Euc B)(p :Euc (S P)) 
                                  :(lt k (S P)) -> (lt ((S P)-(k+1)) (S P)) -> R.
intros.
generalize H.
intro H1.
apply arith_basic in H1.
pose lk := lastk ((S P)-(k+1)) (S P) p H0.
pose fk := firstk k (S P) p H.
pose pk := EucNth k p.
rewrite (_: (P.+1)%nat = (k + (P.+1 - (k + 1)%coq_nat)%coq_nat.+1)%coq_nat) in I.
exact ( Derive (fun PK => EucSum (QuadraticError (I (fk +++ (PK ::: lk)) input) train )) pk ).
apply H1.
Defined.

在 Coq 上转换离开先前状态的引理

Transform the lemma leaving previous state on Coq

coq

dependent-type