Zulip Chat Archive

Stream: new members

Topic: What does rintros and hk mean?


Pascal Schoppenhauer (Nov 11 2021 at 11:36):

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 (Nov 11 2021 at 11:37):

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

Floris van Doorn (Nov 11 2021 at 12:09):

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

Ruben Van de Velde (Nov 11 2021 at 12:12):

It might help a bit to start with

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

Yaël Dillies (Nov 11 2021 at 12:33):

And rintro is exactly the same as rintros.

Pascal Schoppenhauer (Dec 05 2021 at 12:45):

@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 (Dec 05 2021 at 12:47):

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

Pascal Schoppenhauer (Dec 05 2021 at 13:37):

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 (Dec 05 2021 at 13:40):

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 (Dec 05 2021 at 13:43):

nat ?
I dont know... :sad:

Pascal Schoppenhauer (Dec 05 2021 at 13:48):

What type is hk?

Notification Bot (Dec 05 2021 at 14:00):

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

Eric Wieser (Dec 05 2021 at 14:01):

@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 (Dec 05 2021 at 14:55):

: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 (Dec 05 2021 at 15:02):

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 (Dec 05 2021 at 15:09):

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

Pascal Schoppenhauer (Dec 05 2021 at 15:12):

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

Huỳnh Trần Khanh (Dec 05 2021 at 15:14):

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

Huỳnh Trần Khanh (Dec 05 2021 at 15:15):

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

Huỳnh Trần Khanh (Dec 05 2021 at 15:15):

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

Kevin Buzzard (Dec 05 2021 at 15:17):

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 (Dec 05 2021 at 15:31):

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 (Dec 05 2021 at 15:32):

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 (Dec 05 2021 at 15:35):

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 (Dec 05 2021 at 15:36):

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

Pascal Schoppenhauer (Dec 05 2021 at 15:36):

Ok thanks a lot :heart:


Last updated: Dec 20 2023 at 11:08 UTC