Coq: создать супер-тип логического и нат - PullRequest
Новая
       33

Coq: создать супер-тип логического и нат

3 голосов
/ 09 июля 2019

Я хочу создать список смешанных типов boolean и nat. Этот список должен содержать элементы некоторого супертипа: boat, где каждый boolean является boat, а каждый nat является boat.

Проблема, с которой я столкнулся, заключается в том, что этот супертип boat должен иметь boat_eq_dec, что означает, что должен быть способ решить, являются ли два boat одинаковыми или разными. Поскольку nat и boolean оба имеют такое решение по равенству, у супертипа также должен быть один.

В приведенном ниже примере я создал супертип, но не могу показать лемму, решающую равенство Lemma boat_eq_dec : forall x y : Boat, {x = y} + {x <> y}.

Inductive Boat : Set :=
  | is_bool (inp: bool)
  | is_nat (inp: nat).

Как правильно определить этот супертип или показать лемму?

1 Ответ

5 голосов
/ 09 июля 2019

Вы также можете напрямую использовать (bool + nat)%type (используя sum), чтобы получить общее представление. Тогда decide equality может решить несколько eq_dec целей. 

Definition boat := (bool + nat)%type.

Lemma boat_eq_dec :
  forall x y : boat, {x = y} + {x <> y} .
Proof.
  intros x y. decide equality.
  all: decide equality.
Defined.

Вы могли бы даже рассмотреть доказательство общей леммы 

forall A B,
  (forall x y : A, {x = y} + {x <> y}) ->
  (forall x y : B, {x = y} + {x <> y}) ->
  forall x y : A + B, {x = y} + {x <> y}.

Это уже доказано в библиотеке Equations, но, вероятно, не стоит устанавливать только для этого.

...