Coq：创建布尔值和nat的超类型

Question

我想创建混合类型的列表boolean和nat。此列表必须包含某些超类型的元素：boat每个boolean都是a boat，每个nat都是a 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).

定义此超类型或显示引理的正确方法是什么？

Answer 1

您也可以直接使用(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库中得到证明，但仅为此目的可能不值得安装。