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.

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

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

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

标签： coq

Answer 1

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