时间戳

首页 > 解决方案 > 如何证明从典型类型到“Prop”的所有函数 P、Q，“forall a, b, P(a) or Q(b) 成立”当且仅当“forall a, P(a), or, forall b, Q (b), 持有”？

coq - 如何证明从典型类型到“Prop”的所有函数 P、Q，“forall a, b, P(a) or Q(b) 成立”当且仅当“forall a, P(a), or, forall b, Q (b), 持有”？

问题描述

Lemma forall_P_Q_a_b_notPa_or_notPb_iff_forall_a_notPa_or_forall_b_notPb : forall (T : Type) (P Q : T->Prop),
  (forall a b, P a \/ Q b) <-> ((forall a, P a) \/ (forall b, Q b))
.
Proof.
  intros. split; intros.
  - admit.
  - destruct H; auto.
Admitted.

我很容易证明了一方，但找不到证明另一方的方法。 edestruct由于范围，对我不起作用。我应该如何证明这个定理？

标签： coq

解决方案

我相信这需要经典逻辑：

Require Import Coq.Logic.Classical.

Lemma forall_P_Q_a_b_notPa_or_notPb_iff_forall_a_notPa_or_forall_b_notPb : forall (T : Type) (P Q : T->Prop),
  (forall a b, P a \/ Q b) <-> ((forall a, P a) \/ (forall b, Q b))
.
Proof.
  intros T P Q. split; intros H.
  - destruct (classic (forall a, P a)) as [HP|HP]; auto. (* Classical reasoning *)
    destruct (not_all_ex_not _ _ HP) as [a Ha]. (* Also here *)
    right; intros b.
    specialize (H a b). tauto.
  - destruct H; auto.
Qed.

推荐阅读