如何解决使用 Coq 证明加法函数是关联的
我试图证明预定义的加法函数是关联的,但我被困在目标读取的步骤
"plus (S x') (plus y z) = plus (plus (S x') y) z",
但我唯一的假设是
"IHx' : forall y z : nat,加x'(加y z)=加(加x' y)z"
解决方法
此时您应该使用函数 plus 的定义,例如使用函数来评估您的目标,例如 cbn
(simpl
或 lazy
也可能有效)。然后,您将获得一个应用归纳假设的目标,这样您就可以完成 congruence.
顺便说一下,x = 0
的基本情况可以简单地通过计算解决,所以 reflexivity
就足够了。
您已经证明了 plus 0 x = x
,但您也可以(轻松)证明 plus (S x) y = S (plus x y)
。如果你这样做,你可以把你的目标改写成
S (plus x' (plus y z)) = S (plus (plus x' y) z)
然后你可以用你的归纳假设重写。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。