证明中生成的奇怪目标“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 returns a Some 时让 boolfun 为真，并在引理中证明这一点。

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

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

Answer 1

如果我们运行Set Printing Coercions.，我们可以看到标准库的所有implicit coercions in our expression (by default, Coq hides them). In our case, the goal turns into isSome (Some 0), because SSReflect adds a coercion between option and bool. By running Set Coercion Paths option bool., we see that isSome itself is the coercion in question (see this部分。

证明中生成的奇怪目标“Some 0 = true”

Weird goal `Some 0 = true` generated in proof

coq