Coq将不存在转换为forall语句 [英] Coq convert non exist to forall statement
问题描述
我是Coq的新手。这是我的问题。
我有一条声明说:
I'm new to Coq. Here's my problem. I have a statement says:
H : forall x : term, ~ (exists y : term, P x y /\ ~ P y x)
我想它等同于:
forall x y : term, (P x y /\ ~ P y x) -> false
但是我可以使用哪种策略转换假设?
But which tactic can I use to convert the hypothesis?
推荐答案
我不知道将不存在转换为永久不存在的策略,但是您总是可以 Ltac
策略定义或简单的定理[1]。)
I don't know of a tactic to turn not-exists into forall-not, but you can always just assert
and prove it. (If you need that repeatedly, you can pack that up into an Ltac
tactic definition or a simple theorem[1].)
以下是证明这一点的三种方法。 (您应该能够将此成绩单复制/粘贴到CoqIDE或Emacs / ProofGeneral中并逐步执行代码。)
Here's three ways of getting this proved. (You should be able to just copy/paste this transcript into CoqIDE or Emacs/ProofGeneral and step through the code.)
[1]存在引理<$ c库中的$ c> not_ex_all_not Coq.Logic.Classical_Pred_Type
,但是加载会引入经典逻辑的公理(这里甚至不需要)。
[1] There exists a lemma not_ex_all_not
in the Library Coq.Logic.Classical_Pred_Type
, but loading that would pull in the axiom for classical logic (which isn't even needed here).
(* 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 *)
(*
这是长版本,有一些解释: *)
(*
Here's the long version, with some explanations: *)
(* 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'.
(*
您也可以在一条语句: *)
(*
you can also do it in a single statement: *)
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'.
(*
这样简单的东西也可以可以用手写来写: *)
(*
simple stuff like this can also be written by hand: *)
pose proof (fun x y Pxy => H x (ex_intro _ y Pxy)) as H'; simpl in H'.
(*
现在您有H'正确的类型;可以选择删除旧的H: *)
(*
now you have H' of the right type; optionally get rid of the old H: *)
clear H; rename H' into H.
这篇关于Coq将不存在转换为forall语句的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!