数据类型转换函数需要很长时间才能证明

Question

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 中模式匹配规则的数量。数据类型中的构造函数越多，模式匹配规则越多，耗时越长

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

Answer 1

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

当函数不是递归时，有两种解决方法：

对于non-recursive函数，我建议使用definition，右边有一个case表达式。然后，您可以使用 HOL-Library.Simps_Case_Conv 中的 simps_of_case 来获取简单规则。但是，您没有很好的区分大小写规则。

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"

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

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

同样，这大大减少了生成方程式后的数量 non-overlapping，但您不再获得相同的区分大小写规则（和归纳规则）。

数据类型转换函数需要很长时间才能证明

Datatype transformation function takes very long to proof

formal-verification

isabelle