## 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.

example : ∀ a b c : ℕ, ite (a ≤ b) c (c + 1) ≤ (c + 2) :=
begin
intros a b c,
by_cases (a ≤ b),

-- 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 ites 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