如何解决Coq以排除的前提条件进行销毁
我正在与softwarefoundations book学习Coq,并且陷入了induction chapter的最后一项任务-练习:5星,高级(binary_inverse)c部分。
给出下一个定义
Inductive bin : Type :=
| Z
| B0 (n : bin)
| B1 (n : bin).
Fixpoint norm_bin (input :bin): bin :=
match input with
| Z => Z
| B0 Z => Z
| B1 restInput => B1 (norm_bin restInput)
| B0 restInput=> match norm_bin restInput with
| Z => Z
| _ => B0 (norm_bin restInput)
end
end.
我正试图证明
Theorem norm_bin_B0_out :
forall b,norm_bin b <> Z -> norm_bin (B0 b) = B0 (norm_bin b).
我尝试destruct b
,但根据条件b = Z
无法解决案件norm_bin b <> Z
,b
不能为Z
。我如何证明呢?预先感谢!
由于下面的回复,我设法证明了这一点:
Theorem norm_bin_B0_out :
forall b,norm_bin b <> Z -> norm_bin (B0 b) = B0 (norm_bin b).
Proof.
intros b H.
simpl.
destruct norm_bin eqn:f.
- simpl in H. tauto.
- simpl. destruct b.
{ discriminate. }
{ reflexivity. }
{ reflexivity. }
- destruct b.
{ discriminate. }
{ reflexivity. }
{ reflexivity. }
Qed.
我不知道norm_bin可以被破坏。那是个问题。
解决方法
当假设H
是一个否定词(例如~A
),但是您知道可以证明被否定的公式(可以证明A
)时,那么好的要执行的步骤是case H
,这将导致您必须证明A
的目标。
在确认这不是SF书中的练习之后,我决定为您提供更多帮助。
您的语句norm_bin (B0 b)
中的公式可以通过simpl
策略进行符号执行计算。做到这一点。
在此步骤之后,您将看到一个包含2个match语句的表达式。其中之一是b
上的match语句,另一个是norm_bin b
上的match语句。然后,您的下一步可以是destruct
上的b
,但是也可以是destruct
上的norm_bin
。尝试两种路线,但如果选择后者,请使用eqn:
destruct
策略的变体。
如果您希望下一步是在b
上执行销毁操作,那么问题是您得到了将norm_bin
应用于(B0 (B0 ...)
的表达式。通过此公式对目标使用simpl
会导致过多的计算。您需要通过使用change
而不是simpl
来解决这个问题,并写下自己认为最适合自己需求的中间计算内容。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。