Coq 中是否有任何策略可以将 bool 表达式转换为 Prop 表达式？答案

【问题标题】：is there any tactic in Coq that can transform a bool expression to a Prop one?Coq 中是否有任何策略可以将 bool 表达式转换为 Prop 表达式？
【发布时间】：2020-09-29 20:18:21
【问题描述】：

例如，我在我的上下文中有这个假设：

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 来修改的，因为我第一次从上下文中读取它时出错了。

【问题讨论】：

如果您在文件中启用Set Printing Coercions.，您的目标会改变吗？
不，它不会改变。
我要做的是最终destruct Heq as (HeqA & HeqB & HeqC) 来证明a = b、c = d 和e = f 三个子目标。应该没那么复杂吧？问题是我无法使用当前 bool 类型的格式来破坏 Heq。
奇怪的是它没有改变，因为你不能直接断言一个假设的类型为bool。您提到的 Is_true 函数在某些 Coq 库中被声明为强制转换，这导致 Coq 在需要将布尔值转换为命题时使用它。默认情况下不显示这些强制，我提到的选项应该显示它们。如果没有强制，假设就不会进行类型检查...
这可能与 Heq 加载到上下文中的方式有关吗？我正在展开一个具有if (a =? b) && (c =? d) && (e =? f) then ... else ... 表达式的函数，而这个Heq 来自于破坏if，如destruct ((a =? b) && (c =? d) && (e =? f)) eqn:Heq.

标签： coq proof coq-tactic formal-verification

【解决方案1】：

我已经解决了：

apply Bool.andb_true_iff in Heq.

将 = true 添加到最后两个布尔表达式，并将第二个&& 替换为/\。

然后我将Heq 表达式拆分为两个子表达式：

destruct Heq as (HeqA & HeqB).

并对剩下的左 bool 子表达式做了同样的事情：

apply Bool.andb_true_iff in HeqA. 
destruct HeqA as (HeqA & HeqC).

最后，我通过以下方式将 bool 等式转换为 Prop 等式：

apply beq_nat_true in HeqA.
apply beq_nat_true in HeqB.
apply beq_nat_true in HeqC.

【讨论】：