1

我是 Coq 的新手。这是我的问题。我有一个声明说：

H : forall x : term, ~ (exists y : term, P x y /\ ~ P y x)

我想它相当于：

forall x y : term, (P x y /\ ~ P y x) -> false

但是我可以使用哪种策略来转换假设？

4

3 回答 3

1

我不知道将不存在变成完全不存在的策略，但你总是可以公正assert并证明它。（如果你反复需要它，你可以把它打包成一个Ltac战术定义或一个简单的定理[1]。）

这是证明这一点的三种方法。（您应该能够将此脚本复制/粘贴到 CoqIDE 或 Emacs/ProofGeneral 并逐步执行代码。）

not_ex_all_not[1] Library 中存在一个引理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.
于 2014-02-11T01:08:06.443 回答
0

您可以使用unfold not at 1 in H. ~ P只是not P, 和not P = (P -> False)定义的符号。at 1部分表示您只希望第unfold一次出现not，in H部分表示您只希望unfold在假设中出现H。

于 2014-02-08T14:17:13.723 回答
0

其实可以直接用coq的库来证明。只需使用From Coq Require Export Init.Logic

于 2020-07-28T14:39:24.943 回答