plus
的内射性不是“基本”陈述,因为plus
函数可以是任意的(且非内射性)
以下是我要证明的内容: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的内置策略injection
和congruence
看起来都很有希望,但它们仅适用于构造函数。
我尝试了以下策略,并不断遇到奇怪的错误或陷入困境:
为归纳(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)
才能得出内部相等性。
plus
的内射性不是“基本”陈述,因为plus
函数可以是任意的(且非内射性)