时间戳

首页 > 解决方案 > 被证明卡住了

coq - 被证明卡住了

问题描述

我对 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不会给我足够的事实来消除某些情况。

标签： coq

解决方案

您需要首先正确地进行数学运算：找到两个彼此相反的函数。

您最初的意图是正确的：一侧是奇数，另一侧是偶数，但是您在每一侧存储的内容应该涵盖所有自然数，因此您可能必须在某个地方除以 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用于该目的。

推荐阅读