Блог

Рассмотрим эту проблему с игрушечным 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.
 

Моя цель здесь состояла в том, чтобы boolfun быть истинным всякий optfun раз, когда возвращается некоторое, и доказать это в лемме.

Однако после приведенных шагов доказательства текущая подцель такова Some 0 = true .

Я подумал, что подобное предложение не должно даже проверять тип, потому что я ожидал Some 0 бы, что оно будет типичным option nat и true будет типичным bool . Почему это происходит? Что-то не так с моим optfun , boolfun или lem ?

Если мы запустим Set Printing Coercions. , мы сможем увидеть все неявные принуждения в нашем выражении (по умолчанию Coq скрывает их). В нашем случае цель превращается в isSome (Some 0) , потому что SSReflect добавляет принуждение между option и bool . Запустив Set Coercion Paths option bool. , мы видим, что isSome само по себе является рассматриваемым принуждением (см. Эту часть стандартной библиотеки).