如何显示函数的单射性？

Question

我要证明的是：Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.

+ 是 plus 的表示法，定义为 https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html:

Fixpoint plus (n : nat) (m : nat) : nat :=
  match n with
    | O ⇒ m
    | S n' ⇒ S (plus n' m)
  end.

在 Agda 中，可以 cong (n + _) 对任何 n m p n + m = n + p 使用这一事实。

Coq 的内置策略 injection 和 congruence 看起来都很有前途，但它们只适用于构造函数。

我尝试了以下策略并不断遇到奇怪的错误或卡住：

做一个归纳类型来捆绑 (n + m = s) 的证明：Sum (n m s)
在显示 Sum (n m s) = Sum (n p s)

congruence

使用构造Sums、destruct和引理来证明n + m = n + p

有没有更简单的方法来证明这一点？我觉得一定有一些我缺少的内置策略或一些 unfold.

的诡计

更新

知道了：

Theorem add_n_injective : forall n m p, n + m = n + p -> m = p.
Proof.
  intros. induction n.
  - exact H.
  - apply IHn.  (* goal: n + m = n + p *)
    simpl in H. (* H: S (n + m) = S (n + p) *)
    congruence.
Qed.

谢谢@ejgallego

Answer 1

plus 的内射性不是 "elementary" 陈述，因为 plus 函数可以是任意的（非内射的）

我想说标准证明确实需要 induction 在左边的论证上，实际上使用这种方法很快就会得到证明。

当您达到 S (n + m) = S (n + p) 形式的目标时，您将需要 injection 来推导内在平等。

如何显示函数的单射性？

How to show injectivity of a function?

coq

coq-tactic