Rewrite condition in `ite`?

Stream: new members

[Michael Stoll]

I am trying to rewrite the condition in an ite term in the following example.

import data.nat.parity

namespace experiment

def foo (n : ℕ) : ℤ := ite (even n) 1 (-1)

lemma foo_mult (m n : ℕ) : foo (m+n) = (foo m)*(foo n) :=
begin
  simp only [foo],
  rw [nat.even_add], -- rewrite `ite (even (m + n)) ...` to `ite (even m ↔ even n) ...`
  sorry
end

But I get the error message

rewrite tactic failed, motive is not type correct
  λ (_a : Prop),
    ite (even (m + n)) 1 (-1) = ite (even m) 1 (-1) * ite (even n) 1 (-1) =
      (ite _a 1 (-1) = ite (even m) 1 (-1) * ite (even n) 1 (-1))

which leaves me quite at a loss...

[Mario Carneiro]

simp might work, but you probably shouldn't do this

[Mario Carneiro]

use split_ifs and prove the cases

[Michael Stoll]

What is "this"? the rewrite or the simp?

[Mario Carneiro]

using simp or other things to do the rewrite

[Michael Stoll]

But why does it not work?

[Mario Carneiro]

because there is a dependent argument after the proposition that proves that the proposition is decidable

[Mario Carneiro]

it is hidden by default

[Michael Stoll]

But decidable nat.even ... should be available?

[Mario Carneiro]

when you rewrite even (m+n) to even m <-> even n, the argument following it, which is a proof of decidable (even (m+n)), is now no longer type correct since it isn't proving decidable (even m <-> even n)

[Michael Stoll]

OK, now I got it.

[Mario Carneiro]

simp fixes this by using the original argument to prove the new decidability

[Mario Carneiro]

this works, but isn't usually what you want

[Michael Stoll]

Is there something like a "classical" version of ite that does not require decidability?

[Mario Carneiro]

well you can work around it with convert and friends

[Mario Carneiro]

you can also use cond which is nondependent

[Michael Stoll]

Thanks; I'll check this out. [I have meeting now, so I'll leave.]

[Mario Carneiro]

the relevant lemma for rewriting if exists, but like I said this whole proof should probably be approached from a different direction

[Mario Carneiro]

Option 1: rw [if_congr (@nat.even_add m n) rfl rfl]

[Mario Carneiro]

Option 2: simp only [nat.even_add]

[Mario Carneiro]

my suggestion is to not rewrite the if at all and do something like

lemma foo_mult (m n : ℕ) : foo (m+n) = (foo m)*(foo n) :=
begin
  conv_rhs { simp only [foo] },
  split_ifs; simp [foo, nat.even_add, *],
end

[Michael Stoll]

Thanks again! There are so many tactics; it is a bit overwhelming for a beginner...

[Kevin Buzzard]

There aren't actually that many tactics -- you only need to know around 25-30 or so. It's the library that's overwhelming; once you have the tactics and the basic techniques you then want to start proving things and then you realise that you're going to have to get some feeling as to what is going on in the relevant corner of a 700K line database.

[Michael Stoll]

@Kevin Buzzard 25-30 is still a lot to learn and keep in mind.

[Kevin Buzzard]

here are the ones I taught my undergraduates; split_ifs and conv and the I tactics (letI, haveI) are the other useful ones (and there are a fair few on that list which aren't useful!)

[Michael Stoll]

That's useful, thanks.