被证明卡住了

Question

我对 Coq 还很陌生，我在 CodeWars 上做了一些 Katas 来娱乐和学习。

我被其中一个困住了，想听听你的一些想法。

所以，我有：

Record iso (A B : Set) : Set :=

bijection {

A_to_B : A -> B;

B_to_A : B -> A;

A_B_A : forall a : A, B_to_A (A_to_B a) = a;

B_A_B : forall b : B, A_to_B (B_to_A b) = b

}.


(* nat_plus_nat : a set having size(nat) more elements than nat. (provided in preloaded) *)
Inductive nat_plus_nat : Set := left (n : nat) | right (n : nat).


Theorem nat_iso_natpnat : iso nat nat_plus_nat.

我有和idea，但是不能实现，不知道是否可行。基本上，我想将每个奇数 nat 映射到一个构造函数（例如，左），并将每个偶数 nat 映射到另一个（例如，右）。这行得通吗？如果没有，怎么办？

现在我坚持这样一个事实，即 A_to_B 定义为 fun n => if odd n then left n else right n 和 B_to_A 定义为 fun n => match n with | left n' => n' | right n' => n' end 不会给我足够的事实来消除某些情况。

Answer 1

您需要先正确地进行数学运算：找到两个互为逆的函数。

您最初的意图是正确的：一侧是奇数，另一侧是偶数，但是您在每一侧存储的内容应该涵盖所有自然数，因此您可能必须在某个地方除以 2。

对于 Coq 的使用，您应该从以下行开始加载 Arith 包：

Require Import Arith.

这样，您可以从现有函数中受益，例如 Nat.div2 和 Nat.even 以及所有关于它们的现有定理。为了找到相关的定理，我建议使用如下命令：

Search Nat.even 2.
Search Nat.div2.

最后提示：通过归纳证明Nat.div2 的属性对于初学者来说相当困难。尽量使用现有的定理。如果您选择对div2 进行归纳证明，请查看文件theories/Arith/Div2.v 中的源代码：该文件的作者为此设计了一个名为ìnd_0_1_SS 的特定归纳定理。