Zulip Chat Archive

Stream: general

Topic: confused about what ih means


Bernd Losert (Jun 05 2022 at 10:26):

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 (Jun 05 2022 at 10:29):

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

Bernd Losert (Jun 05 2022 at 10:30):

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

Kevin Buzzard (Jun 05 2022 at 10:30):

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 (Jun 05 2022 at 10:31):

I know. This is just an experiment.

Yaël Dillies (Jun 05 2022 at 10:31):

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

Kevin Buzzard (Jun 05 2022 at 10:31):

Yael there is no ih

Kevin Buzzard (Jun 05 2022 at 10:31):

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

Bernd Losert (Jun 05 2022 at 10:31):

ih = m + n? Let me check.

Yaël Dillies (Jun 05 2022 at 10:31):

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

Kevin Buzzard (Jun 05 2022 at 10:32):

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

Mario Carneiro (Jun 05 2022 at 10:32):

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

Kevin Buzzard (Jun 05 2022 at 10:32):

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 (Jun 05 2022 at 10:33):

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

Mario Carneiro (Jun 05 2022 at 10:33):

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 (Jun 05 2022 at 10:33):

Try exact succ ih ;-)

Yaël Dillies (Jun 05 2022 at 10:33):

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

Kevin Buzzard (Jun 05 2022 at 10:34):

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 (Jun 05 2022 at 10:35):

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 (Jun 05 2022 at 10:35):

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 (Jun 05 2022 at 10:35):

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

Bernd Losert (Jun 05 2022 at 10:35):

So ih is basically a recursive call.

Bernd Losert (Jun 05 2022 at 10:36):

Alright. Thanks everyone.

Henrik Böving (Jun 05 2022 at 10:38):

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 (Jun 05 2022 at 14:44):

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 (Jun 05 2022 at 16:11):

Nice.


Last updated: Dec 20 2023 at 11:08 UTC