coq中的自然数列表

Question

我有一个自然数列表，列表中的元素按降序排列。我想写关于列表的引理，即第一个元素h大于list的所有元素。令list为[h; h1; t]。 0小时1？请指导我，如何写h大于列表尾部的所有元素。

Answer 1

您需要说

对于任何自然数，以及诸如h::t之类的任何列表，如果列表是降序并且如果数字在尾部，则它小于头。

所以您可以用Coq语言写

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对于x中的所有l都成立。现在我们可以将提到的引理写成

Lemma head_is_max : forall h t, desc (h::t) -> All (fun n => h >= n) t.