What does rintros and hk mean?

Stream: new members

[Pascal Schoppenhauer]

I have this code example from the "Mathematics in Lean" Tutorial:
But I do not understand what rintros does. And how does hk know it is n=2*k?

import data.nat.parity tactic
open nat

example : ∀ m n : nat, even n → even (m * n) :=
begin
  -- say m and n are natural numbers, and assume n=2*k
  rintros m n ⟨k, hk⟩,
  -- We need to prove m*n is twice a natural. Let's show it's twice m*k.
  use m * k,
  -- substitute in for n
  rw hk,
  -- and now it's obvious
  ring,
end

[Eric Wieser]

rintros m n ⟨k, hk⟩ is the same as intros m n hk', cases hk' with k hk,, if that helps

[Floris van Doorn]

as a second piece to the puzzle: docs#even is defined to be ∃ k, a = 2 * k

[Ruben Van de Velde]

It might help a bit to start with

example : ∀ m n : nat, even n → even (m * n) :=
begin
  dsimp only [even],

[Yaël Dillies]

And rintro is exactly the same as rintros.

[Pascal Schoppenhauer]

@Heather Macbeth Hey I'm sorry to bother you, but I'm still very new to Lean and I would like to understand what the "rintros" command does. I have seen it in many simple examples but I can't find a good explanation of what its purpose is.

[Eric Wieser]

tactic#rintro might be helpful (rintros is the same as rintro)

[Pascal Schoppenhauer]

Ok, thanks for the answer. Why does

rintros ⟨k, hk⟩,

all of the sudden create a k and

hk: n = 2 * k

Where does the 2 * k come from?

[Kevin Buzzard]

If you replaced rintros \<k, hk\> with intro x, what would the type of x be? And how do you make a term of that type?

[Pascal Schoppenhauer]

nat ?
I dont know... :sad:

[Pascal Schoppenhauer]

What type is hk?

[Notification Bot]

This topic was moved here from #Is there code for X? > Addition of interiors by Eric Wieser

[Eric Wieser]

@Pascal Schoppenhauer, you made a thread about this almost a month ago (which I've now combined your latest post with), but never responded - did you not see the replies?

[Pascal Schoppenhauer]

:laughing: yeah I saw the responses, but I didn't get any smarter from them... Does hk stand for anything, or is it just the name for the term?

[Pascal Schoppenhauer]

Or rather: I don't understand where the 2 comes from. I now understand what rintros does, but thats up with the \<k, hk\>

[Huỳnh Trần Khanh]

hk is just a name. it means a hypothesis about k

[Pascal Schoppenhauer]

Ahh ok, thanks. :thank_you: That makes sense. Now what is this ⟨k, hk⟩ Syntax?

[Huỳnh Trần Khanh]

do you know "destructuring"/"unpacking"/"structured bindings" in programming languages?

[Huỳnh Trần Khanh]

the even n hypothesis is a structure with 2 fields: a natural number and a hypothesis about that number

[Huỳnh Trần Khanh]

you use that syntax to "destructure"/"unpack" the two fields

[Kevin Buzzard]

To give a term of type even n is to give a pair of terms -- first a natural k and second a proof that n = 2 * k. So the rintro takes the term apart into its two pieces.

[Stuart Presnell]

To see what's happening with the rintros command, let's play it back in slow motion:

  -- We start with `∀ m n : nat, even n → even (m * n)`
  intros m n H, -- This introduces `m` and `n` of type `ℕ`, and the hypothesis `H : even n`
  unfold even at H,  -- What does `even n` mean?  It means there's a `k : ℕ` such that `n = 2 * k`
  cases H with k hk, -- This decomposes that `∃` statement, introducing `k : ℕ` and `hk : n = 2 * k`

So hk is just the name that's been chosen for the proposition n = 2 * k — we could have called it something else. And that proposition is part of the premise that n is even.

rintros m n ⟨k, hk⟩ is just a super-slick way of combining all these steps into one.

[Pascal Schoppenhauer]

Ok that sounds smart. :thumbs_up: Thanks! So even n is kind of like an array and i could unpack that array with something like that (pseudocode): h, hk = even n. I found that I can write it like this:

...
example : ∀ m n : nat, even n → even (m * n) :=
begin
  -- say m and n are natural numbers, and assume n=2*k
  intro m,
  intro n,
  /-
  m n : ℕ
  ⊢ even n → even (m * n)
  -/
  rintros ⟨k, hk⟩,
...

I think I understand it but let me try to clarify it for myself: The intro just takes the first element of the list of expressions befor the → sign. The rintro does that recursively.

[Pascal Schoppenhauer]

Ok now this is cool. Love it thanks a lot! :big_smile: One more questin why do I have to use ⟨ ⟩ why not ( ) or [ ]? How do I know when to use these?

[Kevin Buzzard]

You just have to learn the syntax for terms and tactics. rintro uses pointies.

[Pascal Schoppenhauer]

Ok thanks a lot :heart: