如何在Coq中实现开式？

Question

如何在Coq中实现开放公式？我认为Coq的 Prop 意思是封闭式，但我也想使用开放式，如 x = 0. 如果有的话 x 是在 R.

Check x = 0.
(* The reference x was not found in the current environment. *)

Answer 1

也许你可以定义一个任意变量x而不实例化它，如。

Variable x:nat.
Check x = 0.

Answer 2

"开放 "公式在Coq和纸笔逻辑中都没有意义 除非你有一个环境来解释变量。Check term 确实需要一个闭合项，所以你必须为以下变量指定一个绑定 x例如 exists x, x = 0.