coq - 某个数字加 1 的证明会改变 Coq 中的奇偶校验

Question

我将 Even 定义为:

Inductive even : nat -> Prop :=
  | ev0: even O
  | evSS: forall n, even n -> even (S (S n)).

但现在我想证明:

Lemma add1_diff (x: nat) : even (S x) = ~even x.

我可以证明:

even (S O) = (~ even O)

提前致谢。

Answer 1

您通常无法证明两个 Prop 的相等。 Prop 中的相等意味着逻辑陈述的证明项是相等的。有时会出现这种情况，但很少见。以下是一些示例:

Require Import PeanoNat.
Import Nat.

Inductive even : nat -> Prop :=
  | ev0: even O
  | evSS: forall n, even n -> even (S (S n)).

Example ex1 (n : nat) : (n >= 1) = (1 <= n).
Proof.
  (* The proofs are equal because >= is defined in terms of <= *)
  reflexivity.
Qed.

Example ex2: even (2+2) = even 4.
Proof.
  (* The proofs are equal because 2+2 can be reduced to 4 *)
  reflexivity.
Qed.

Example ex3 (n : nat) : even (2+n) = even (n+2).
Proof.
  (* The proofs are equal because 2+n is equal to n+2 *)
  rewrite add_comm.
  reflexivity.
Qed.

Example ex4 (n : nat): even (S (S n)) = even n.
Proof.
  (* The proofs cannot be equal, because the left side proof always
     requires one evSS constructor more than the right hand side. *)
Abort.

出于这个原因，我们使用两个 Prop 的等价性，即 <-> ，而不是平等。最后一条语句的等价性是可证明的:

Example ex4 (n : nat): even (S (S n)) <-> even n.
Proof.
  split; intros H.
  - inversion H.
    assumption.
  - constructor.
    assumption.
Qed.

所以回答你的问题:两个陈述的相等性很可能无法证明，但等价性是可以证明的。如果您需要帮助，请询问。