我可以在 Coq
中证明以下内容吗?
Lemma bool_uip (H1 : true = true): H1 = eq_refl true.
即true = true
的所有证明都相同吗?
例如 forall c (H1 H2: c = true), H1 = H2.
最好不要添加任何公理(如 UIP)。我发现以下线程表明可能是这种情况:
最佳答案
这是一个用显式术语写成的证明。
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
)的类型是可判定的,我们就可以使用相同的技术来证明身份证明的唯一性。
关于coq - (true=true) 的所有证明都一样吗?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/50847669/