(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)会很高兴.我发现以下线程表明可能是这种情况:

在COQ中证明平等是反身性

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)的类型是可判定的,我们就可以使用相同的技术来证明身份证明的唯一性.