confused about what ih means

Stream: general

[Bernd Losert]

Consider this code:

def add (m n : ℕ) : ℕ :=
begin
  induction n,
  case zero : { exact m },
  case succ : n ih { sorry }
end

What does ih mean here? And how do I finish of the succ case?

[Yaël Dillies]

It stands for "induction hypothesis", if this is what you mean.

[Bernd Losert]

I realize that, but ih : ℕ and I'm wondering which ℕ it is.

[Kevin Buzzard]

You shouldn't really be using tactic mode to make definitions (as a rule of thumb). There is no ih in your context anyway, Lean has not picked it up.

[Bernd Losert]

I know. This is just an experiment.

[Yaël Dillies]

You're defining m + (n + 1) at that point, right? So ih is m + n.

[Kevin Buzzard]

Yael there is no ih

[Kevin Buzzard]

Berndt if you change ih to foobar then your context does not change

[Bernd Losert]

ih = m + n? Let me check.

[Yaël Dillies]

I'm answering the question Bernd meant, not the question Bernd asked.

[Kevin Buzzard]

But when we start talking about n_ih I conjecture that Yael is correct.

[Mario Carneiro]

why wouldn't there be a ih variable in that context?

[Kevin Buzzard]

Try it online? It gets named n_ih whatever you try, it's one of those random cases where you can't name variables.

[Bernd Losert]

Hmm... when I have case succ : n ih { exact ih } and I try #eval add 1 3, I get 1.

[Mario Carneiro]

def add (m n : ℕ) : ℕ :=
begin
  induction n,
  case zero : { exact m },
  case succ : n ih {
    -- case nat.succ
    -- m n ih: ℕ
    -- ⊢ ℕ
    sorry }
end

tested locally

[Kevin Buzzard]

Try exact succ ih ;-)

[Yaël Dillies]

Yes, because you just defined m + (n + 1) to be m + n.

[Kevin Buzzard]

Mario Carneiro said:

def add (m n : ℕ) : ℕ :=
begin
  induction n,
  case zero : { exact m },
  case succ : n ih {
    -- case nat.succ
    -- m n ih: ℕ
    -- ⊢ ℕ
    sorry }
end

tested locally

Oh weird, I wonder why that wasn't working for me? I had n_n and n_ih whatever I did.

[Kevin Buzzard]

Apologies all -- must have been some copy paste error at my end. Yes there is an ih, ignore most of my comments as noise.

[Bernd Losert]

Ah, the succ helped. It's really confusing though since I can't tell what ih is in terms of the other variables.

[Kevin Buzzard]

Right -- tactic mode was not designed to make definitions.

[Bernd Losert]

So ih is basically a recursive call.

[Bernd Losert]

Alright. Thanks everyone.

[Henrik Böving]

In general (including when you do proofs) the induction hypothesis can be seen as a recursive call, instead of writing induction proofs in tactic mode you can also write them using match statements and recursive "calls" to your theorems

[Kyle Miller]

Using French quotation marks, you have a lot more freedom to name hypotheses -- here's something more meaningful than ih:

def add (m n : ℕ) : ℕ :=
begin
  induction n,
  case zero : { exact m },
  case succ : n «add m n» { exact nat.succ «add m n» }
end

I don't recommend this, but I just wanted to point out that you're free to choose anything other than ih.

[Bernd Losert]

Nice.