Coq可判定不等性的证明无关性及相关命题无公理证明问询

首先你的两个目标确实等价：Coq中~false即false -> False，和你给出的false <> true（即false = true -> False）的证明无关性论证逻辑完全一致。
结论是：在不引入证明无关性公理的前提下，该目标可以构造性证明，但需要依赖函数外延性公理，如果要求完全不使用任何公理，标准Coq默认规则下无法证明。

• 你提到的bool_irrelevance是Hedberg定理的直接推论：Hedberg定理明确，所有满足你给出的可判定相等性定义{x = y} + {x <> y}的类型，都天然满足唯一恒等性（UIP），即同一相等命题的任意两个证明都相等。bool作为可判定相等的基础归纳类型，forall (b:bool) (p q: b = true), p = q的证明完全不需要任何公理。
• 你的待证目标讨论的是否定命题~P（此处P为false或false = true）的证明无关性：~P本质是P -> False的函数类型，标准Coq默认规则下要证明两个函数相等，需要用到函数外延性公理（即若两个函数对所有输入的输出都相等，则函数本身相等），不需要用到证明无关性公理。
  • 对于~P的特殊场景，当P是不可满足命题时，对任意输入x:P，可以通过空类型消去规则直接得到a x = b x，结合函数外延性即可直接推出a = b。
• 在Ssreflect搭配数学组件库的常用环境中，默认启用函数外延性公理，因此该目标不需要用到证明无关性公理即可完成证明，符合你的预期。

结论是：不需要证明无关性公理即可证明，仅需要函数外延性公理；如果允许使用Coq的严格命题（sProp）扩展，甚至不需要任何公理即可实现。

• False -> False的所有证明都是空类型到空类型的函数，对于任意两个该类型的函数f、g，对任意输入x:False，可以通过False的归纳原理直接得到f x = g x，结合函数外延性即可得到f = g，整个过程完全没有用到证明无关性公理。
• 如果要求完全不使用任何公理，标准Coq的基础类型论没有提供函数相等的判定规则，因此无法构造该命题的证明；但如果将False -> False声明为sProp类型，利用sProp内置的证明无关性规则，不需要任何公理即可得到该结论。

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