Fixpoint index_value (i: nat) (j: nat) (l: list nat) : nat :=
match l with
| nil => 0
| cons h t => match (eqb i j) with
| true => h
| false => index_value (S i) j t
end
end.
index1 < index2
1 index_value 0 (S index2) (n' :: l) <= n'.
2 index_value 0 index2 (n' :: l) <=
index_value 0 (S index1) (n' :: l)
In hypothesis I have
H1 : (length l =? 0) = false
H2 : 0 < S index2
H3 : forall (l : list nat) (d : nat),
descending l ->
forall m : nat, In m l -> m <= hd d l.
我正在使用上述功能在自然数列表中查找不同的值。我可以通过更改索引j并保持i = 0来在列表中找到任何值。index_value 0 0 [n :: t] = n，这是最大的，因为降序排列。列表中的任何其他值，可通过更改找到j应小于n。要证明这两个案例。谢谢您的帮助。
[很高兴您重新提出问题@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).
现在，我们只需要证明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）。