Weird goal `Some 0 = true` generated in proof

Question

Consider this toy Coq problem (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.

My goal here was to have boolfun be true whenever optfun returns a Some, and to prove that in the lemma.

However, after the proof steps given, the current subgoal is Some 0 = true.

I thought a proposition like that should not even type check because I'd expect Some 0 to be of type option nat and true to be of type bool. Why does this happen? Is there something wrong with my optfun, boolfun or lem?

Joshua Grosso Reinstate CMs Joshua Grosso Reinstate CMs · Accepted Answer · 2021-10-05T23:01:08

If we run Set Printing Coercions., we can see all the 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 part of the standard library).

Weird goal `Some 0 = true` generated in proof

1 Answers