Coq：构建可判定 sigma 类型成员的最简单方法？

Question

考虑以下玩具开发：

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

我想创建一个函数，给定一个我个人认为是偶数的数字，returns 类型 EvenNat 的相应值，无需大惊小怪。

Example fortyTwo : EvenNat := mkEven 42.

Answer 1

我不确切知道你的假设是什么，但我想说的一种方法是使用 classes:

类型的自动化功能

Require Import Coq.Init.Specif.

Inductive IsEven : nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Class EvenClass n :=
  is_even : IsEven n.

Definition EvenNat := { n | EvenClass n }.

Lemma EvenClass_IsEven :
  forall n, EvenClass n -> IsEven n.
Proof.
  intros n h.
  exact h.
Qed.

#[export] Hint Extern 1 (EvenClass 0) =>
  apply is_even_z
  : typeclass_instances.

#[export] Hint Extern 1 (EvenClass (S (S ?n))) =>
  apply is_even_S ; apply EvenClass_IsEven
  : typeclass_instances.

#[export] Hint Extern 1 (EvenClass (proj1_sig ?x)) =>
  apply proj2_sig
  : typeclass_instances.

#[export] Hint Extern 4 (EvenClass ?n) =>
  my_decision_procedure
  : typeclass_instances.

我没有定义实例，而是使用 Hint Extern 机制来注入我想要解决目标的任何策略。假设你有一个策略来决定你的属性你可以在那里使用它。自然数表示每个提示的“成本”，因此搜索将首先尝试应用成本最低的提示。

一旦你有了这个，你想要的功能就是

Definition mkEven (n : nat) {h : EvenClass n} : EvenNat :=
  exist _ n h.

然后只需写入 mkEven n 就会触发上述提示所述的证明搜索。

Definition ev := mkEven 42.

为了详细说明 Yves 的答案和我的答案之间的区别，我选择使用提示而不是 class 个实例，这样证明搜索就不会太贪心。

例如，当我真的想证明 EvenClass 0 时，我强制搜索只使用 is_even_z，如下例所示：

Goal exists n, EvenClass n.
Proof.
  eexists. Fail exact _.
Abort.

#[export] Instance foo : EvenClass 0.
Proof.
  exact _.
Qed.

Goal exists n, EvenClass n.
Proof.
  eexists. exact _.
Qed.

如您所见，在第一种情况下，我们将 EvenClass ?n 作为目标，因此证明搜索没有找到任何候选人。但是，如果我们将 0 案例添加为类型 class 实例，则通过统一 ?n 和 0 证明搜索将成功。我认为这对于手头的案例来说有点过分了，但是这两种解决方案都有它们的应用。

Answer 2

这个问题，正如最初所说，有一个明显的答案。

问题 A： 如果您的上下文中有一个 nat 类型的数字 n 和一个带有语句 IsEven n，如何构造EvenNat类型的对象？

你可以简单地构造一个EvenNat类型的对象，写下下面的表达式

exist _ n knowledge

或者，如果你真的想要明确：

exist IsEven n knowledge

这体现在下面的脚本中

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

Definition mkEven (n : nat) (knowledge : IsEven n) : EvenNat :=
  exist IsEven n knowledge.

题的另一种解读如下：

问题 B: 你如何从一个已知的常量（比如 42）构造一个 EvenNat 类型的对象，这个常量在肉眼看来显然是偶数？

这是我对 Theo Winterhalter 草拟的解决方案的详细阐述，完整使用了 classes 类型的设备。

Require Import Coq.Init.Specif.

Inductive IsEven: nat -> Prop :=
| is_even_z : IsEven 0
| is_even_S : forall n, IsEven n -> IsEven (S (S n)).

Definition EvenNat := {n | IsEven n}.

Definition makeEvenNat (n : nat) (knowledge : IsEven n) : EvenNat :=
  exist IsEven n knowledge.

Class EvenClass n : Prop :=
  is_even : IsEven n.

#[export] Instance evenClass0 : EvenClass 0.
Proof.
apply is_even_z.
Qed.

#[export] Instance evenClassS n {h : EvenClass n}  : EvenClass (S (S n)).
Proof.
apply is_even_S; exact h.
Qed.

(* Using curly braces for the second argument h here deserves an
  explanation. *)
Definition mkEven (n : nat) {h : EvenClass n} : EvenNat :=
  exist IsEven n h.

Definition ev42 := mkEven 42.

Lemma ev42P : proj1_sig ev42 = 42.
Proof. easy. Qed.

Lemma IsEven42 : IsEven 42.
Proof. exact (proj2_sig ev42). Qed.

mkEven定义中使用大括号的解释是 mkEven 实际上需要 2 个参数，但是第二个不是用户编写的：它必须使用类型 class 推理机制自动构造。此证明必须成功才能真正定义对象。

ev42的定义就是问题B的答案。请注意，依赖于 mkEven 3 的定义将失败，因为无法找到 3 为偶数的证据。

Fail Definition ev3 := mkEven 3.

此代码已使用 coq.8.15.0 进行测试。

Coq：构建可判定 sigma 类型成员的最简单方法？

Coq: easiest way to construct members of a decidable sigma type?

coq