Zulip Chat Archive

Stream: general

Topic: wlog is slow


Kenny Lau (Apr 26 2020 at 16:26):

import tactic.wlog

set_option profiler true

-- elaboration of wlog_is_slow took 2.22s
theorem wlog_is_slow (x y : ) (h1 : x ^ y = 3) (h2 : x ^ y = 3) (h3 : x ^ y = 3) (h4 : x ^ y = 3) :
   m n, x = m  y = n  x + y = m + n  x * y = m * n  x ^ y = m ^ n :=
begin
  wlog hxy : x  y using [x y, y x],
end

Kenny Lau (Apr 26 2020 at 16:28):

completed version:

import tactic.wlog

set_option profiler true

-- elaboration of wlog_is_slow took 2.62s
theorem wlog_is_slow (x y : ) (h1 : x ^ y = 3) (h2 : x ^ y = 3) (h3 : x ^ y = 3) (h4 : x ^ y = 3) :
   m n, x = m  y = n  x + y = m + n  x * y = m * n  x ^ y = m ^ n :=
begin
  wlog hxy : x  y := le_total x y using [x y, y x],
  exact x, y, rfl, rfl, rfl, rfl, rfl
end

Alexander Bentkamp (Apr 27 2020 at 15:33):

wlog has an undocumented argument called discharger. If you set it to something other than the default value, wlog can be faster. Just try wlog hxy : x ≤ y := le_total x y using [x y, y x] skip, to get started. Maybe you have an idea what could be a good default for discharger?

Kenny Lau (Apr 27 2020 at 15:35):

import tactic.wlog

-- unknown identifier 'skip'
theorem wlog_is_buggy (x y : ) (h1 : x ^ y = 3) (h2 : x ^ y = 3) (h3 : x ^ y = 3) (h4 : x ^ y = 3) :
   m n, x = m  y = n  x + y = m + n  x * y = m * n  x ^ y = m ^ n :=
begin
  wlog hxy : x  y := le_total x y using [x y, y x] skip,
  exact x, y, rfl, rfl, rfl, rfl, rfl
end
#check tactic.interactive.skip -- tactic.interactive.skip : tactic unit

Kenny Lau (Apr 27 2020 at 15:36):

looks like I need tactic.interactive.skip

Kenny Lau (Apr 27 2020 at 15:40):

it doesn't even do anything:

import tactic.wlog

theorem wlog_is_buggy (x y : ) (h1 : x ^ y = 3) (h2 : x ^ y = 3) (h3 : x ^ y = 3) (h4 : x ^ y = 3) :
   m n, x = m  y = n  x + y = m + n  x * y = m * n  x ^ y = m ^ n :=
begin
  wlog hxy : x  y := le_total x y using [x y, y x] (tactic.interactive.exact ```(x, y, rfl, rfl, rfl, rfl, rfl))
/-
case main
x y : ℕ,
hxy : x ≤ y,
h1 h2 h3 h4 : x ^ y = 3
⊢ ∃ (m n : ℕ), x = m ∧ y = n ∧ x + y = m + n ∧ x * y = m * n ∧ x ^ y = m ^ n

case invariant
x y : ℕ,
hxy : y ≤ x,
this :
  y ^ x = 3 →
  y ^ x = 3 →
  y ^ x = 3 → y ^ x = 3 → (∃ (m n : ℕ), y = m ∧ x = n ∧ y + x = m + n ∧ y * x = m * n ∧ y ^ x = m ^ n)
⊢ x ^ y = 3 →
  x ^ y = 3 →
  x ^ y = 3 → x ^ y = 3 → (∃ (m n : ℕ), x = m ∧ y = n ∧ x + y = m + n ∧ x * y = m * n ∧ x ^ y = m ^ n)
-/
end

Kenny Lau (Apr 27 2020 at 15:40):

the case main is still here after the exact

Alexander Bentkamp (Apr 27 2020 at 15:54):

The discharger is only applied to case invariant

Kenny Lau (Apr 27 2020 at 15:55):

oh

Kenny Lau (Apr 27 2020 at 15:56):

ok, this works:

import tactic.wlog

theorem wlog_is_awkward (x y : ) (h1 : x ^ y = 3) (h2 : x ^ y = 3) (h3 : x ^ y = 3) (h4 : x ^ y = 3) :
   m n, x = m  y = n  x + y = m + n  x * y = m * n  x ^ y = m ^ n :=
begin
  wlog hxy : x  y := le_total x y using [x y, y x] (tactic.interactive.exact ```(λ _ _ _ _, x, y, rfl, rfl, rfl, rfl, rfl)),
  exact x, y, rfl, rfl, rfl, rfl, rfl
end

Alexander Bentkamp (Apr 27 2020 at 16:01):

In this example, simp also woks:

wlog hxy : x  y := le_total x y using [x y, y x] (interactive.simp none false [] [] (interactive.loc.wildcard) {}),

(although I just had a hard time to pass the arguments to interactive.simp)

Alexander Bentkamp (Apr 27 2020 at 16:02):

So maybe simp would be a better default value?

Kenny Lau (Apr 27 2020 at 16:02):

simp is slow

Alexander Bentkamp (Apr 27 2020 at 16:02):

Not as slow as the current value of the discharger for sure

Kenny Lau (Apr 27 2020 at 16:03):

sure


Last updated: Dec 20 2023 at 11:08 UTC