Coq证明出现Some 0 = true跨类型子目标的原因排查

问题原因 #

你定义的optfun、boolfun以及引理lem的逻辑表述都没有问题，问题根源是当前环境中isSome的定义不符合预期。

标准的isSome来自Coq.Init.Option标准库，类型为 forall A : Type, option A -> bool，作用是判断一个option类型的值是否为Some构造子，内部实现为：

Definition isSome (A:Type) (o:option A) :=
  match o with
  | Some _ => true
  | None => false
  end.

你当前的环境没有引入这个标准定义，存在的异常isSome定义会直接返回输入的option值本身，导致isSome (Some 0)被规约为Some 0，而非预期的布尔值true，才会出现option nat类型的Some 0和bool类型的true相等的反常子目标。

修复方案 #

只需要在代码开头引入标准库的Option模块，即可正常完成证明：

Require Import ssreflect ssrfun ssrbool.
Require Import Unicode.Utf8.
Require Import Coq.Init.Option. (* 引入标准isSome定义 *)

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.
    - simpl. reflexivity.
    - simpl. reflexivity.
Qed.

内容的提问来源于stack exchange，提问作者Sami Liedes