Вычисление Eval является неполным, когда в Coq используется собственная разрешимость

Question

Eval compute Команда не всегда оценивается как простое выражение. Рассмотрим код:

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Qed.

И, если я выполню следующую команду:

Eval compute in (if (In_dec eq_nat_dec 10 [3;4;5]) then 1 else 2).

Coq говорит мне, что результат 2, Тем не менее, когда я выполняю следующее выражение:

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

Я получаю длинное выражение, в котором In-предикат кажется развернутым, но результат не дается.

Что я должен изменить, чтобы получить ответ 1 напоследок Eval compute линия?

Answer 1

В Coq есть две команды-терминатора для корректных скриптов: Qed а также Defined, Разница между ними заключается в том, что первое создает непрозрачные термины, которые нельзя развернуть даже Eval compute, Последнее создает прозрачные условия, которые затем можно развернуть как обычно. Таким образом, вы просто должны поставить Defined в месте Qed.:

Require Import Coq.Lists.List.
Require Import Coq.Arith.Peano_dec.
Import ListNotations.

Inductive I : Set := a : nat -> I | b : nat -> nat -> I.

Lemma I_eq_dec : forall x y : I, {x = y}+{x <> y}.
Proof.
  repeat decide equality.
Defined.

Eval compute in (if (In_dec I_eq_dec (a 2) [(a 1);(a 2)]) then 1 else 2).

Я лично нахожу тип сумбул {A} + {B} не очень хорошо для выражения разрешимых предложений, именно потому, что доказательства и вычисления слишком запутаны; в частности, доказательства влияют на то, как сокращаются сроки. Я считаю, что лучше следовать стилю Ssreflect, разделять доказательства и вычисления и связывать их через специальный предикат:

Inductive reflect (P : Prop) : bool -> Set :=
  | ReflectT of P : reflect P true
  | ReflectF of ~ P : reflect P false.

это дает удобный способ сказать, что логическое вычисление возвращает true, если какое-либо свойство имеет значение true. Ssreflect предоставляет поддержку для удобного переключения между вычислительным логическим представлением и логическим представлением.

Answer 2

Если вы хотите оценить свои доказательства, вы должны сделать их прозрачными. Вы делаете это, заканчивая их Defined команда. Qed команда делает их непрозрачными, то есть отбрасывает их вычислительное содержание.