#coq #dependent-type
#coq #зависимый тип
Вопрос:
Я хочу частично выводить функции, ввод которых представляет собой зависимый список.
Я попытался определить deriveP
с помощью доказательства.
Derive
является функцией в Coquelicot.Производное.
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, потому что H используется в fk.
Я могу применить arith_basic к H перед созданием fk, но тогда я не могу создать fk, потому что его нет k < P. 1
.
Я хочу применить arith_basic к H при выходе k < P. 1
.
Пожалуйста, помогите мне.
(***********************************************************)
Это зависимый список 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.
Ответ №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, которая автоматически решает арифметические цели Z, nat, positive и N.
Theorem arith_basic : forall k P, k < P -> k S (P - (k 1)) = P.
intros;lia.
Qed
Несмотря на то, что я рекомендую автоматизацию, доказательство руками может помочь понять вашу главную цель, которая может быть не в состоянии быть решена только автоматизацией.
Комментарии:
1. вероятно, вы должны добавить команду
rewrite arith_basic
илиrewrite <- arith_basic
непосредственно перед оскорбительной командой.
Ответ №2:
Я решил самостоятельно.
Мы можем дублировать лемму в подцели с generalize
помощью tactic.
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.