Zulip Chat Archive

Stream: general

Topic: wlog


view this post on Zulip 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

view this post on Zulip Johan Commelin (Oct 05 2019 at 04:20):

Note that wlog : a ≤ b succeeds after thinking for a long time.

view this post on Zulip 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.

view this post on Zulip 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,?

view this post on Zulip 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

view this post on Zulip Simon Hudon (Oct 05 2019 at 04:53):

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

view this post on Zulip Johan Commelin (Oct 05 2019 at 05:01):

You need 6 permutations, right?

view this post on Zulip Johan Commelin (Oct 05 2019 at 05:01):

And then it times out... @Simon Hudon

view this post on Zulip Johan Commelin (Oct 05 2019 at 05:02):

Huh... it works

view this post on Zulip Simon Hudon (Oct 05 2019 at 05:03):

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

view this post on Zulip Johan Commelin (Oct 05 2019 at 05:03):

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

view this post on Zulip Johan Commelin (Oct 05 2019 at 05:07):

@Simon Hudon #1509

view this post on Zulip Johan Commelin (Nov 12 2019 at 06:59):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 13 2019 at 21:29):

Thanks, that looks very helpful!

view this post on Zulip Chris Hughes (Nov 13 2019 at 21:31):

But I guess you could use a more sensible tactic.

view this post on Zulip Simon Hudon (Nov 13 2019 at 21:33):

I thought that had been changed in mathlib already

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 15 2019 at 19:18):

@Alexander Bentkamp Thanks a lot for looking at this!

view this post on Zulip Johan Commelin (Nov 15 2019 at 19:19):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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