Coq 信息理论 %B is_true
Coq infotheo %B is_true
我用一个证明撞墙了（Coq 版本 8.13.1，使用 infotheo），其中上下文假设是目标，只是附加了一个“%B”。我理解它表示'is_true'，但如何进行证明？
（展开is_true不去掉“%B”，重写H并应用H不起作用）。
A: finType
B: eqType
i: B
i0: A
X: A -> B
H: (X i0 == i)%B
===
(1/1)
X i0 = i
感谢任何建议。
%B 表示这是在不同的范围内解析的。等号在 H 和目标中意味着不同的东西。它是 == vs = btw.
您可以关闭符号以查看这两个术语的真正含义。
== 可能比 = 弱。
感谢您的回答。
问题已解决：
move/eqP in H.
apply H.
Qed.
我用一个证明撞墙了（Coq 版本 8.13.1，使用 infotheo），其中上下文假设是目标，只是附加了一个“%B”。我理解它表示'is_true'，但如何进行证明？
（展开is_true不去掉“%B”，重写H并应用H不起作用）。
A: finType
B: eqType
i: B
i0: A
X: A -> B
H: (X i0 == i)%B
===
(1/1)
X i0 = i
感谢任何建议。
%B 表示这是在不同的范围内解析的。等号在 H 和目标中意味着不同的东西。它是 == vs = btw.
您可以关闭符号以查看这两个术语的真正含义。
== 可能比 = 弱。
感谢您的回答。 问题已解决：
move/eqP in H.
apply H.
Qed.