If 语句不计算

Question

我知道像这样的问题似乎被人看不起，但我一直没能在网上找到答案。我有以下功能：

fun count :: "'a ⇒ 'a list ⇒ nat" where
  "count a [] = 0"
| "count a (b # xs) = (count a xs) + (if a = b then 1 else 0)"

它计算列表中与给定项目匹配的元素数。然而，当我执行以下操作时，这很简单： value "count x [x,x,y,x,y]"

我得到这个作为输出

"(if x = y then 1 else 0) + 1 + (if x = y then 1 else 0) + 1 + 1" :: "nat"

所以你可以看到输出中有挂起的“if”语句和未计算的添加。有没有可能让伊莎贝尔简化这个？

Answer 1

我不这么认为。 value 命令更像是一个纯粹的诊断工具，它主要用于评估基本项（即没有自由变量）。你得到一个结果的原因是它从它的标准方法（编译为 ML，运行 ML 代码，并将结果转换回 HOL 术语）退回到 NBE（通过评估标准化，这是慢得多，至少根据我的经验，大部分时间都没有那么有用。

我有时做的一个技巧是设置引理

lemma "count x [x, x, y, x, y] = myresult"

其中右侧的 myresult 只是一个虚拟变量。那我做

apply simp

并查看生成的证明状态（如果您没有看到任何东西：尝试在选项中打开“编辑器输出状态”）：

proof (prove)
goal (1 subgoal):
 1. (x = y ⟶ Suc (Suc (Suc (Suc (Suc 0)))) = myresult) ∧
    (x ≠ y ⟶ Suc (Suc (Suc 0)) = myresult)

有点乱，但您可以很好地读取结果：如果 x = y，则结果为 5，否则为 3。摆脱 Suc 的简单技巧在输出中是转换为 int，即 lemma "int (count x [x, x, y, x, y]) = myresult"。然后你得到：

(x = y ⟶ myresult = 5) ∧ (x ≠ y ⟶ myresult = 3)

If statement doesn't evaluate