n m : nat
在 Coq 中表示相邻偶数的一种可能方式是归纳定义该关系,从 0 和 2 开始。
Inductive adj_ev : nat -> nat -> Prop :=
| ae_0 : adj_ev 0 2
| ae_1 : forall ( n m : nat ), adj_ev n m -> adj_ev m ( S ( S m ) )
| ae_2 : forall ( n m : nat ), adj_ev n m -> adj_ev m n.
ae_0
说明 0 和 2 是相邻的偶数。ae_1
指出如果一些n m : nat
是相邻的偶数,那么m
和 也是m + 2
。使用这两个构造函数,我们可以覆盖所有相邻偶数对,直到无穷大。可是等等!这适用于n
且m
当且仅当n < m
。所以我们需要最后一个构造函数ae_2
来翻转关系中的任何给定数字对。
现在我已经定义了关系,我想对其进行一些健全性检查以确保它有效。例如,我知道 1 和 3 不是相邻的偶数,我也知道adj_ev 1 3
从我定义的方式中永远无法得到adj_ev
。所以我肯定可以证明,~ ( adj_ev 1 3 )
对吧?
Theorem test' : ~ ( adj_ev 1 3 ).
unfold not. intros H.
inversion H. inversion H0.
经过几次反转后,我很快陷入了无限循环。就好像我在问 Coq,“如何才能相邻且均匀?n
” m
Coq 回答“嗯,也许m
andn
是相邻的,甚至是……”然后我问,“and 是如何m
相邻的n
,甚至是?” Coq 说“嗯,也许n
和m
是相邻的,甚至是……” 无穷无尽。
普遍的问题是,当你有一些归纳定义的对称关系R
时,很容易证明它R
在它真正成立的地方成立,但很难证明它在它不成立的地方不成立。也许有比inversion
在这种情况下提取矛盾更好的策略,但我不确定它可能是什么。
有什么想法吗?