Zulip Chat Archive

Stream: new members

Topic: Dealing with ite

view this post on Zulip 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) :=
   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

view this post on Zulip Mario Carneiro (Oct 09 2019 at 03:15):

use the split_ifs tactic after the intros

view this post on Zulip Mario Carneiro (Oct 09 2019 at 03:16):

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

view this post on Zulip 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 :=
    rw f,
    by_cases (a = b),
        {simp [a = b],},
        {simp [a  b],},

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.

   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?

view this post on Zulip 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 :=
    simp [a = b],
#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 :=
    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],},

if_simp_congr is a version of if_congr with less decidability assumptions than if_congr.

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Reuben Rowe (Nov 21 2019 at 10:55):

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

view this post on Zulip 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