伊莎贝尔为什么不简化我的"if _ then _ else"结构的主体？

Question

我有以下Isabelle目标:

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语句(the b = c)的条件,但从不试图简化if语句的主体.

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

apply (simp cong del: if_weak_cong)

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

apply (simp cong: if_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其成为默认情况.

Answer 2

除了案例分析和同余规则之外,还有第三种方法可以通过简化器来解决这个目标:分离器.分离器允许简化器自己执行有限形式的案例分析.只有当术语不能单独进行简化时才会运行(分裂案例很容易导致目标爆炸).

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

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在summary(split_if)中拆分a的规则是默认设置的一部分.

BTW,对于每种数据类型t,数据类型包提供拆分规则t.split,t.split_asm并为case涉及该类型的表达式提供案例分析t.