1

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” mCoq 回答“嗯，也许mandn是相邻的，甚至是……”然后我问，“and 是如何m相邻的n，甚至是？” Coq 说“嗯，也许n和m是相邻的，甚至是……” 无穷无尽。

普遍的问题是，当你有一些归纳定义的对称关系R时，很容易证明它R在它真正成立的地方成立，但很难证明它在它不成立的地方不成立。也许有比inversion在这种情况下提取矛盾更好的策略，但我不确定它可能是什么。

有什么想法吗？

4

1 回答 1

1

首先我尝试induction了一些额外的方程，但这还不够。

Goal forall n1 n2, adj_ev n1 n2 -> n1 = 1 -> n2 = 3 -> False.
Proof. induction 1. Abort.

我设法通过首先证明两个相邻的偶数是偶数来证明你的定理。

使用等价关系启用重写。

Require Import Coq.Setoids.Setoid.

使用时关闭证明搜索firstorder。只允许简化。

Set Firstorder Depth 0.

创建与、或Hints一起使用的提示数据库。autoautorewriteautounfold

Create HintDb Hints.

常用战术的简写。

Ltac simplify := repeat (firstorder || subst || autorewrite with Hints in *).

Inductive even : nat -> Prop :=
  | even_0 : even 0
  | even_S : forall n1, even n1 -> even (S (S n1)).

很简单。

Conjecture C1 : even 0 <-> True.
Conjecture C2 : even 1 <-> False.
Conjecture C3 : forall n1, even (S (S n1)) <-> even n1.

Hint Rewrite C1 C2 C3 : Hints.

Theorem T1 : forall n1 n2, adj_ev n1 n2 -> even n1 /\ even n2.
Proof. induction 1; simplify. Qed.

Goal ~ adj_ev 1 3. Proof. intro H1. apply T1 in H1. simplify. Qed.

你也可以定义

Definition least : (nat -> Prop) -> nat -> Prop := fun p1 n1 => p1 n1 /\ (forall n2, p1 n2 -> n2 >= n1).

Definition greatest : (nat -> Prop) -> nat -> Prop := fun p1 n1 => p1 n1 /\ (forall n2, p1 n2 -> n2 <= n1).

Definition even : nat -> Prop := fun n1 => exists n2, n1 = 2 * n2.

Definition least_greater_even : nat -> nat -> Prop := fun n1 => least (fun n2 => n2 > n1 /\ even n2).

Definition greatest_less_even : nat -> nat -> Prop := fun n1 => greatest (fun n2 => n2 < n1 /\ even n2).

Definition adjacent_even : nat -> nat -> Prop := fun n1 n2 => least_greater_even n1 n2 /\ greatest_less_even n2 n1 \/ greatest_less_even n1 n2 /\ least_greater_even n2 n1.

并从那里开始工作。还有其他定义谓词的方法。

Inductive adj_ev : nat -> nat -> Prop :=
  | adj_ev_0_2 : adj_ev 0 2
  | adj_ev_2_0 : adj_ev 2 0
  | adj_ev_S_S : forall n1 n2, adj_ev n1 n2 -> adj_ev (S (S n1)) (S (S n2)).

Goal ~ adj_ev 1 3. Proof. inversion 1. Qed.
于 2014-07-16T13:27:33.503 回答