isabelle - 为什么 Isabelle 不简化我的“if _ then _ else”构造的主体？

Question

我有以下伊莎贝尔目标：

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"

战术simp, fast, clarsimp, blast,fastforce等都没有在目标上取得任何进展，尽管它非常简单。

为什么 Isabelle 不只是简化if构造体，使 "a ≠ a" 和 "b ≠ b" 都变为False，从而解决目标？

Answer 1

一致性if_weak_cong规则

默认情况下，Isabelle 包含一组“一致性规则”，这些规则会影响简化发生的位置。特别是，默认的同余规则是if_weak_cong，如下所示：

b = c ⟹ (if b then x else y) = (if c then x else y)

这个全等规则告诉简化器简化if语句的条件（the b = c），但从不尝试简化if语句的主体。

您可以使用以下方法禁用一致性规则：

apply (simp cong del: if_weak_cong)

或者用一个替代的（更强大的）同余规则覆盖它：

apply (simp cong: if_cong)

这两个都将解决上述引理。

为什么if_weak_cong在默认的conset中

另一个合理的问题可能是：“如果它导致上述问题，为什么会if_weak_cong在默认同余集中？”

一个动机是防止简化器无限展开递归函数，例如在以下情况下：

fun fact where
    "fact (n :: nat) = (if n = 0 then 1 else (n * fact (n - 1)))"

在这种情况下，

lemma "fact 3 = 6"
  by simp

解决了目标，而

lemma "fact 3 = 6"
  by (simp cong del: if_weak_cong)

将简化器发送到循环中，因为定义的右侧fact不断展开。

第二种情况往往比原始问题中的情况更频繁地发生，这促使if_weak_cong成为默认情况。

Answer 2

拆分规则

除了案例分析和同余规则，还有第三种方法可以用简化器解决这个目标：拆分器。拆分器允许简化器自行执行有限形式的案例分析。它仅在术语本身无法进一步简化时运行（拆分案例很容易导致目标爆炸）。

引理split_if_asm指示拆分器if在假设中拆分 an：

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"
  by (simp split: split_if_asm)

可以使用以下split方法执行单步拆分：

lemma "⟦ if foo then a ≠ a else b ≠ b ⟧ ⟹ False"
  apply (split split_if_asm)
  apply simp_all
  done

请注意，if在结论 ( split_if) 中拆分 an 的规则是默认设置的一部分。

顺便说一句，对于每个 datatype t， datatype 包都提供了拆分规则t.split，并为涉及 type 的表达式t.split_asm提供了案例分析。caset

Answer 3

一致性规则

正如其他答案中已经指出的那样，if_weak_cong全等规则阻止简化器简化 if 语句的分支。在这个答案中，我想详细说明简化器对同余规则的使用。

有关详细信息，另请参阅Isabelle/Isar 参考手册中有关简化器的章节（特别是第 9.3.2 节）。

同余规则控制简化器如何降级为项。它们可用于限制重写并提供额外的假设。默认情况下，如果简化器遇到一个函数应用程序，它会在尝试重写生成的 term 之前s t同时下降到sandt将它们重写为s'and 。t's' t'

对于每个常量（或变量）c，可以注册一个同余规则。该规则if_weak_cong默认注册为常量If（这是if ... then ... else ...语法的基础）：

?b = ?c ⟹ (if ?b then ?x else ?y) = (if ?c then ?x else ?y)

其内容为：“如果遇到一个术语if ?b then ?x else ?y并且?b可以简化为?c，则重写if ?b then ?x else ?y为if ?c then ?x else ?y”。由于全等规则取代了默认策略，因此禁止对?x和进行任何重写?y。

一种替代方法if_weak_cong是强同余规则if_cong：

⟦ ?b = ?c; (?c ⟹ ?x = ?u); (¬ ?c ⟹ ?y = ?v) ⟧
    ⟹ (if ?b then ?x else ?y) = (if ?c then ?u else ?v)

注意两个假设(?c ⟹ ?x = ?u)和(¬ ?c ⟹ ?y = ?v)：它们告诉简化器，在简化 if 的左（或右）分支时，它可能假设条件成立（或不成立）。

例如，考虑简化器在目标上的行为

if foo ∨ False then ¬foo ∨ False else foo ⟹ False

并假设我们对foo. 然后，

• apply simp：有了规则if_weak_cong，这将被简化为 if foo then ¬ foo ∨ False else foo ⟹ False，只有条件被重写
• apply (simp cong del: if_weak_cong)：没有任何同余规则，这将被简化为 if foo then ¬ foo else foo ⟹ False，因为条件和分支被重写

• apply (simp cong: if_cong del: if_cancel)：有了规则if_cong，这个目标将简化为 if foo then False else False ⟹ False：条件foo ∨ False将被改写为foo。对于这两个分支，简化器现在重写 foo ⟹ ¬foo ∨ False和¬foo ⟹ foo ∨ False，这两个显然都重写为 False。

  （我删除了if_cancel，这通常会完全解决剩下的目标）

Answer 4

在证明包含中取得进展的另一种自然方式if _ then _ else _是对条件进行案例分析，例如，

lemma "(if foo then a ~= a else b ~= b) ==> False"
  by (cases foo) simp_all

或者 iffoo不是一个自由变量，而是由一个最外层的元级通用量词绑定（在应用脚本中经常出现这种情况）：

lemma "!!foo. (if foo then a ~= a else b ~= b) ==> False"
  apply (case_tac foo)
  apply simp_all
done

不幸的是，iffoo受另一种量词的约束，例如

lemma "ALL foo. (if foo then a ~= a else b ~= b) ==> False"

或通过嵌套假设中的元级通用量词，例如

lemma "True ==> (!!foo. (if foo then a ~= a else b ~= b)) ==> False"

既不cases也不case_tac适用。

注意：另请参阅此处cases了解和之间的（轻微）差异case_tac。