Coq中的简单身份

Question

我可能遗漏了一些基本的东西.

我可以证明以下"身份":

Theorem identity_simple : forall a : Prop, a -> a.

随着intro. intro. assumption..

但是,我似乎无法证明:

Theorem identity : forall a : Prop, a.

我当然能做到intro,但这让我:

a : Prop
_________(1/1)
a

我不知道该怎么做.
第一种形式似乎是多余的,表明对所有人而言a,a意味着a.

Answer 1

forall a : Prop, a -> a.

读作"给定一些命题的证明,a我们可以构建同一命题的证明".这是真的,因为我们可以返回原始证明.

让我们用Coq检查一下:

Print identity_simple.
(* 
output:

identity_simple = fun (a : Prop) (H : a) => H
     : forall a : Prop, a -> a
*)

证明术语fun (a : Prop) (H : a) => H完全表达了所描述的行为.

第一种形式似乎是多余的,表明对所有人而言a,a意味着a.

你是对的,在某种意义上-这是很明显的.您可以将其视为一种测试 - 如果您无法证明它,那么逻辑肯定存在问题.

forall a : Prop, a.

读作"我们可以构建任何命题的证明".这不是真的,因为例如,您无法构造False(在空上下文中)的证明.这将是一场灾难 - 我们不希望使用一切都可以证明的逻辑.