在Coq中惯用地表达"以下是等价的"

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.

表明这个引理可能需要一些聪明才能找到足够强大的归纳推广.我现在无法证明这一点,但如果你愿意,可能会在以后的答案中添加一个解决方案.