Coq：创建 boolean 和 nat 的超类型

Question

我想创建一个 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).

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

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 库中得到证明，但可能不值得为此安装。

Coq：创建 boolean 和 nat 的超类型

Coq: Create a super-type of boolean and nat

mixed

types

coq