Why won't Isabelle simplify the body of my "if _ then _ else" construct?
isabelle
Solution
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.
Problem
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?