coq - 证明中生成了奇怪的目标 `Some 0 = true`

Question

考虑这个玩具 Coq 问题 ( CollaCoq ):

Require Import ssreflect ssrfun ssrbool.
Require Import Unicode.Utf8.

Definition optfun (n: nat) : option nat :=
    match n with
    | 0 => Some 0
    | _ => None
    end.

Definition boolfun (n: nat) : bool :=
    match n with
    | 0 => true
    | _ => false
    end.

Lemma lem : ∀ n, isSome (optfun n) = boolfun n.
Proof.
    intro. unfold optfun, boolfun. destruct n.

我的目标是在 optfun 返回 Some 时让 boolfun 为真，并在引理中证明这一点。

但是，在给出证明步骤之后，当前的子目标是Some 0 = true。

我认为这样的命题甚至不应该进行类型检查，因为我希望 Some 0 是 option nat 和 true 类型为 bool 类型。为什么会这样？我的 optfun、boolfun 或 lem 有问题吗？

Answer 1

如果我们运行 Set Printing Coercions.，我们可以看到所有 implicit coercions在我们的表达式中(默认情况下，Coq 隐藏它们)。在我们的例子中，目标变为 isSome (Some 0)，因为 SSReflect 在 option 和 bool 之间添加了强制转换。通过运行 Set Coercion Paths option bool.，我们看到 isSome 本身就是有问题的强制(参见标准库的 this 部分)。