数据类型转换函数需要很长时间来证明答案

【问题标题】：Datatype transformation function takes very long to proof数据类型转换函数需要很长时间来证明
【发布时间】：2019-05-24 11:26:18
【问题描述】：

Isabelle 需要很多时间来证明（在我看来）相当简单的数据类型转换函数的正确性。例如，我创建了数据类型来表示数学和布尔表达式以及简化此类表达式的函数。

datatype 'a math_expr =
  Num int |
  Add "'a math_expr" "'a math_expr" |
  Mul "'a math_expr" "'a math_expr" |
  Sub "'a math_expr" "'a math_expr" |
  Div "'a math_expr" "'a math_expr"

datatype 'a expr =
  True |
  False |
  And "'a expr" "'a expr" |
  Or "'a expr" "'a expr" |
  Eq "'a math_expr" "'a math_expr" |
  Ne "'a math_expr" "'a math_expr" |
  Lt "'a math_expr" "'a math_expr" |
  Le "'a math_expr" "'a math_expr" |
  Gt "'a math_expr" "'a math_expr" |
  Ge "'a math_expr" "'a math_expr" |
  If "'a expr" "'a expr" "'a expr"

function (sequential) simplify :: "'a expr ⇒ 'a expr" where
"simplify (And a True) = a" |
"simplify (And True b) = b" |
"simplify (Or a True) = True" |
"simplify (Or True b) = True" |
"simplify e = e"
by pat_completeness auto
termination by lexicographic_order

在我的笔记本上，Isabelle 需要相当长的时间来证明功能（突出显示签名和正文），甚至需要更多时间来证明其完整性（突出显示by pat_completeness auto）。所需的计算时间很大程度上取决于expr 数据类型的复杂性和simplify 中模式匹配规则的数量。数据类型中的构造函数越多，模式匹配规则越多，耗时越长。

这种行为的原因是什么？有没有办法让这样的函数更容易证明？

【问题讨论】：

标签： isabelle formal-verification

【解决方案1】：

sequential 选项使function 命令专门化重叠方程，使它们不再重叠。然而，这只是实际内部构造的预处理器，它实际上支持重叠模式（前提是可以证明右侧表示重叠实例的相同 HOL 值，即它们是一致的）。这种一致性证明表示为单个目标（如果使用sequential 选项，auto 基本上总是可以解决，因为它足以证明它们不能重叠）。然而，在消歧方程的数量上存在二次方的目标。因此，如果您添加更多构造函数，重叠的方程将被拆分为更多案例，这些案例将转化为二次目标数。

当函数不递归时有两种变通方法：

对于非递归函数，我建议使用definition 和右侧的case 表达式。然后，您可以使用HOL-Library.Simps_Case_Conv 中的simps_of_case 来获取simp 规则。但是，您并没有很好的区分大小写规则。

definition simplify :: "'a expr ⇒ 'a expr" where
  "simplify e = (case e of And a True => a | And True b => b | ... | _ => e)"

simps_of_case simplify_simps [simp]: simplify_def

如果你想有好的区分定理，你可以把函数定义拆分成几个辅助函数：

fun simplify_add :: "'a expr => 'a expr => 'a expr" where
  "simplify_add a True = a"
| "simplify_add True b = b"
| "simplify_add a b = Add a b"

fun simplify_or (* similarly *)

fun simplify :: "'a expr => 'a expr" where
  "simplify (And a b) = simplify_and a b"
| "simplify (Or a b) = simplify_or a b"
| "simplify e = e"

对于递归函数，您可以通过将一些大小写区别移到右侧来避免爆炸。例如：

fun simplify :: "'a expr ⇒ 'a expr" where
  "simplify (And a b) = (case b of True => a | _ => case a of True => b | _ => And a b)"
| ...

同样，在使它们不重叠后，这大大减少了方程的数量，但您不再获得相同的案例区分规则（和归纳规则）。

【讨论】：