Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip Sebastien Gouezel (Mar 13 2019 at 21:44):

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

view this post on Zulip Patrick Massot (Mar 13 2019 at 21:47):

I think you think repeat means iterate 2

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:48):

Lean's definition of 6 is 3 + 3

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:48):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:50):

set_option pp.numerals false.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:51):

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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:51):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 13 2019 at 21:55):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)) ?

view this post on Zulip Mario Carneiro (Mar 13 2019 at 22:17):

5 = bit1 (bit0 1)

view this post on Zulip Mario Carneiro (Mar 13 2019 at 22:17):

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

view this post on Zulip cbailey (Mar 13 2019 at 22:30):

Oops. That's what I meant...


Last updated: May 13 2021 at 18:26 UTC