# Zulip Chat Archive

## Stream: new members

### Topic: 'repeat' tactic vs 'apply' x n

#### cbailey (Mar 13 2019 at 21:41):

Why do these two examples exhibit different behavior (iterative application of a tactic vs repeat)? The definitions of repeat and repeat_aux don't seem to suggest they would do anything different.

example : 5 < (1 + (1 + 6)) := begin apply nat.lt_add_left, -- 5 < 1 + 6 apply nat.lt_add_left, -- 5 < 6 apply nat.lt.base end example : 5 < (1 + (1 + 6)) := begin repeat {apply nat.lt_add_left}, -- 5 < 1 end

#### Sebastien Gouezel (Mar 13 2019 at 21:44):

What happens if you `apply nat.lt_add_left`

once more in the first example?

#### Patrick Massot (Mar 13 2019 at 21:47):

I think you think `repeat`

means `iterate 2`

#### cbailey (Mar 13 2019 at 21:47):

Well that explains that.

example : 5 < (1 + (1 + 6)) := begin apply nat.lt_add_left, -- 5 < 1 + 6 apply nat.lt_add_left, -- 5 < 6 apply nat.lt_add_left, -- 5 < 3 apply nat.lt_add_left, -- 5 < 1 end

#### Kevin Buzzard (Mar 13 2019 at 21:48):

Lean's definition of 6 is 3 + 3

#### Kevin Buzzard (Mar 13 2019 at 21:48):

numerals are defined by binary: 7 := 3 + 3 + 1 and 8 := 4 + 4 etc etc

#### Kevin Buzzard (Mar 13 2019 at 21:50):

`set_option pp.numerals false`

.

#### cbailey (Mar 13 2019 at 21:50):

Ah okay. I didn't know it used a binary representation internally but that makes sense. Thank you.

#### Kevin Buzzard (Mar 13 2019 at 21:50):

def bit0 {α : Type u} [s : has_add α] (a : α) : α := a + a def bit1 {α : Type u} [s₁ : has_one α] [s₂ : has_add α] (a : α) : α := (bit0 a) + 1

This is what Lean uses when it sees numeric characters.

#### Kevin Buzzard (Mar 13 2019 at 21:51):

Obviously nat is represented as succ (succ (succ ...))) -- that's the definition.

#### Kevin Buzzard (Mar 13 2019 at 21:51):

It's the digits `[0-9]+`

that get turned into binary.

#### Kevin Buzzard (Mar 13 2019 at 21:54):

example : (5 : ℕ) < ((1 : ℕ) + ((1 : ℕ) + (6 : ℕ))) := begin repeat {unfold bit1 <|> unfold bit0}, repeat {rw add_assoc}, apply nat.lt_add_left, -- 5 < 7 apply nat.lt_add_left, -- 5 < 6 apply nat.lt_add_left, -- 5 < 5 apply nat.lt_add_left, -- 5 < 4 apply nat.lt_add_left, -- 5 < 3 apply nat.lt_add_left, -- 5 < 2 apply nat.lt_add_left, -- 5 < 1 sorry end

#### Kevin Buzzard (Mar 13 2019 at 21:55):

or more precisely, `⊢ 1 + (1 + (1 + (1 + 1))) < 1 + (1 + (1 + (1 + (1 + (1 + 1)))))`

etc

#### Kevin Buzzard (Mar 13 2019 at 21:56):

example : (5 : ℕ) < ((1 : ℕ) + ((1 : ℕ) + (6 : ℕ))) := begin repeat {unfold bit1 <|> unfold bit0}, repeat {rw ←add_assoc}, apply nat.lt_add_left, -- 1 + 1 + 1 + 1 + 1 < 1 sorry end

#### Kevin Buzzard (Mar 13 2019 at 21:57):

The actual behaviour of the code depends exactly on how the numerals are being stored. I am messing around with them with the unfolding code and can get repeat {apply nat.lt_add_left} to display different behaviour.

#### cbailey (Mar 13 2019 at 22:09):

Sorry, furiously tabbing back and forth between these definitions. So when you have

example : (5 : ℕ) < ((1 : ℕ) + ((1 : ℕ) + (6 : ℕ))) :=

The 5 is always just an element of nat, but it's constructed as ` bit1 S (S (0)) S (S (0)) `

?

#### Mario Carneiro (Mar 13 2019 at 22:17):

`5 = bit1 (bit0 1)`

#### Mario Carneiro (Mar 13 2019 at 22:17):

`= (1 + 1) + (1 + 1) + 1`

#### cbailey (Mar 13 2019 at 22:30):

Oops. That's what I meant...

Last updated: May 13 2021 at 18:26 UTC