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

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