我正在尝试证明以下情况是家庭作业，并且一直在工作，但仍然没有运气。
关于我做错了什么的任何建议或意见？
问问题
370 次
3 回答
4
这就是你在 Coq 中证明它的方式：
Coq < Theorem curry : forall p q r, ((q /\ p) -> r) -> p -> q -> r.
1 subgoal
============================
forall (p q : Prop) (r : Type), (q /\ p -> r) -> p -> q -> r
首先，我们命名所有的前提：
curry < intros p q r f x y.
1 subgoal
p : Prop
q : Prop
r : Type
f : q /\ p -> r
x : p
y : q
============================
r
产生子目标的唯一前提r是f：
curry < apply f.
1 subgoal
p : Prop
q : Prop
r : Type
f : q /\ p -> r
x : p
y : q
============================
q /\ p
要应用f，我们首先需要满足子目标q和p：
curry < split.
2 subgoals
p : Prop
q : Prop
r : Type
f : q /\ p -> r
x : p
y : q
============================
q
subgoal 2 is:
p
前提y是子目标的证明q：
curry < exact y.
1 subgoal
p : Prop
q : Prop
r : Type
f : q /\ p -> r
x : p
y : q
============================
p
前提x是子目标的证明p：
curry < exact x.
No more subgoals.
我们完成了。这是完整的证明：
curry < Qed.
intros p q r f x y.
apply f.
split.
exact y.
exact x.
curry is defined
在像 Haskell 这样的函数式编程语言中，您将拥有：
curry :: ((q, p) -> r) -> p -> q -> r
curry f x y = f (y, x)
由于库里-霍华德的通信，一切都解决了。
于 2016-02-17T03:44:01.370 回答
1
感谢@Aadit，我们有一个 Coq 证明，而且提供 Agda 证明才是公平的 --- 合乎道德的？---。
一个直接而简单的证明是
open import Data.Product
portation : {P Q R : Set} → (P × Q → R) → (P → Q → R)
portation P×Q→R = λ p q → P×Q→R (p , q)
当然，如果提问者不熟悉 Agda 并且正在寻求形式化，这可能根本不清楚。所以让我们详细介绍一下！！
在建设性逻辑中，命题可以被视为小类型：
ℙrop = Set
然后配对是形成共轭的常用方式，
data _∧_ (P Q : ℙrop) : Set where
∧I : P → Q → P ∧ Q
在构造逻辑中，蕴涵只是函数空间：说一件事暗示另一件事就等于产生一个过程，该过程以第一类输入返回第二类输出。
_⇒_ : (P Q : ℙrop) → Set
_⇒_ = λ P Q → (P → Q)
隐含引入就是通常的函数定义，隐含消除只不过是函数应用。
⇒I : ∀ {P Q} → (P → Q) → P ⇒ Q
⇒I P→Q = P→Q
⇒E : ∀ {P Q} → P ⇒ Q → P → Q
⇒E P→Q p = P→Q p
现在提问者使用自然演绎风格的证明，所以让我们引入一些语法糖来弥补从纸笔证明到 Agda 形式化的差距。
syntax ⇒I {P} {Q} (λ p → q) = ⇒-I-assuming-proof p of P we-have Q proved-by q
现在证明！
shunting : (P Q R : ℙrop) → (P ∧ Q) ⇒ R → P ⇒ (Q ⇒ R)
shunting P Q R P∧Q⇒R =
⇒-I-assuming-proof p of P
we-have Q ⇒ R proved-by
⇒-I-assuming-proof q of Q
we-have R proved-by
⇒E P∧Q⇒R (∧I p q)
这不仅可读性强，而且有点接近提问者的介绍！
阿格达真是太高兴了！
于 2016-02-17T18:58:23.663 回答
0
这是使用 Klement 的 Fitch 式自然演绎证明检查器和提供解释的forallx教科书的证明。（链接如下。）
最初尝试的主要问题是第 8 行和第 9 行没有解除假设。根据缩进和大括号，它们似乎停留在相同的子证明中。
否则证明与我提供的相同。在我的第 6 行，我通过引入条件（第 3-5 行）解除了我在第 3 行对“Q”所做的假设。在我的第 7 行，我通过引入条件（第 2-6 行）解除了在第 2 行所做的假设“P”。
参考
Kevin Klement 的 JavaScript/PHP Fitch 风格的自然演绎证明编辑器和检查器http://proofs.openlogicproject.org/
PD Magnus、Tim Button 以及 J. Robert Loftis 的添加，由 Aaron Thomas-Bolduc、Richard Zach 重新混合和修订，forallx Calgary Remix: An Introduction to Formal Logic，2018 年冬季。http: //forallx.openlogicproject.org/
于 2018-11-22T02:19:07.987 回答