我很高兴你重新提出你的问题@laibanaz。
您现在的引理只是您在上一个 post 中提出的先前引理的更强大版本。
例如，知道所有值都等于/小于列表的最大值，因此也知道某个列表的第 n 个尾部的任何值：
Fixpoint taill {A} (x : nat) (ls : list A) : list A :=
match x with
|S n => match ls with
|k :: u => taill n u
|[] => []
end
|0 => ls
end.
Theorem maxValue_tail : forall ls y (H : [] <> ls) n, In n (taill y ls) -> n <= maxvalue H.
你应该可以得到：
(* your lemma probably will need a way of checking the index boundaries, so I put this additional checking*)
Theorem sorting_leb_order : forall (l : list nat) k k',
descending l -> k' < length l -> k < length l -> k <= k ->
index_value k' l <= index_value k l.
仅仅依赖于任何（降序）排序列表，头部是最大值并且获得某个列表的索引，只是某个第 n 个列表的头部。
(* the j second index is really necessary? *)
Fixpoint index_value (i: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h t =>
match (Nat.eqb i 0) with
| true => h
| false => index_value (i - 1) t
end
end.
Definition hd A (ls : list A) : [] <> ls -> A :=
match ls return [] <> ls -> A with
|x :: xs => fun H => x
|[] => fun H => match (H eq_refl) with end
end.
Theorem maxl_prop : forall (l : list nat) (H : [] <> l),
descending l -> maxvalue H = hd H.
(* the index of some value is the head of nth tail *)
Theorem index_taill : forall (ls : list nat) k (H : [] <> (taill k ls)),
index_value k ls = hd H.
(* We'll need a way of getting a In preposition of some index value *)
Theorem index_InBound : forall k k' l, k' < length l -> k <= k' ->
In (index_value k' l) (taill k l).
Theorem inToIndex : forall (ls : list nat) k, k < length ls -> In (index_value k ls) ls
现在，我们只需要证明sorting_leb_order 用上面的定理重写引理（其他定理在你上一个post 中可用）：
Theorem sorting_leb_order : forall (l : list nat) k k',
descending l -> k' < length l -> k < length l -> k <= k' ->
index_value k' l <= index_value k l.
intros.
destruct (destruct_list (taill k l)).
do 2! destruct s.
have : ~ [] = taill k l. rewrite e; done.
move => H'.
(*rewrite the definitions*)
pose (inToIndex H0).
rewrite (index_taill H'); rewrite <- maxl_prop.
by apply : maxValue; apply : index_InBound.
clear i e x0 H0 H1.
move : H.
(* cut a sorted listed produces a cutted list sorted *)
unfold descending.
elim/@taill_scheme : (taill k l).
intros; assumption.
intros; assumption.
intros; apply : H; simpl in H0.
destruct u.
exact I.
(*bound checking *)
by case : H0.
have : False.
elim/@taill_scheme : (taill k l) H1 e.
intros; subst.
inversion H1.
intros; inversion H1.
intros; apply : H1.
auto with arith.
trivial.
move => //=.
Qed.
我提出了排序介词的定义，但是你可以毫无问题地证明你的介词的对应关系。
引理不一定很难，但可以快速增长，这取决于您使用的定义类型。在这种情况下，一旦您更喜欢使用未绑定的索引版本（最好使用Fin），引理就更具挑战性，首先是因为边缘情况，其次是因为使用索引进行归纳需要更多指定的方案。不幸的是 ... 引理变得有点大，因此我无法在此处发布完整的证明，但您可以得到 here)。