orange bar hell!

Stream: general

[Huỳnh Trần Khanh]

why on earth does this take an eternity to typecheck :cry:

import tactic

inductive word_size_t
| char
| i32
| i64

def get_left_bound : word_size_t → ℤ
| word_size_t.char := -128
| word_size_t.i32 := -2147483648
| word_size_t.i64 := -9223372036854775808

def get_right_bound : word_size_t → ℤ
| word_size_t.char := 128
| word_size_t.i32 := 2147483648
| word_size_t.i64 := 9223372036854775808

@[derive decidable_pred] def within_bounds (word_size : word_size_t) (x : ℤ) : Prop := get_left_bound word_size ≤ x ∧ x < get_right_bound word_size

lemma x_le_sum (l : list ℤ) (lb : ℤ) (h' : ∀ x, x ∈ l → lb ≤ x) : (↑l.length : ℤ) * lb ≤ l.sum := begin
  induction l,
  norm_num,
  norm_num,
  rw add_mul,
  norm_num,
  have := l_ih begin
    intros x y,
    have := h' x,
    have := this (list.mem_cons_of_mem l_hd y),
    assumption,
  end,
  have := int.add_le_add this (h' l_hd (list.mem_cons_self l_hd l_tl)),
  clear_except this,
  conv begin
    to_rhs,
    rw add_comm,
  end,
  assumption,
end

lemma sum_le_x (l : list ℤ) (ub : ℤ) (h' : ∀ x, x ∈ l → x ≤ ub) : l.sum ≤ (↑l.length : ℤ) * ub := begin
  induction l,
  norm_num,
  norm_num,
  rw add_mul,
  norm_num,
  have := l_ih begin
    intros x y,
    have := h' x,
    have := this (list.mem_cons_of_mem l_hd y),
    assumption,
  end,
  have := int.add_le_add this (h' l_hd (list.mem_cons_self l_hd l_tl)),
  clear_except this,
  conv begin
    to_lhs,
    rw add_comm,
  end,
  assumption,
end

lemma split2 (input : list ℤ) (output : ℤ)
  (h : ∀ (x : ℤ), x ∈ input → -20 ≤ x ∧ x ≤ 20)
  (h' : input.length ≤ 30) :
  ∀ (x : ℤ),
    x ∈ [↑(input.length), ↑(input.length), input.sum] ++ input →
    within_bounds word_size_t.i32 x :=
begin
  intros x y,
  have := list.mem_append.mp y,
  cases this,
  clear_except this h h',
  cases this,
  rw this,
  clear_except h',
  simp only [get_right_bound, get_left_bound, within_bounds],
  split,
  {
    clear_except,
    have := int.coe_zero_le input.length,
    have a' : (-2147483648 : ℤ) ≤ 0 := by norm_num,
    exact le_trans a' this,
  },
  {
    have := int.coe_nat_le.mpr h',
    clear_except this,
    norm_num at this,
    have a' : (30 : ℤ) < 2147483648 := by norm_num,
    exact gt_of_gt_of_ge a' this,
  },
  cases this,
  rw this,
  clear_except h',
  simp only [get_right_bound, get_left_bound, within_bounds],
  split,
  {
    clear_except,
    have := int.coe_zero_le input.length,
    have a' : (-2147483648 : ℤ) ≤ 0 := by norm_num,
    exact le_trans a' this,
  },
  {
    have := int.coe_nat_le.mpr h',
    clear_except this,
    norm_num at this,
    have a' : (30 : ℤ) < 2147483648 := by norm_num,
    exact gt_of_gt_of_ge a' this,
  },
  cases this,
  rw this,
  clear_except h h',
  simp only [get_right_bound, get_left_bound, within_bounds],
  split,
  have a1 := x_le_sum input (-20 : ℤ) begin
    intros x y,
    exact (h x y).left,
  end,
  have a2 : -600 ≤ (↑input.length) * (-20 : ℤ) := begin
    clear_except h',
    have := (mul_le_mul_left_of_neg (show (-20 : ℤ) < (0 : ℤ), by { clear_except, norm_num, })).mpr (int.coe_nat_le.mpr h'),
    rw (show (-20 : ℤ) * (↑30 : ℤ) = -600, by norm_num) at this,
    rw mul_comm at this,
    exact this,
  end,
  have a3 : -600 ≤ input.sum := begin
    clear_except a1 a2,
    exact le_trans a2 a1,
  end,
  clear_except a3,
  {
    have a' : (-2147483648 : ℤ) ≤ -600 := by norm_num,
    exact le_trans a' a3,
  },
  have a1 := sum_le_x input 20 begin
    intros x y,
    exact (h x y).right,
  end,
  have a2 : (↑input.length) * (20 : ℤ) ≤ 600 := begin
    clear_except h',
    have := @mul_le_mul ℤ _ (↑input.length : ℤ) (20 : ℤ) (30 : ℤ) (20 : ℤ) begin
      have := int.coe_nat_le.mpr h',
      assumption,
    end (by norm_num) (by norm_num) (by norm_num),
    norm_num at this,
    assumption,
  end,
  have : input.sum ≤ 600 := begin
    clear_except a1 a2,
    exact le_trans a1 a2,
  end,
  clear_except this,
  {
    have a' : (600 : ℤ) < 2147483648 := by { clear_except, norm_num, },
    exact gt_of_gt_of_ge a' this,
  },
  clear_except this,
  exfalso,
  have := list.not_mem_nil x this,
  assumption,
  clear_except h this,
  have := h x this,
  clear_except this,
  simp only [get_right_bound, get_left_bound, within_bounds],
  split,
  have := this.left,
  clear_except this,
  {
    have a' : (-2147483648 : ℤ) ≤ -20 := by { clear_except, norm_num, },
    exact le_trans a' this,
  },
  have := this.right,
  clear_except this,
  have a' : (20 : ℤ) < 2147483648 := by { clear_except, norm_num, },
  exact gt_of_gt_of_ge a' this,
end

[Huỳnh Trần Khanh]

what might be causing this issue? this time i didn't use linarith... and i'm pretty sure that i'm not using slow tactics... so why on earth is this proof so slow lol

[Arthur Paulino]

Do you know exactly where the bottleneck is?

[Alex J. Best]

You can add set_option profiler true and then use sorry; { blah } to comment out parts of the proof and see where the slow point is

[Huỳnh Trần Khanh]

oh... this is so bizarre... i commented out most of the proof and it still takes forever to typecheck...

lemma split2 (input : list ℤ) (output : ℤ)
  (h : ∀ (x : ℤ), x ∈ input → -20 ≤ x ∧ x ≤ 20)
  (h' : input.length ≤ 30) :
  ∀ (x : ℤ),
    x ∈ [↑(input.length), ↑(input.length), input.sum] ++ input →
    within_bounds word_size_t.i32 x :=
begin
  intros x y,
  have := list.mem_append.mp y,
  cases this,
  clear_except this h h',
  cases this,
  rw this,
  clear_except h',
  simp only [get_right_bound, get_left_bound, within_bounds],
  split,
  {
    clear_except,
    have := int.coe_zero_le input.length,
    have a' : (-2147483648 : ℤ) ≤ 0 := by norm_num,
    exact le_trans a' this,
  },
  {
    have := int.coe_nat_le.mpr h',
    clear_except this,
    norm_num at this,
    have a' : (30 : ℤ) < 2147483648 := by norm_num,
    exact gt_of_gt_of_ge a' this,
  },
  sorry, sorry,
  -- cases this,
  -- rw this,
  -- clear_except h',
  -- simp only [get_right_bound, get_left_bound, within_bounds],
  -- split,
  -- {
  --   clear_except,
  --   have := int.coe_zero_le input.length,
  --   have a' : (-2147483648 : ℤ) ≤ 0 := by norm_num,
  --   exact le_trans a' this,
  -- },
  -- {
  --   have := int.coe_nat_le.mpr h',
  --   clear_except this,
  --   norm_num at this,
  --   have a' : (30 : ℤ) < 2147483648 := by norm_num,
  --   exact gt_of_gt_of_ge a' this,
  -- },
  -- cases this,
  -- rw this,
  -- clear_except h h',
  -- simp only [get_right_bound, get_left_bound, within_bounds],
  -- split,
  -- have a1 := x_le_sum input (-20 : ℤ) begin
  --   intros x y,
  --   exact (h x y).left,
  -- end,
  -- have a2 : -600 ≤ (↑input.length) * (-20 : ℤ) := begin
  --   clear_except h',
  --   have := (mul_le_mul_left_of_neg (show (-20 : ℤ) < (0 : ℤ), by { clear_except, norm_num, })).mpr (int.coe_nat_le.mpr h'),
  --   rw (show (-20 : ℤ) * (↑30 : ℤ) = -600, by norm_num) at this,
  --   rw mul_comm at this,
  --   exact this,
  -- end,
  -- have a3 : -600 ≤ input.sum := begin
  --   clear_except a1 a2,
  --   exact le_trans a2 a1,
  -- end,
  -- clear_except a3,
  -- {
  --   have a' : (-2147483648 : ℤ) ≤ -600 := by norm_num,
  --   exact le_trans a' a3,
  -- },
  -- have a1 := sum_le_x input 20 begin
  --   intros x y,
  --   exact (h x y).right,
  -- end,
  -- have a2 : (↑input.length) * (20 : ℤ) ≤ 600 := begin
  --   clear_except h',
  --   have := @mul_le_mul ℤ _ (↑input.length : ℤ) (20 : ℤ) (30 : ℤ) (20 : ℤ) begin
  --     have := int.coe_nat_le.mpr h',
  --     assumption,
  --   end (by norm_num) (by norm_num) (by norm_num),
  --   norm_num at this,
  --   assumption,
  -- end,
  -- have : input.sum ≤ 600 := begin
  --   clear_except a1 a2,
  --   exact le_trans a1 a2,
  -- end,
  -- clear_except this,
  -- {
  --   have a' : (600 : ℤ) < 2147483648 := by { clear_except, norm_num, },
  --   exact gt_of_gt_of_ge a' this,
  -- },
  -- clear_except this,
  -- exfalso,
  -- have := list.not_mem_nil x this,
  -- assumption,
  -- clear_except h this,
  -- have := h x this,
  -- clear_except this,
  -- simp only [get_right_bound, get_left_bound, within_bounds],
  -- split,
  -- have := this.left,
  -- clear_except this,
  -- {
  --   have a' : (-2147483648 : ℤ) ≤ -20 := by { clear_except, norm_num, },
  --   exact le_trans a' this,
  -- },
  -- have := this.right,
  -- clear_except this,
  -- have a' : (20 : ℤ) < 2147483648 := by { clear_except, norm_num, },
  -- exact gt_of_gt_of_ge a' this,
end

[Eric Wieser]

How fast are the norm_nums?

[Eric Wieser]

Try extracting those haves to their own lemmas

[Huỳnh Trần Khanh]

the norm nums are very fast apparently, most norm nums take less than 5ms to complete...

[Kevin Buzzard]

The moment you accidentally trigger something which attempts to unfold 2147483648 you're dead, I guess.

[Huỳnh Trần Khanh]

I think you are correct. because lean has finished elaborating the proof :joy:

[Huỳnh Trần Khanh]

next time I'll probably find a roundabout way to represent large constants because lean has a hard time dealing with them :cry:

[Kevin Buzzard]

Lean 3 does...