Why won't Isabelle simplify the body of my “if

问题:

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?

回答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.

回答2:

Split rules

Besides case analysis and congruence rules, there is a third way to solve this goal with the simplifier: The splitter. The splitter allows the simplifier to perform a limited form of case analysis on its own. It is only run when the term cannot be simplified any further on its own (splitting cases can easily lead to an explosion of the goal).

The lemma split_if_asm instructs the splitter to split an if in the assumptions:

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

A single-step split can be performed with the split method:

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

Note that the rule to split an if in the conclusion (split_if) is part of the default setup.

BTW, for each datatype t, the datatype package provides the split rules t.split and t.split_asm which provide case analysis for case expressions involving the type t.

回答3:

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)

回答4:

Another natural way of making progress in a proof containing if _ then _ else _ is case analysis on the condition, e.g.,

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

or if foo is not a free variable, but bound by an outermost meta-level universal quantifier (as is often the case in apply-scripts):

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

Unfortunately, if foo is bound by another kind of quantifier, e.g.

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

or by a meta-level universal quantifier in a nested assumption, e.g.

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

neither cases nor case_tac are applicable.

Note: See also here for the (slight) difference between cases and case_tac.