>我有一个自然数列表，列表中的元素按降序排列。 我想写关于列表的引理，第一个元素h大于列表的所有元素。让列表为 [h;h1;t] .0 h1？ 请指导我，如何写h大于列表尾部的所有元素。
你需要说
对于任何自然数，以及任何像
h::t这样的列表，如果列表是降序的，如果数字在尾部，那么它比头部小。
所以你可以用辅酶语言写
Lemma head_is_max : forall n h t, desc (h::t) -> In n t -> h >= n.
如果 desc 是一个布尔谓词，你可以写
Lemma head_is_max : forall n h t, desc (h::t) = true -> In n t -> h >= n.
对t进行归纳将用于证明。
以更复杂的方式，您可以使用列表上的谓词，该谓词断言列表的所有元素都具有特定属性，您可以将其定义为
Fixpoint All {T : Type} (P : T -> Prop) (l : list T) : Prop :=
match l with
| [] => True
| h :: t => P h / All P t
end.
所以All P l意味着P x对l中的所有x都成立。现在我们可以把提到的引理写成
Lemma head_is_max : forall h t, desc (h::t) -> All (fun n => h >= n) t.
要表示给定的自然数列表是按降序排列的，您可以使用 CoqList模块中的现有函数。
Require Import List Lia.
Definition desc (l : list nat) : Prop :=
forall i j, i <= j -> nth j l 0 <= nth i l 0.
我做了什么？ 我只是表示，对于任何大于ij，排名i的值必须大于排名j的值。 这在微妙的方式上是聪明的。 表达式实际上nth j l 0表示排名i的值(如果i小于列表的长度l否则0。 碰巧0比任何其他自然数都小，所以这个定义确实有效。 相反，如果您要求严格降序排列的数字列表，那么我将不得不编写一个更精确的定义，仅涉及小于列表长度的秩(您可以使用函数length)。 我让你这样做作为一种练习。
当你写一个像这里desc这样的逻辑谓词时，测试这个定义是很重要的，以确保你真的抓住了你心中的概念。 为了测试我自己的定义，我编写了以下代码：
Definition sample1 := 1 :: 2 :: 3 :: nil.
Definition sample2 := map (fun x => 10 - x) sample1.
Lemma s2_desc : desc sample2.
Proof.
intros [ | [ | [ | [ | ]]]] [ | [ | [ | [ | ]]]];
intros ilej; simpl; lia.
Qed.
Lemma s1_n_desc : ~desc sample1.
Proof.
intros abs; generalize (abs 0 1 (le_S _ _ (le_n _))).
compute; lia.
Qed.
s2_desc的证明是通过蛮力证明，它实际上尝试所有小于 4 的秩对，并检查 在所有这些情况下，自然数(列表中的等级或值)之间的比较确实给出了逻辑上可证明的公式。
s1_n_desc证明用于检查我对desc的定义是否真的拒绝了显然不符合标准的列表。 我写了这个证明是一件好事，因为它帮助我发现了我的desc代码中的一个错误，而这个错误没有被以前的证明捕获：我写了nth 0 l i而不是nth i l 0！
最后但并非最不重要的一点是，我的解决方案从Require Import List Lia.这意味着我们使用两个现有的 Coq 模块。 第一个提供了关于列表的常用函数，第二个提供了一个自动工具来执行关于数字(实际上是自然数或整数)之间比较的简单证明。
下一步，还可以编写一个布尔函数，该函数在其输入时准确计算true值。 降序并开发测试证明，以验证这两个函数的行为是否相应地。
你需要定义你所说的descending是什么意思，并在你的证明中使用它。 @Yves也许有最整洁的方式。 这是另一个定义 只是写下一个简单的归纳定义。 如果尾部呈降序，并且第一个元素大于或等于第二个元素，则列表呈降序。
归纳定义的一个好处是，你可以对它们进行归纳，这在每个证明案例中都为你提供了大量信息，而工作量很小。
Require Import List.
Inductive descending : list nat -> Prop :=
desc_nil : descending nil
| desc_1 n : descending (cons n nil)
| desc_hd n m l :
m <= n ->
descending (cons m l) ->
descending (cons n (cons m l)).
Lemma head_gt l d:
descending l -> forall m, In m l -> m <= hd d l.
Proof.
induction 1; intros k H'.
now exfalso; apply in_nil in H'.
now replace k with n; [ | inversion H'].
now inversion H';
[ subst; apply le_n
| eapply PeanoNat.Nat.le_trans; auto].
Qed.