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，但是我要return一个P (S n) _ _ (next _ _)，所以等式关系不走"together"的归纳法，最后记住永远遇到一个奇怪的问题。

Answer 1

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

对于给定的 n，您有 n1 = S n，并且您想对 n1 进行归纳（实际上是对向量进行归纳，但这对我们的目的而言并不重要）。 Coq 首先将您的目标概括为依赖于 n1 的所有内容（包括 n1 = S n 的证明）。但这是错误的归纳假设；仅当 n1 是此特定 n 的后继者时，您才不会试图通过归纳来证明您的陈述。相反，您想在 n1 是 any n 的后继者时证明您的陈述，因此您必须在执行归纳之前对 n 进行概括。

作为替代方案，在这种情况下，您可以先证明 S n <> 0，然后您不需要 remember 任何东西，因为您的第三种情况已经有了一个荒谬的假设。

Coq：如何在不搞乱归纳假设的情况下正确记住相关值？

Coq : How to correctly remember dependent values without messing up the induction hypothesis?

coq

proof

dependent-type