# Zulip Chat Archive

## Stream: general

### Topic: wlog

#### Johan Commelin (Oct 05 2019 at 04:19):

@Simon Hudon Can you explain to me how I should invoke `wlog`

in this problem that is *clearly* (lol) symmetric:

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) : (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 := begin wlog : a ≤ b ∧ b ≤ c, end

#### Johan Commelin (Oct 05 2019 at 04:20):

Note that `wlog : a ≤ b`

succeeds after thinking for a long time.

#### Johan Commelin (Oct 05 2019 at 04:20):

I wouldn't mind if it dumps some proof obligations in my face. I can then manually select a hammer to kill them off.

#### Simon Hudon (Oct 05 2019 at 04:44):

What if you specified the variables on which the symmetry hinges? `wlog : a ≤ b ∧ b ≤ c using a b c,`

?

#### Johan Commelin (Oct 05 2019 at 04:47):

@Simon Hudon

To generate cases at least two permutations are required, i.e. `using [x y, y x]` or exactly 0 or 2 variables

#### Simon Hudon (Oct 05 2019 at 04:53):

You could do `wlog : a ≤ b ∧ b ≤ c using [a b c,b c a],`

#### Johan Commelin (Oct 05 2019 at 05:01):

You need 6 permutations, right?

#### Johan Commelin (Oct 05 2019 at 05:01):

And then it times out... @Simon Hudon

#### Johan Commelin (Oct 05 2019 at 05:02):

Huh... it works

#### Simon Hudon (Oct 05 2019 at 05:03):

You can file an issue. I'll have a closer look later

#### Johan Commelin (Oct 05 2019 at 05:03):

Ooh, no, it doesn't. It generates a side goal that is false.

#### Johan Commelin (Oct 05 2019 at 05:07):

@Simon Hudon #1509

#### Johan Commelin (Nov 12 2019 at 06:59):

@Simon Hudon Do you have any thoughts on this issue?

#### Alexander Bentkamp (Nov 13 2019 at 21:03):

I just found out that there is another parameter of this tactic: `discharger : tactic unit`

. Its default value is `tactic.solve_by_elim <|> tactic.tautology tt <|> using_smt (smt_tactic.intros >> smt_tactic.solve_goals)`

, which is the reason `wlog`

takes so long. If you use `skip`

instead, `wlog`

is very fast. Of course, the disadvantage is that you get a lot of stupid goals afterwards.

lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) : (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 := begin wlog : a ≤ b ∧ b ≤ c using [a b c, c a b, b c a, c b a, b a c, a c b] skip, end

#### Johan Commelin (Nov 13 2019 at 21:29):

Thanks, that looks very helpful!

#### Chris Hughes (Nov 13 2019 at 21:31):

But I guess you could use a more sensible tactic.

#### Simon Hudon (Nov 13 2019 at 21:33):

I thought that had been changed in mathlib already

#### Alexander Bentkamp (Nov 13 2019 at 21:53):

Let us know if you find a nice way to discharge these goals. Maybe there could be a different default value for `discharger`

?

#### Alexander Bentkamp (Nov 15 2019 at 17:40):

@Johan Commelin With an auxiliary lemma for wlog with three variables, we can speed this up a lot. Maybe this lemma `wlog3`

should be in mathlib:

lemma wlog3 {α : Type*} [linear_order α] (p : α → α → α → Prop) (x y z : α) (h₁ : ∀ a b c, p a b c → p b a c) (h₂ : ∀ a b c, p a b c → p a c b) (hp : ∀ a b c, a ≤ b ∧ b ≤ c → p a b c) : p x y z := begin have h₃ : ∀ (a b c : α), p a b c → p c a b, { intros, apply h₁, apply h₂, assumption }, wlog : x ≤ y ∧ y ≤ z using [x y z, y z x, z x y, z y x, y x z, x z y], { cases le_total x y with hc₁; cases le_total y z with hc₂; cases le_total x z with hc₃; cc }, { apply hp, assumption }, end lemma forty_two (a b c : ℕ) (h : (0:ℚ) < 1 - (1/a + 1/b + 1/c)) : (1:ℚ)/(1 - (1/a + 1/b + 1/c)) ≤ 42 := begin revert h, apply wlog3 _ a b c, { intros a b c h, change implies _ _, convert h using 3, ac_refl, ac_refl}, { intros a b c h, change implies _ _, convert h using 3, ac_refl, ac_refl}, sorry end

The trick is that we actually do not need to consider all 5 non-identity permutations. Just 2 permutations are enough to express all others.

Unfortunately, I don't see a fast way to discharge the resulting goals in a way that is both fast and generally applicable.

#### Simon Hudon (Nov 15 2019 at 18:31):

We could tag `wlog3`

with a `wlog`

attribute and get the tactic `wlog`

to try those before trying the `discharger`

#### Johan Commelin (Nov 15 2019 at 19:18):

@Alexander Bentkamp Thanks a lot for looking at this!

#### Johan Commelin (Nov 15 2019 at 19:19):

It's already a lot better than the mess that I initially had :wink:

#### Johan Commelin (Nov 15 2019 at 19:19):

I'm still hoping that tactics could crunch away more of the administrative parts of the proof.

#### Johan Commelin (Nov 15 2019 at 19:20):

It would be nice if one could drill down to the heart of the matter in <5 lines

#### Alexander Bentkamp (Nov 15 2019 at 19:20):

You can replace

{ intros a b c h, change implies _ _, convert h using 3, ac_refl, ac_refl},

by `cc`

. But unfortunately, that's very slow. I am not sure why.

Last updated: Dec 20 2023 at 11:08 UTC