Классы типов с несколькими полями против одного поля в Coq / Неожиданное поведение команды Compute - PullRequest
Новая
       30

Классы типов с несколькими полями против одного поля в Coq / Неожиданное поведение команды Compute

3 голосов
/ 18 мая 2019

Я изучаю классы типов в Coq с книгой Software Foundations.

Запуск следующего: 

Class Eq A :=
{
eqb: A -> A -> bool;
}.

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) => 
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.

Compute (true =? false).

Я получаю сообщение = false : bool, как и ожидалось. Но если я сделаю следующее вместо этого, 

Class Eq A :=
{
eqb: A -> A -> bool;
eqb_refl: forall (x : A), eqb x x = true;
}.

Notation "x =? y" := (eqb x y) (at level 70).

Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) => 
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.
Proof.
  intros []; reflexivity.
Qed.

Compute (true =? false).

Я получаю сообщение = (let (eqb, _) := eqBool in eqb) true false : bool. Кажется, я не могу упростить это выражение и не уверен, что пошло не так и где. Как я могу определить приведенный выше класс типов с помощью дополнительной гипотезы и при этом иметь возможность использовать определенный мной экземпляр (т.е. получить то же сообщение, что и раньше)?

Большое спасибо!

1 Ответ

3 голосов
/ 18 мая 2019

Команда Qed создает непрозрачные определения, которые никогда не раскрываются такими командами, как Compute.Вы можете указать Coq сделать непрозрачным только обязательство по доказательству, используя команду Program Instance: 

Require Import Coq.Program.Tactics.

Class Eq A :=
{
eqb: A -> A -> bool;
eqb_refl: forall (x : A), eqb x x = true;
}.

Notation "x =? y" := (eqb x y) (at level 70).

Program Instance eqBool : Eq bool :=
{
eqb := fun (b c : bool) =>
   match b, c with
     | true, true => true
     | true, false => false
     | false, true => false
     | false, false => true
   end
}.
Next Obligation. now destruct x. Qed.

Compute (true =? false).
...