证明包含不存在的定理

Question

我试图证明我正在阅读的一篇论文（Bennett，Having a Part Twice Over，2013 年）中的定理，但我不知道如何解决子目标。

这是我应该用于证明的代码：

Parameter Entity: Set.
Parameter F : Entity -> Entity -> Prop.
Parameter Ps : Entity -> Entity -> Prop.
Definition P x y := exists s, F x s /\ Ps s y.
Definition PP x y := P x y /\ ~ P y x.
Definition PPs x y := Ps x y /\ ~ F y x.
   
(* Mutual Occupancy is Identity *)
Axiom A6 : forall x y z1 z2,
  (Ps z1 y /\ F x z1) /\ (Ps z2 x /\ F y z2) -> x = y.

(* Single Occupancy *)
Axiom A7 : forall x y,
  Ps x y -> exists! z, F z x.

(* Anti-Symmetry *)
Theorem T8 : forall x y,
  (P x y /\ P y x) -> x = y.
Proof.
  unfold P.
  firstorder.
  apply A6 with (z1 := x1) (z2 := x0).
  auto.
Qed.

这是定理和我不完整的证明：

(* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP; unfold PPs; unfold P.
  intro b.
  split.
  (* left to right *)
  - intro Ea.
    destruct Ea as (a, PPab).
    destruct PPab as (Pab, nPba).
    destruct Pab as (c, Pab).
    destruct Pab as (Fac, Pscb).
    exists c.
    split.
    -- apply Pscb.
    -- admit.           (* Here! *)
  (* right to left *)
  - intro Ea.
    destruct Ea as (a, PPsab).
    destruct PPsab as (Psab, nFba).
    apply A7 in Psab as Ec.
    destruct Ec as (c, Fca).
    destruct Fca as (Fca, Uc).
    exists c.
    split.
    -- exists a.
       split.
       --- apply Fca.
       --- apply Psab.
    -- admit.            (* And here! *)
Admitted.

所以有两个子目标我无法证明。在每一个中，都有 ~ (exists s : Entity, F b s /\ Ps s a) 作为假设或作为子目标。我被困在这一点上。根据论文中的证明，我应该在某个点上使用定理T8，但我不明白如何。

第一个未解决子目标的状态是

1 subgoal
b, a, c : Entity
Fac : F a c
Pscb : Ps c b
nPba : ~ (exists s : Entity, F b s /\ Ps s a)
______________________________________(1/1)
~ F b c

关于第二个：

1 subgoal
b, a : Entity
Psab : Ps a b
c : Entity
Fca : F c a
Uc : forall x' : Entity, F x' a -> c = x'
nFba : ~ F b a
______________________________________(1/1)
~ (exists s : Entity, F b s /\ Ps s c)

作为指南，这里是论文中写的证明：

那我该怎么办？（如果答案能用简单的战术而不是超强自动的战术就更好了，这样我就明白了。）

Answer 1

我不知道您可能已经拥有的所有其他公理或引理，并且可能需要它们来证明这一点，但是在这里进行否定的一种方法可能是使用对位法。在 ssreflect 中，您将 nPba 推向目标，然后 apply contra_not 引理：

contra_not
     : ∀ P Q : Prop, (Q → P) → ¬ P → ¬ Q.

事情可能会更容易从那里取得进展。

Answer 2

事实证明，您拥有完成目标所需的一切。这是你定理的证明，自愿不是自动的。一些见解：

非公式 ~P 实际上等于 P -> False 并且您可以这样对待它们（使用 intros、apply 等）。如果您尝试展开 not 本身，您会看到这一点。
您可以分组展开：unfold P, PP, PPs
您可以同时 intros 和 destruct : intros [A B] 等同于 intros H. destruct H as (A,B).
您可以使用 ; 链接策略：tactic1; tactic2. 如果 tactic1 创建多个子目标，那么 tactic2 将应用于每个子目标。
当一个策略（如 split）创建多个子目标时，您还可以通过使用 split; [ tactic1 | tactic2 ]. 为每个分支使用不同的策略如果您的策略创建超过 2 个目标也有效。
pose proof 允许您将结果添加到您的假设中，而无需将其直接应用于目标（相反哟 apply）
assert (H: _) 或 assert _ as H 允许您进行 正向推理 ：您可以陈述您想要的结果。它将创建两个目标，一个用于规定的结果，一个用于先前的目标，结果作为附加假设 H

(* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP, PPs, P. (* you can group unfolds *)
  intros b.
  split.
  - intros [a [[c [Fac Pscb]] nPba]]. (* using brackets allows you to destruct and intros at the same time *)
    exists c.
    split; [ assumption |]. 
    pose proof (A7 _ _ Pscb) as [d [Fdc Uc]].
    intros Fbc. 
    pose proof (Uc a Fac). subst.
    pose proof (Uc b Fbc). subst. 
    apply nPba.
    exists c; split.
    + apply Fbc.
    + apply Pscb.
  - intros [a [Psab nFba]].
    pose proof (A7 _ _ Psab) as [c [Fca Uc]].
    exists c.
    split.
    + exists a; split; eauto.
    + intros [d [Fbd Psdc]].
      apply nFba.
      assert (b = c) as Heqbc.
      * (* proof of b = c *)
        eapply A6 with (z1 := d) (z2 := a).
        repeat split; assumption.
      * rewrite Heqbc in *.
        apply Fca.        
Qed.

如果您正在围绕这些结果进行大型开发，您可能会发现为经常遇到的目标（或重写）定义自己的自动化策略很有用。某些 Coq 库还旨在帮助您缩短证明，例如 SSReflect (https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#) or LibTactics (https://softwarefoundations.cis.upenn.edu/sf-4.0/UseTactics.html)。它们需要比普通 Coq 多学习一些关键字和技术，但非常有用。为了这个例子，使用 SSReflect 的更自动化的证明看起来像这样：

(* Composites <-> Slot-Composites *)
Theorem T12 : forall y,
  ((exists x, PP x y) <-> (exists z, PPs z y)).
Proof.
  unfold PP, PPs, P => b; split.
  - move => [a [[c [Fac Pscb]] nPba]].
    move : (A7 Pscb) => [d [Fdc Uc]].
    exists c; split => // => Fbc.
    apply nPba.
    exists c; split => //.
    rewrite -(Uc _ Fac) (Uc _ Fbc) => //.
  - move => [a [Psab nFba]].
    move: (A7 Psab) => [c [Fca Uc]].
    exists c; split; eauto.
    move => [d [Fbd Psdc]].
    assert (b = c) ; subst; eauto using A6.
Qed.

如有其他问题，请随时发表评论！

克莱门特

证明包含不存在的定理

Proving a theorem containing not exists

coq