在 Coq 中惯用地表达 "The Following Are Equivalent"

Question

Coq'Art中的练习 6.7，或软件基础中逻辑章节的最后练习：证明以下是等价的.

Definition peirce := forall P Q:Prop, ((P->Q)->P)->P.
Definition classic := forall P:Prop, ~~P -> P.
Definition excluded_middle := forall P:Prop, P\/~P.
Definition de_morgan_not_and_not := forall P Q:Prop, ~(~P/\~Q)->P\/Q.
Definition implies_to_or := forall P Q:Prop, (P->Q)->(~P\/Q).

解决方案集使用五个独立的引理，通过蕴含的循环链来表达这一点。但是 "TFAE" 证明在数学中很常见，我想用一个成语来表达它们。 Coq 里有吗？

Answer 1

这种类型的模式很容易在 Coq 中表达，尽管设置基础结构可能需要一些努力。

首先，我们定义一个命题，表示一个列表中的所有命题都是等价的：

Require Import Coq.Lists.List. Import ListNotations.

Definition all_equivalent (Ps : list Prop) : Prop :=
  forall n m : nat, nth n Ps False -> nth m Ps True.

接下来，我们要捕捉证明这种结果的标准模式：如果列表中的每个命题都蕴含下一个命题，而最后一个命题蕴含第一个命题，我们知道它们都是等价的。（我们也可以有一个更通用的模式，我们用 graph 命题之间的蕴涵替换直接的蕴涵列表，其传递闭包生成一个完整的图。我们将避免这种情况为了简单起见。）这种模式的前提很容易表达；只是上面英文解释的代码转写

Fixpoint all_equivalent'_aux 
  (first current : Prop) (rest : list Prop) : Prop :=
  match rest with
  | []         => current -> first
  | P :: rest' => (current -> P) /\ all_equivalent'_aux first P rest'
  end.

Definition all_equivalent' (Ps : list Prop) : Prop :=
  match Ps with
  | first :: second :: rest =>
    (first -> second) /\ all_equivalent' first second rest
  | _ => True
  end.

困难的部分是表明这个前提蕴含了我们想要的结论：

Lemma all_equivalentP Ps : all_equivalent' Ps -> all_equivalent Ps.

证明这个引理成立可能需要一些独创性才能找到足够强大的归纳概括。我现在无法完全证明这一点，但如果您愿意，可以稍后在答案中添加一个解决方案。

在 Coq 中惯用地表达 "The Following Are Equivalent"

Idiomatically expressing "The Following Are Equivalent" in Coq

coq