'repeat' tactic vs 'apply' x n

Stream: new members

[cbailey]

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]

What happens if you apply nat.lt_add_left once more in the first example?

[Patrick Massot]

I think you think repeat means iterate 2

[cbailey]

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]

Lean's definition of 6 is 3 + 3

[Kevin Buzzard]

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

[Kevin Buzzard]

set_option pp.numerals false.

[cbailey]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

It's the digits [0-9]+ that get turned into binary.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

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]

5 = bit1 (bit0 1)

[Mario Carneiro]

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

[cbailey]

Oops. That's what I meant...