如何显示函数的内射性?

问题描述 投票:0回答:1

以下是我要证明的内容: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 = n + p用于任意n m p的事实。

Coq的内置策略injectioncongruence看起来都很有希望,但它们仅适用于构造函数。

我尝试了以下策略,并不断遇到奇怪的错误或陷入困境:

  • 为归纳(n + m = s)的证明:归纳(n m s)]的归纳类型]] >>

  • 在显示congruence的引理中使用Sum (n m s) = Sum (n p s)策略>

  • 使用构造Sum s,destruct,以及引理表明n + m = n + p

  • 有没有更简单的方法来证明这一点?我觉得我必须缺少一些内置策略,或者使用unfold时有些诡计。

    [这就是我要证明的:定理add_n_injective:全部n m p,n + m = n + p-> m = p。加号(+)表示,如https://softwarefoundations.cis.upenn.edu/lf-current / ...

plus的内射性不是“基本”陈述,因为plus函数可以是任意的(且非内射性)

我想说标准证明确实需要在左引数上输入induction,实际上使用这种方法,证明很快就会遵循。

到达形式为injection的目标时,需要S (n + m) = S (n + p)才能得出内部相等性。

coq coq-tactic
1个回答
0
投票

plus的内射性不是“基本”陈述,因为plus函数可以是任意的(且非内射性)

© www.soinside.com 2019 - 2024. All rights reserved.