## 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},
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},
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