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

您通常无法证明两个 Props的相等性。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.

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

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

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