Why won't Isabelle simplify the body of my "if _ then _ else" construct?

Question

I have the following Isabelle goal:

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

None of the tactics simp, fast, clarsimp, blast, fastforce, etc. make any progress on the goal, despite it being quite simple.

Why doesn't Isabelle just simplify the body of the if construct so that both "a ≠ a" and "b ≠ b" become False, and hence solve the goal?

Answer 1

The if_weak_cong congruence rule

By default, Isabelle includes a set of "congruence rules" that affect where simplification takes place. In particular, a default congruence rule is if_weak_cong, as follows:

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

This congruence rule tells the simplifier to simplify the condition of the if statement (the b = c) but never attempt to simplify the body of the if statement.

You can either disable the congruence rule using:

apply (simp cong del: if_weak_cong)

or override it with an alternative (more powerful) congruence rule:

apply (simp cong: if_cong)

Both of these will solve the above lemma.

Why if_weak_cong is in the default cong set

Another reasonable question might be: "Why would if_weak_cong be in the default congruence set if it causes problems like the above?"

One motivation is to prevent the simplifier from unfolding a recursive function infinitely, such as in the following case:

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

in this case,

lemma "fact 3 = 6"
  by simp

solves the goal, while

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

sends the simplifier into a loop, because the right-hand-side of the fact definition continually unfolds.

This second scenario tends to occur more frequently than the scenario in the original question, which motivates if_weak_cong being the default.

Answer 2

Congruence rules

As already noted in the other answers, the if_weak_cong congruence rule prevents the simplifier from simplifying the branches of the if statement. In this answer, I want to elaborate a bit on the use of congruence rules by the simplifier.

For further information, see also the chapter about the Simplifier in the Isabelle/Isar Reference Manual (in particular section 9.3.2).

Congruence rules control how the simplifier descends into terms. They can be used to limit rewriting and to provide additional assumptions. By default, if the simplifier encounters a function application s t it will descend both into s and t to rewrite them to s' and t', before trying to rewrite the resulting term s' t'.

For each constant (or variable) c one can register a single congruence rule. The rule if_weak_cong is registered by default the constant If (which is underlying the if ... then ... else ... syntax):

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

This reads as: "If you encounter a term if ?b then ?x else ?y and ?b can be simplified to ?c, then rewrite if ?b then ?x else ?y to if ?c then ?x else ?y". As congruence rules replace the default strategy, this forbids any rewriting of ?x and ?y.

An alternative to if_weak_cong is the strong congruence rule if_cong:

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

Note the two assumptions (?c ⟹ ?x = ?u) and (¬ ?c ⟹ ?y = ?v): They tell the simplifier that it may assume that the condition holds (or holds not) when simplifying the left (or right) branch of the if.

As an example, consider the behaviour of the simplifier on the goal

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

and assume that we know nothing about foo. Then,

• apply simp: with the rule if_weak_cong, this will be simplified to if foo then ¬ foo ∨ False else foo ⟹ False, only the condition is rewritten
• apply (simp cong del: if_weak_cong): Without any congruence rule, this will be simplified to if foo then ¬ foo else foo ⟹ False, as the condition and the branches are rewritten

• apply (simp cong: if_cong del: if_cancel): With the rule if_cong, this goal will simplified to if foo then False else False ⟹ False: The condition foo ∨ False will be rewritten to foo. For the two branches, the simplifier now rewrites foo ⟹ ¬foo ∨ False and ¬foo ⟹ foo ∨ False, both of which obviously rewrite to False.

  (I removed if_cancel, which would usually solve the remaining goal completely)