# Zulip Chat Archive

## Stream: new members

### Topic: Dealing with ite

#### Chu-Wee Lim (Oct 09 2019 at 03:03):

Are there any good tips for dealing with ite cases? The following seems unnecessarily verbose.

I'd greatly appreciate any advice. Thanks in advance for any suggestions.

example : ∀ a b c : ℕ, ite (a ≤ b) c (c + 1) ≤ (c + 2) := begin intros a b c, by_cases (a ≤ b), simp [h], apply nat.le_add_right, simp [h], apply nat.add_le_add_left, -- Is there an easier way to show 1 ≤ 2? apply nat.succ_le_succ, exact zero_le_one end

#### Mario Carneiro (Oct 09 2019 at 03:15):

use the `split_ifs`

tactic after the `intros`

#### Mario Carneiro (Oct 09 2019 at 03:16):

the `1 <= 2`

can be solved by `norm_num`

or `exact dec_trivial`

#### Reuben Rowe (Nov 21 2019 at 00:08):

This is very useful - `split_ifs`

seems to make handling the cases of if-then-else very convenient. However I'd still like to understand a bit more about how `simp`

deals with if-then-else.

Like Chu-Wee, I had hit upon the strategy of using `by_cases`

on the branching condition, and then using `simp`

. The following (a slight variation of Chu-Wee's code) is a MWE demonstrating the situation I was playing around with.

def f {α : Sort*} [decidable_eq α] (a b : α) : ℕ := if a = b then 0 else 0 example {α : Sort*} [decidable_eq α] : ∀ (a b : α), (f a b) = 0 := begin intros, rw f, by_cases (a = b), {simp [‹a = b›],}, {simp [‹a ≠ b›],}, end

But then I read in the documentation for `simp`

that it is bad practice to use it in the middle of a proof (OK, here it is at the end of each case's proof, but this is just a MWE, and in general I might need to do further proving). So I used the `set_option trace.simplify.rewrite true`

option to display the lemmas that `simp`

found and used, with the aim of replacing the use of `simp`

with `rewrite`

using these lemmas. Taking the first case (`a = b`

), I got the following output.

0. [simplify.rewrite] [h]: a ==> b 0. [simplify.rewrite] [eq_self_iff_true]: b = b ==> true 0. [simplify.rewrite] [if_true]: ite true 0 0 ==> 0 0. [simplify.rewrite] [eq_self_iff_true]: 0 = 0 ==> true

Things seem to start off well, but I quickly hit a snag:

... by_cases (a = b), { -- Current goal is ite (a = b) 0 0 = 0 rw ‹a = b›, -- Current goal is ite (b = b) 0 0 = 0 rw eq_self_iff_true, -- rewrite tactic failed, motive is not type correct

Using the `set_option trace.check true`

, I got the following information about the failure.

[check] application type mismatch at ite _a argument type decidable (b = b) expected type decidable _a

The goal that I would expect to see after this last rewrite is `ite (true) 0 0 = 0`

. So I understand that what is going wrong here is that `ite`

is taking an implicitly inserted argument, which is a proof that the branching condition is decidable. For the goal `ite (b = b) 0 0 = 0`

I'm guessing the proof that is implicitly synthesised is probably `decidable.is_true rfl : decidable (b = b)`

. Now, after the rewrite `a = b ==> true`

, I imagine that the branching condition `(b = b)`

in `ite (b = b) 0 0 = 0`

is being transformed, but not the decidability proof, and the source of the above error is that this is a witness for `decidable (b = b)`

but not for `decidable (true)`

.

So, I don't understand how `simp`

is using the `eq_self_iff_true`

lemma in a rewrite.

I also noticed that it then uses the lemma `if_true`

, and after digging around in the library I found that `if_true`

actually uses the lemma:

`if_pos {c : Prop} [h : decidable c] (hc : c) {α : Sort u} {t e : α} : (ite c t e) = t`

I was able to use this directly in the following calculational proof of the case.

calc f a b = (if (a = b) then 0 else 0) : by refl ... = 0 : by rw if_pos ‹a = b›,

So, my question here is: what proof is `simp`

finding in this situation?

#### Alex J. Best (Nov 21 2019 at 00:30):

You can always use `#print`

to see the proof term like

lemma aa {α : Sort*} [decidable_eq α] (a b : α) (h : a = b) : ite (a = b) 0 0 = 0 := begin simp [‹a = b›], end #print aa

this is a bit ugly but we can see the names of some key lemmas like `if_simp_congr`

which says two `ite`

s are equal if their arguments are all equal and the props are equivalent. You can use this via

example {α : Sort*} [decidable_eq α] : ∀ (a b : α), (f a b) = 0 := begin intros, rw f, by_cases (a = b), {rw ‹a = b›, rw if_simp_congr (eq_self_iff_true b) (rfl) (rfl), rw if_true, }, {simp [‹a ≠ b›],}, end

`if_simp_congr`

is a version of `if_congr`

with less decidability assumptions than `if_congr`

.

#### Kevin Buzzard (Nov 21 2019 at 08:02):

The `simp`

rule is that you should only use it to close a goal, so both applications in @Reuben Rowe 's example above are fine (by the way if you write ` ```lean `

at the top instead of just ` ``` `

when quoting code then you get syntax highlighting i.e. colours)

#### Kevin Buzzard (Nov 21 2019 at 08:08):

As for the motive not being type correct, `simp`

is more powerful than `rw`

here. You can use `simp only [eq_self_iff_true]`

to get from `ite (b = b) 0 0 = 0`

to `ite true 0 0 = 0`

and `simp only`

is Ok in the middle of a proof.

#### Reuben Rowe (Nov 21 2019 at 10:55):

Thanks @Alex J. Best and @Kevin Buzzard , this is really helpful.

#### Reuben Rowe (Nov 21 2019 at 10:56):

I see what is going on: `set_option trace.simplify.rewrite true`

is only showing the lemmas with the `[simp]`

attribute, even though the `simp`

tactic uses other things, like `[congr]`

lemmas.

Last updated: May 08 2021 at 10:12 UTC