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.