Dealing with ite

Stream: new members

[Chu-Wee Lim]

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]

use the split_ifs tactic after the intros

[Mario Carneiro]

the 1 <= 2 can be solved by norm_num or exact dec_trivial

[Reuben Rowe]

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]

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]

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]

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]

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

[Reuben Rowe]

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.