wlog

Stream: general

[Johan Commelin]

@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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

@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]

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

[Johan Commelin]

You need 6 permutations, right?

[Johan Commelin]

And then it times out... @Simon Hudon

[Johan Commelin]

Huh... it works

[Simon Hudon]

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

[Johan Commelin]

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

[Johan Commelin]

@Simon Hudon #1509

[Johan Commelin]

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

[Alexander Bentkamp]

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]

Thanks, that looks very helpful!

[Chris Hughes]

But I guess you could use a more sensible tactic.

[Simon Hudon]

I thought that had been changed in mathlib already

[Alexander Bentkamp]

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]

@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]

We could tag wlog3 with a wlog attribute and get the tactic wlog to try those before trying the discharger

[Johan Commelin]

@Alexander Bentkamp Thanks a lot for looking at this!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Alexander Bentkamp]

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.