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

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


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

But I guess you could use a more sensible tactic.

#### 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: May 06 2021 at 21:09 UTC