英文:
Forall and exists in a Coq proof
问题
目前，在我的理论中，我有以下的公理：
Axiom context_existence : forall s t a,
F a s -> Ps t a -> exists u, C u s t.
当我在证明中使用这个公理时，我会这样做：
pose proof (context_existence s t a Fas Psta) as (u & Cust).
然而，由于 a 在我的公理结论中没有被使用，我将公理重写如下：
Axiom context_existence : forall s t,
(exists a, F a s /\ Ps t a) -> exists u, C u s t.
并且，由于 (exists a, F a s /\ Ps t a) 在我的理论中具有意义，我定义了一个谓词 Cb 如下：
Definition Cb s t := exists a, F a t /\ Ps s a.
然后，我将我的公理重写如下：
Axiom context_existence : forall s t,
Cb t s -> exists u, C u s t.
然而，证明变得不那么直接。我会做类似于这样的操作：
pose proof (context_existence s t) as (u & Cust).
exists a; split; auto.
我知道如果只有 and 的话，我可以这样做：
pose proof (context_existence s t (conj Fas Psta)) as (u & Cust).
然而，由于存在 exists 子句，我不知道该如何处理它。是否有一种方法，类似于 conj 这样的函数，可以让我在一行中完成证明？
英文:
Currently, I have in my theory the following axiom:
Axiom context_existence : forall s t a,
F a s -> Ps t a -> exists u, C u s t.
When i use this axiom in a proof, I do like this:
pose proof (context_existence s t a Fas Psta) as (u & Cust).
However, as a is not used in the conclusion of my axiom, I rewrite the axiom like this:
Axiom context_existence : forall s t,
(exists a, F a s /\ Ps t a) -> exists u, C u s t.
And as (exists a, F a s /\ Ps t a) has a meaning in my theory, I defined a predicate Cb like this:
Definition Cb s t := exists a, F a t /\ Ps s a.
And I rewrite my axiom like this:
Axiom context_existence : forall s t,
Cb t s -> exists u, C u s t.
However, the proof become less direct. I do something like this:
pose proof (context_existence s t) as (u & Cust).
exists a; split; auto.
I know that if it was just the and I could do something like:
pose proof (context_existence s t (conj Fas Psta)) as (u & Cust).
However, there is the exists clause and I don’t know how to deal with it. Is there a way, like a function such as conj, that would enable me to do my proof in one line?
答案1
得分: 2
不确定我完全理解你的问题，但我尝试翻译如下。
与_/\_类似，exist在Coq中不是原始的，而是以如下方式定义的归纳谓词：
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
ex_intro : forall x : A, P x -> exists y, P y.
ex_intro : forall [A : Type] (P : A -> Prop) (x : A), P x -> exists y, P y
Arguments ex [A]%type_scope P%function_scope
Arguments ex_intro [A]%type_scope P%function_scope x _
（这是使用Print ex.和About ex_intro.打印的）
有一个名为ex_intro的构造函数，它接受：
- 第一个隐式参数（从上下文中可推断出的类型
A） - 第二个参数：关于A的谓词
P - 第三个参数：见证
x : A - 第四个参数：
P x的证明
因此，与conj一样，您可以手动构造exists公式的证明。
在这里，这会产生类似于以下的内容：
pose proof (context_existence s t
(ex_intro _ a (conj Fas Psta))) as (u & Cu).
注意，Coq足够聪明，可以从类型为(F a s /\ Ps t a)的(Fas /\ Psta)的证明中推断出谓词(fun x => F x s /\ Ps x a)，这相当有趣（我们没有提供显式谓词，而是留下了_）。同样的事情也可以用于a在这里。
英文:
Not sure I understand completely your question but here is my try.
As with _/\_, exist is not primitive in Coq, it is an inductive predicate defined this way :
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
ex_intro : forall x : A, P x -> exists y, P y.
ex_intro : forall [A : Type] (P : A -> Prop) (x : A), P x -> exists y, P y
Arguments ex [A]%type_scope P%function_scope
Arguments ex_intro [A]%type_scope P%function_scope x _
(This is printed with Print ex. and About ex_intro.)
There is one constructor called ex_intro taking
- a first implicit argument (the type
Ainferable from the context) - a second argument : a predicate
Pon A - a third argument : a witness
x : A - a fourth argument : a proof of
P x
So, as with conj, you may manually construct proofs of exists formulas.
Here, this gives something like this:
pose proof (context_existence s t
(ex_intro _ a (conj Fas Psta))) as (u & Cu).
Notice that Coq was smart enough to infer from the proof of (Fas /\ Psta) of type (F a s /\ Ps t a) the predicate (fun x => F x s /\ Ps x a) which is quite interesting (we did not provide an explicit predicate, but left _). The same could be done for a here.
通过集体智慧和协作来改善编程学习和解决问题的方式。致力于成为全球开发者共同参与的知识库，让每个人都能够通过互相帮助和分享经验来进步。
评论