如何解决卡住了证明
我对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.
我有主意,但我无法实现它,也不知道这是否可行。基本上,我想将每个奇数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
并不能给我足够的事实来消除某些情况
解决方法
首先需要正确地进行数学运算:找到两个互为逆的函数。
您最初的意图是正确的:一侧是奇数,另一侧是偶数,但是您在每一侧存储的内容应该覆盖所有自然数,因此您可能必须在某处除以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
的特定归纳定理。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。