coq 归纳法，传入相等

Question

我有一个已知值的列表，想对其进行归纳，跟踪原始列表是什么，并按元素引用它。也就是说，我需要通过 l[i] 使用不同的 i 而不是只有 (a::l) 来引用它。

我试图制定一个归纳原则来允许我这样做。这是一个使用简化示例将所有不必要的定理替换为 Admitted 的程序。目标是使用 countDown_nth 证明 allLE_countDown，并以方便的形式获得 list_nth_rect。 (该定理很容易在没有任何这些的情况下直接证明。)

Require Import Arith.
Require Import List.

Definition countDown1 := fix f a i := match i with
| 0 => nil
| S i0 => (a + i0) :: f a i0
end.

(* countDown from a number to another, excluding greatest. *)
Definition countDown a b := countDown1 b (a - b).

Theorem countDown_nth a b i d (boundi : i < length (countDown a b))
    : nth i (countDown a b) d = a - i - 1.
Admitted.

Definition allLE := fix f l m := match l with
| nil => true
| a :: l0 => if Nat.leb a m then f l0 m else false
end.

Definition drop {A} := fix f (l : list A) n := match n with
| 0 => l
| S a => match l with
  | nil => nil
  | _ :: l2 => f l2 a
  end
end.

Theorem list_nth_rect_aux {A : Type} (P : list A -> list A -> nat -> Type)
    (Pnil : forall l, P l nil (length l))
    (Pcons : forall i s l d (boundi : i < length l), P l s (S i) -> P l ((nth i l d) :: s) i)
    l s i (size : length l = i + length s) (sub : s = drop l i) : P l s i.
Admitted.

Theorem list_nth_rect {A : Type} (P : list A -> list A -> nat -> Type)
    (Pnil : forall l, P l nil (length l))
    (Pcons : forall i s l d (boundi : i < length l), P l s (S i) -> P l ((nth i l d) :: s) i)
    l s (leqs : l = s): P l s 0.
Admitted.

Theorem allLE_countDown a b : allLE (countDown a b) a = true.
  remember (countDown a b) as l.
  refine (list_nth_rect (fun l s _ => l = countDown a b -> allLE s a = true) _ _ l l eq_refl Heql);
    intros; subst; [ apply eq_refl | ].
  rewrite countDown_nth; [ | apply boundi ].
  pose proof (Nat.le_sub_l a (i + 1)).
  rewrite Nat.sub_add_distr in H0.
  apply leb_correct in H0.
  simpl; rewrite H0; clear H0.
  apply (H eq_refl).
Qed.

因此，我有 list_nth_rect 并且能够根据需要通过引用第 n 个元素将其与优化一起使用来证明定理。但是，我必须自己构建命题 P。通常，您希望使用归纳法。

这需要区分哪些元素是原始列表 l 与引入的子列表 s。所以，我可以使用记住。

Theorem allLE_countDown a b : allLE (countDown a b) a = true.
  remember (countDown a b) as s.
  remember s as l.
  rewrite Heql.

这让我在

  a, b : nat
  s, l : list nat
  Heql : l = s
  Heqs : l = countDown a b
  ============================
  allLE s a = true

但是，我似乎无法像上面那样通过平等。当我尝试

  induction l, s, Heql using list_nth_rect.

我收到错误

Error: Abstracting over the terms "l", "s" and "0" leads to a term
fun (l0 : list ?X133@{__:=a; __:=b; __:=s; __:=l; __:=Heql; __:=Heqs})
  (s0 : list ?X133@{__:=a; __:=b; __:=s; __:=l0; __:=Heql; __:=Heqs})
  (_ : nat) =>
(fun (l1 l2 : list nat) (_ : l1 = l2) =>
 l1 = countDown a b -> allLE l2 a = true) l0 s0 Heql
which is ill-typed.
Reason is: Illegal application: 
The term
 "fun (l l0 : list nat) (_ : l = l0) =>
  l = countDown a b -> allLE l0 a = true" of type
 "forall l l0 : list nat, l = l0 -> Prop"
cannot be applied to the terms
 "l0" : "list nat"
 "s0" : "list nat"
 "Heql" : "l = s"
The 3rd term has type "l = s" which should be coercible to 
"l0 = s0".

那么，我该如何改变归纳原理
这样它就适用于感应策略？
看起来它之间变得困惑
外部变量和内部变量
功能。但是，我没有办法说话
关于不在范围内的内部变量。
这很奇怪，因为调用它
完善工作没有问题。
我知道比赛，有作为条款，但
我不知道如何在这里应用它。
或者，有没有办法让 list_nth_rect 使用 P l l 0并且仍然指出哪些变量对应于 l 和 s？

Answer 1

首先，您可以通过重用更基本的结果来更容易地证明这个结果。这是一个基于 ssreflect 库定义的版本:

From mathcomp
Require Import ssreflect ssrfun ssrbool ssrnat eqtype seq.

Definition countDown n m := rev (iota m (n - m)).

Lemma allLE_countDown n m : all (fun k => k <= n) (countDown n m).
Proof.
rewrite /countDown all_rev; apply/allP=> k; rewrite mem_iota.
have [mn|/ltnW] := leqP m n.
  by rewrite subnKC //; case/andP => _; apply/leqW.
by rewrite -subn_eq0 => /eqP ->; rewrite addn0 ltnNge andbN.
Qed.

在这里， iota n m是 m的列表从 n 开始计数的元素, 和 all是您的 allLE 的通用版本.标准库中存在类似的函数和结果。

回到您最初的问题，确实有时我们需要在记住我们开始的整个列表的同时对列表进行归纳。不知道有没有办法用标准的感应战术来得到你想要的东西；我什至不知道它有一个多参数变体。当我想证明 P l使用这种策略，我通常按以下步骤进行:

查找谓词 Q : nat -> Prop使得 Q (length l)暗示 P l .通常，Q n将有表格 n <= length l -> R (take n l) (drop n l) ，其中 R : list A -> list A -> Prop .

证明 Q n所有 n通过归纳。