coq - 在 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.

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

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.

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