coq - (true=true) 的所有证明都一样吗？

Question

我可以在 Coq 中证明以下内容吗？

Lemma bool_uip (H1 : true = true): H1 = eq_refl true.

即true = true 的所有证明都相同吗？

例如 forall c (H1 H2: c = true), H1 = H2.

最好不要添加任何公理(如 UIP)。我发现以下线程表明可能是这种情况:

Proof in COQ that equality is reflexivity

Answer 1

这是一个用显式术语写成的证明。

Definition bool_uip (H1 : true = true): H1 = eq_refl true :=
  match H1 as H in _ = b
        return match b return (_ = b) -> Prop with
               | true => fun H => H = eq_refl true
               | false => fun _ => False
               end H with
  | eq_refl => eq_refl
  end.

H1 : true = _ 的类型具有一个索引 ( _)。模式匹配通过首先将该类型概括为 true = b 来进行( in 子句)，并实例化索引 b在每个分支机构。

要克服的主要障碍是这种泛化 H1 : true = b使结果类型为 H1 = eq_refl true不再是类型良好的(两侧有不同的类型)。解决方案是在 b 上进行模式匹配重新调整类型(在一个分支中；另一个分支未使用，实际上我们可以放置任何东西而不是 False)。

只要“equalees”(这里是 true 类型 bool )的类型是可判定的，我们就可以使用相同的技术来证明身份证明的唯一性。