如何在 coq 中使用带有 sig 的强制

Question

我有这样的代码

Definition even := {n : nat | exists k, n = k + k}.

Definition even_to_nat (e : even) : nat.
Admitted.

Coercion even_to_nat : even >-> nat.

Example Ex : forall n : even, exists k, k + k = n.
Admitted.

Example Ex2 : forall k, exists n : even, k + k = n.
Admitted.

在这种情况下，我应该如何删除 Admitted？

还有，为什么

Example Ex' : forall n : even, exists k, n = k + k

强制还不行？有什么好的方法可以消除此类错误吗？

Answer 1

这是用 Gallina 编写的 even_to_nat 函数的定义：

Definition even := {n : nat | exists k, n = k + k}.

Definition even_to_nat (e : even) : nat :=
  match e with
  | exist _ n _ => n
  end.

Coercion even_to_nat : even >-> nat.

它在 e 上进行模式匹配以检索包装的自然数 n。

这是使用策略的等效实现：

Definition even_to_nat_tac (e : even) : nat.
destruct e.
auto.
Defined.

destruct 策略本质上是 e 上的模式匹配。然后，auto自动使用里面的自然数完成定义。

这是第一个示例的 Gallina 实现：

Example Ex : forall n : even, exists k, k + k = n :=
  fun n => match n with
  | exist _ n (ex_intro _ k eq) => ex_intro (fun k => k + k = n) k (eq_sym eq)
  end.

本质上，它在 n 上进行模式匹配，检索 k 和 n = k + k 的证明，然后使用 eq_sym 翻转等式。

这是 Ex2 的实现：

Example Ex2 : forall k, exists n : even, k + k = n :=
  fun k =>
  let n := k + k in
  let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
  let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
  ex_intro (fun n => k + k = even_to_nat n) even_nat eq_refl.

exists_k是偶数exists k, n + n = k中的证明。 even_nat是满足条件exists n, k + k = n的偶数，其中n显然是k + k。最后，我居住在所需的类型中。好像不能在这里使用强制转换，所以我明确使用 even_to_nat.

或者，如果我添加类型注释，强制转换会起作用：

Example Ex2 : forall k, exists n : even, k + k = n :=
  fun k =>
  let n := k + k in
  let exists_k := ex_intro (fun k => n = k + k) k eq_refl in
  let even_nat := exist (fun n => exists k, n = k + k) n exists_k in
  ex_intro (fun (n : even) => k + k = n) even_nat eq_refl.

对于您的 Ex' 示例，请参阅 this example from the coercion documentation 中的警告。给定强制 Coercion bool_in_nat : bool >-> nat.:

Note that Check (true = O) would fail. This is "normal" behavior of coercions. To validate true=O, the coercion is searched from nat to bool. There is none.

您只能在相等类型的右侧进行强制转换，而不能在左侧进行强制转换。

如何在 coq 中使用带有 sig 的强制

How to use coercion with sig in coq

coercion

coq