Coq：如何正确记住从属值而不弄乱归纳假设？

Question

我对一个具有leb值（x <= y）的向量有一个归纳方案，

Definition vector_ind_with_leb : forall (A : Type) (P : forall n y: nat, y <= n -> vector A n -> Prop),
       (forall (n : nat) (y : nat) (H : S y <= S n) (a : A) (v : vector A n),
        P n y (le_S_n _ _ H) v -> P (S n) (S y) H (insert a v)) ->
       (forall (n : nat) (H : 0 <= S n) (a : A) (v : vector A n),
         P (S n) 0 H (insert a v)) ->     
        (forall (y : nat) (H : 0 <= 0), P 0 0 H (empty A)) -> forall (n : nat) (y : nat) (Heq : y <= n) (v : vector A n), P n y Heq v.

have : forall n, 0 <= S n -> 0 <= n.
auto with arith.

move => P' A P H K K'.
refine ( fix Ffix (x : nat) (y : nat) (Heq : y <= x) (x0 : vector _ x) {struct x0} : 
       P x y Heq x0 := _).

destruct x0.
destruct y.
refine (K n Heq a _).
refine (H n _ Heq a _ (Ffix _ y _ x0)).
  have : forall y, y <= 0 -> y = 0.
    auto with arith.

move => F'.
set only_0 := F' _ Heq.
destruct y.
refine (K' 0 Heq).
inversion Heq.
Show Proof.
Defined.

我必须证明类似的东西：

Theorem update_vector_correctly : forall {A} n y (x : vector A (S n)) (H : S n >= S y) v, get_value (set_value x (S y) v) (S y) = Some v.

所以我得到了三种情况。

when (for y and n),
     S y <= S n.
     0 <= S n.
     0 <= 0.

但是，如果您注意到案例3对于所有0 <> S n来说都是荒谬的，一次n，所以我必须记住(S n)是一个成功的数字。

当我使用这个时：记住（S n）。

我明白了：

H : 0 <= 0
Heqn0 : 0 = S n

但是在第一种情况下，我得到了：

H0 : n1 = S n -> get_value (set_value v0 y0 v) y0 = Some v
Heqn0 : S n1 = S n

这既不是错误案例也不是真实案例。问题是我的假设是n，但是我必须返回P (S n) _ _ (next _ _)，因此等式关系不会“一起”走归纳法，最后记住总会遇到一个奇怪的问题。

Answer 1

解决方案是generalize dependent n和remember之间的induction。您遇到的问题如下：

Answer 2

我解决了专门用于归纳方案的问题