Why isn’t Isabelle simplifying the body of my "if _ then _ else" construct?

Question

I have the following goal Isabelle:

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

None of the tactics of simp , fast , clarsimp , blast , fastforce , etc. makes no progress towards the goal, despite the fact that it is quite simple.

Why doesn't Isabelle simply simplify the body of the if construct, so that "a ≠ a" and "b ≠ b" become False and therefore solve the target?

Answer 1

if_weak_cong congruence if_weak_cong

By default, Isabelle includes a set of “congruence rules” that affect where simplification occurs. In particular, the default comparison rule is if_weak_cong , as shown below:

 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 ( b = c ), but never tries to simplify the body of the if .

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 solutions will solve the above lemma.

Why if_weak_cong is in the default set

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

One motivation is to prevent simplification from infinitely sweeping a recursive function, for example, 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 

decides the goal, and

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

sends the simplifier to the loop, since the right-hand side of the fact definition is constantly expanding.

This second script tends to occur more often than the script in the original question, which motivates if_weak_cong by default.

Answer 2

Another natural way to make progress in a proof containing if _ then _ else _ is to analyze the case, provided, for example,

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

or if foo not a free variable, but is bound by the most external universal quantifier of the meta level (as is often the case in application 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 type of quantifier, for example

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

or a meta-level universal quantifier in a nested assumption, for example

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

Neither cases nor case_tac .

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

Answer 3

Separation rules

In addition to analyzing cases and rules of congruence, there is a third way to solve this problem with the help of simplification: a splitter. The splitter allows the simplifier to independently perform a limited form of case analysis. It starts only when this term cannot be simplified in the future (splitting cases can easily lead to an explosion of the target).

The lemma split_if_asm tells the delimiter to split a if under assumptions:

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

One-step splitting can be done using 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 if split_if separation rule ( split_if ) is part of the default setting.

BTW, for each data type t in the data packet there are separation rules t.split and t.split_asm , which provide case analysis for case expressions containing type t .

Answer 4

Congruence Rules

As already noted in other answers, the if_weak_cong congruence if_weak_cong does not allow the simplifier to simplify the branches of the if statement. In this answer, I want to talk a little about using the rules of congruency with the help of a simplifier.

For more information, see also the simplifier chapter in the Isabelle / Isar reference manual (in particular, section 9.3.2).

Matching rules control how simplification descends into terms. They can be used to limit rewriting and provide additional assumptions. By default, if the simplifier encounters the st application, it will go down to both s and t to rewrite them to s' and t' before trying to rewrite the resulting member s' t' .

For each constant (or variable) c, one congruence rule can be registered. if_weak_cong rule If constant is registered by default (which lies in the syntax if ... then ... else ... ):

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

It looks like this: "If you come across the term if ?b then ?x else ?y and ?b , you can simplify it to ?c , rewrite if ?b then ?x else ?y into if ?c then ?x else ?y " . Since matching rules replace the default strategy, this prohibits any rewriting of ?x and ?y

An alternative to if_weak_cong is the strong if_cong congruence if_cong :

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

Pay attention to two assumptions (?c ⟹ ?x = ?u) and (¬ ?c ⟹ ?y = ?v) : they tell the simplicity that he can assume that the condition is satisfied (or does not matter) while simplifying the left ( or right) if branches.

As an example, consider simplification behavior on purpose

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

and suppose we don't know anything about foo . Then,

• apply simp : with the if_weak_cong rule 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 a congruency rule, this will be simplified if foo then ¬ foo else foo ⟹ False , since the condition and branches are overwritten

• apply (simp cong: if_cong del: if_cancel) : With the if_cong rule this goal will be simplified if foo then False else False ⟹ False : The condition foo ∨ False will be rewritten to foo . For the two branches, simplification is now overwritten by foo ⟹ ¬foo ∨ False and ¬foo ⟹ foo ∨ False , which are obviously rewritten to False.

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