如何解决Coq中有什么策略可以将布尔表达式转换为Prop表达式?
例如,在我的上下文中我有这个假设:
Heq: (a =? b) &&
(c =? d) &&
(e =? f) = true
我想转变成这样:
Heq: (a = b) /\
(c = d) /\
(e = f)
我看过这篇文章
coq tactic for replacing bools with Prop
但是使用这些策略对我来说并不是真正的直截了当,因为在我的上下文中表达式中没有 Is_true
。
编辑:
Heq
通过添加 = true
进行了修改,因为我是第一次从上下文中读取它时犯了一个错误。
解决方法
我已通过以下方式解决了该问题:
apply Bool.andb_true_iff in Heq.
将 = true
添加到最后两个bool表达式中,并将第二个&&
替换为/\
。
然后我通过以下方式将Heq
表达式分为两个子表达式:
destruct Heq as (HeqA & HeqB).
并在剩余的左布尔子表达式上做同样的事情:
apply Bool.andb_true_iff in HeqA.
destruct HeqA as (HeqA & HeqC).
最后,我通过以下方式将布尔等式转换为Prop相等:
apply beq_nat_true in HeqA.
apply beq_nat_true in HeqB.
apply beq_nat_true in HeqC.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。