## Stream: new members

### Topic: Rewrite condition in ite?

#### Michael Stoll (Feb 22 2022 at 14:52):

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 (Feb 22 2022 at 14:53):

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

#### Mario Carneiro (Feb 22 2022 at 14:53):

use split_ifs and prove the cases

#### Michael Stoll (Feb 22 2022 at 14:53):

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

#### Mario Carneiro (Feb 22 2022 at 14:54):

using simp or other things to do the rewrite

#### Michael Stoll (Feb 22 2022 at 14:54):

But why does it not work?

#### Mario Carneiro (Feb 22 2022 at 14:54):

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

#### Mario Carneiro (Feb 22 2022 at 14:54):

it is hidden by default

#### Michael Stoll (Feb 22 2022 at 14:55):

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

#### Mario Carneiro (Feb 22 2022 at 14:56):

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 (Feb 22 2022 at 14:57):

OK, now I got it.

#### Mario Carneiro (Feb 22 2022 at 14:58):

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

#### Mario Carneiro (Feb 22 2022 at 14:58):

this works, but isn't usually what you want

#### Michael Stoll (Feb 22 2022 at 14:58):

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

#### Mario Carneiro (Feb 22 2022 at 14:59):

well you can work around it with convert and friends

#### Mario Carneiro (Feb 22 2022 at 14:59):

you can also use cond which is nondependent

#### Michael Stoll (Feb 22 2022 at 15:00):

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

#### Mario Carneiro (Feb 22 2022 at 15:01):

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

#### Mario Carneiro (Feb 22 2022 at 15:04):

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

#### Mario Carneiro (Feb 22 2022 at 15:04):

Option 2: simp only [nat.even_add]

#### Mario Carneiro (Feb 22 2022 at 15:06):

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] },
end


#### Michael Stoll (Feb 22 2022 at 15:38):

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

#### Kevin Buzzard (Feb 22 2022 at 15:40):

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 (Feb 22 2022 at 15:41):

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

#### Kevin Buzzard (Feb 22 2022 at 16:00):

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 (Feb 22 2022 at 16:03):

That's useful, thanks.

Last updated: Dec 20 2023 at 11:08 UTC