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

Question

我有以下伊莎贝尔目标:

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

无计谋simp , fast , clarsimp , blast , fastforce等在目标上取得任何进展，尽管它很简单。

为什么伊莎贝尔不只是简化 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 的条件语句( b = c )但从不尝试简化 if 的主体陈述。

您可以使用以下方法禁用同余规则:

apply (simp cong del: if_weak_cong)

或使用替代(更强大)的同余规则覆盖它:

apply (simp cong: if_cong)

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

为什么if_weak_cong在默认的配置集中

另一个合理的问题可能是:“如果 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是默认的。