如何解决Coq无法统一-如何更改假设?
Coq初学者在这里。
我有以下愚蠢的定理:
Theorem plus_same : forall a b c : nat,a+b=a+c -> b=c.
Proof. Admitted.
Theorem advanced_commutivity:
forall x y z w : nat,x + y + (z+w) = x + z + (y + w).
Proof.
intros x y z w.
apply (plus_same x (y + (z+w)) (z + (y + w))).
但是,当我尝试运行apply
行时,出现错误:
Unable to unify "y + (z + w) = z + (y + w)" with
"x + y + (z + w) = x + z + (y + w)".
我需要在这里更改我的假设吗?如何在此处将plus_same
应用于advanced_commutivity
证明中的论点?
解决方法
您误解了目标:.....com....
代表x + y + (z + w)
,因为(x + y) + (z + w)
已注册为左关联,与+
不同。
因此,为了应用引理,您应该首先通过与另一个x + (y + (z + w))
重写来重新关联+
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。