在Coq中证明All时遇True目标，为何reflexivity可完成证明？

1. 拆解当前证明状态 #

你的证明上下文和目标含义如下：

• T : Type：声明了一个任意类型T（可以是自然数、列表等任何类型）
• P : T -> Prop：P是T上的一个谓词——给每个T类型的元素，都指派了一个命题
• H : forall x : T, False -> P x：这是一个空真假设，意思是“对任意x，如果False成立，则P x成立”。因为False本身没有任何证明，所以这个命题天然成立，而且它和你当前的目标无关。
• 目标True：你需要证明的是Coq里的恒真命题。

2. True命题的本质 #

在Coq的构造逻辑中，True是一个最简单的恒真命题，它的定义只有一个构造子I，即：

Inductive True : Prop := I : True.

也就是说，只要能构造出I这个项，就完成了True的证明——I本身就是True的唯一证明。

3. 为什么reflexivity能完成证明？ #

通常reflexivity是用来证明等式（比如n = n），它会自动调用等式的自反性构造子eq_refl。但Coq的策略有一定的适配性：当目标是True这种不需要任何前提就能直接构造证明的命题时，reflexivity会尝试匹配目标的构造子，自动生成I来完成证明。

其实更直接的策略是用exact I或者trivial，但reflexivity在这里也能工作，本质是它的底层逻辑会处理这种无前提的简单恒真目标。

内容的提问来源于stack exchange，提问作者bluesquare