我有一个已知值的列表，希望在其上进行归纳，并跟踪原始列表，并通过元素引用它。也就是说，我需要通过不同的i来引用l[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函数，并且能够使用它和refine证明定理。但是，我必须自己构建命题P。通常，你想使用归纳法。
这需要区分哪些元素是原始列表l，哪些是归纳的子列表s。因此，我可以使用remember。
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".
那么，如何更改归纳原理以使其与归纳策略一起使用呢？
看起来它在外部变量和函数内部的变量之间混淆了。
但是，我没有办法谈论不在范围内的内部变量。
这非常奇怪，因为使用精炼调用没有问题。
我知道对于匹配，有as子句，但是我无法弄清楚如何在此应用。
或者，是否有一种方法可以使list_nth_rect使用P l l 0并仍然指示哪些变量对应于l和s？