我不知道有什么策略可以将“不存在”变成“forall-not”,但你总是可以assert
并证明这一点。 (如果您反复需要,可以将其打包到an Ltac战术定义或一个简单的定理[1]。)
以下是证明这一点的三种方法。 (您应该能够将此脚本复制/粘贴到 CoqIDE 或 Emacs/ProofGeneral 中并单步执行代码。)
[1] 存在引理not_ex_all_not
在图书馆Coq.Logic.Classical_Pred_Type,但是加载它会引入经典逻辑的公理(这里甚至不需要)。
(* dummy context to set up H of the correct type, for testing it out *)
Lemma SomeName (term : Type) (P : term -> term -> Prop) :
(forall x : term, ~ (exists (y : term), P x y /\ ~ P y x)) ->
True. (* dummy goal *)
Proof.
intro H.
(* end dummy context *)
(*
这是长版本,带有一些解释:*)
(* this states the goal, result will be put into the context as H' *)
assert (forall (x y : term), (P x y /\ ~ P y x) -> False) as H'.
(* get rid of unneeded variables in context, get new args *)
clear - H; intros x y Pxy.
(* unfolding the not shows the computational structure of this *)
unfold not at 1 in H.
(* yay... (x, y, Pxy) will produce False via H *)
(* specialize to x and apply... *)
apply (H x).
(* ...and provide the witness. *)
exists y. exact Pxy.
(* done. *)
(* let's do it again... *)
clear H'.
(*
您也可以在一条语句中完成此操作:*)
assert (forall x y, (P x y /\ ~ P y x) -> False) as H'
by (clear -H; intros x y Pxy; apply (H x (ex_intro _ y Pxy))).
(* and again... *)
clear H'.
(*
像这样简单的东西也可以用手写:*)
pose proof (fun x y Pxy => H x (ex_intro _ y Pxy)) as H'; simpl in H'.
(*
现在你有了正确类型的 H';可选择删除旧的 H:*)
clear H; rename H' into H.