wlog is slow

Stream: general

[Kenny Lau]

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]

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]

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]

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]

looks like I need tactic.interactive.skip

[Kenny Lau]

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]

the case main is still here after the exact

[Alexander Bentkamp]

The discharger is only applied to case invariant

[Kenny Lau]

oh

[Kenny Lau]

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]

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]

So maybe simp would be a better default value?

[Kenny Lau]

simp is slow

[Alexander Bentkamp]

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

[Kenny Lau]

sure