Zulip Chat Archive

Stream: new members

Topic: WLOG


view this post on Zulip Ali Sever (Aug 14 2018 at 09:48):

I'm trying to get more efficient in my proofs, so I want to learn about the wlog tactic, but I didn't understand the comments where the tactic was written. Are there any examples I can read (preferably about something I could understand)?

view this post on Zulip Sean Leather (Aug 14 2018 at 09:51):

Not to derail your question entirely, but I also recently had issues trying to understand the comments. In particular, it started with the summary:

Without loss of generality: reduces to one goal under variables permutations

What does “reduces to one goal under variables permutations” mean?

view this post on Zulip Mario Carneiro (Aug 14 2018 at 09:52):

wlog applies when the goal is symmetric under permutation of some variables, and there is a "symmetry breaking" relation that holds when disjoined over all permutations

view this post on Zulip Mario Carneiro (Aug 14 2018 at 09:53):

i.e. you want to prove x * y <= 1, then wlog you can assume x <= y

view this post on Zulip Mario Carneiro (Aug 14 2018 at 09:55):

import tactic.wlog

example (x y : ) : x * y  1 :=
begin
  wlog h : x  y,
  -- x ≤ y ⊢ x * y ≤ 1
end

view this post on Zulip Mario Carneiro (Aug 14 2018 at 09:56):

I agree the wording is not very good. I invite suggestions for rewording

view this post on Zulip Ali Sever (Aug 14 2018 at 10:04):

The wlog I want to do is a little more complicated, for example I have ( p(a) \or p(b) ), where p is a pseudo-order relation. I also have stuff like h1 : p(a) → c and h2 : p(b) → d, so I want to include these in my wlog.

view this post on Zulip Mario Carneiro (Aug 14 2018 at 10:06):

What's the goal?

view this post on Zulip Mario Carneiro (Aug 14 2018 at 10:07):

what do you mean by pseudo order relation? wlog is very general, so I'm sure it will apply, but you have to figure out how to get it in a form it can accept

view this post on Zulip Ali Sever (Aug 14 2018 at 10:22):

I want to wlog over a b c d where I have p a b c d \or p c d a b, I just tried wlog h : p a b c d and it asked me for a proof of p a b c d \or p c d a b, which was very surprising. Sometimes Lean is a lot smarter than I expect.

view this post on Zulip Ali Sever (Aug 14 2018 at 10:39):

So I started the wlog proof, and I finished the first case. Now for the second case it wants a proof of h1 : p(b) → c and h1 : p(a) → d, but those aren't true. How would I tell Lean to add c and d to the wlog, so they swap as well for the second case?

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 10:58):

Ali -- can you formalise a MWE of what you're asking? i.e. abstract the situation and post a problem of the form example (alpha : type) (p : alpha -> alpha -> alpha -> alpha -> Prop) (h1 : blah -> blah) (h2 : blah) ... : goal := sorry and set it as a WLOG challenge.

view this post on Zulip Ali Sever (Aug 14 2018 at 11:01):

I was fearing this, I'll see what I can do.

view this post on Zulip Ali Sever (Aug 14 2018 at 12:09):

Here's a MWE:

import tactic.wlog
variables {α : Type}

def E : α  α  α  α  Prop := sorry

def B : α  α  α  Prop := sorry

def D : α  α  α  α  Prop := sorry

def S : α  α  α  Prop := sorry

lemma S.symm {a b c : α} : S a b c  S a c b := sorry

lemma B.symm {a b c : α} : B a b c  B a c b := sorry

lemma E.flip {a b c d : α} : E a b c d  E b a d c := sorry

theorem t1 (a b c d : α) : D a b c d  D c d a b := sorry

theorem t2 {a b c d p q r s : α} : D a b c d  E a b p q  E c d r s  D p q r s := sorry

theorem t3 {a b c : α} : S a b c  D a b a c  B a b c := sorry

theorem t4 {a b c p q r : α} : B a b c  B p q r  E a b p q  E a c p r  E b c q r := sorry

-- Had to name it a₁ because Lean didn't let me use a on line 39?
example {a₁ b c p q r : α} : S a₁ b c  S p q r  E a₁ b p q  E a₁ c p r  E b c q r :=
begin
intros h h1 h2 h3,
wlog h4 : D a₁ b a₁ c,
    exact t1 a₁ b a₁ c,
  have h5 : D p q p r,
    exact t2 h4 h2 h3,
  have h6 : B a₁ b c,
    exact t3 h h4,
  have h7 : B p q r,
    exact t3 h1 h5,
  exact t4 h6 h7 h2 h3,
have hx :  p q r, S a₁ c b  S p q r  E a₁ c p q  E a₁ b p r  E c b q r := sorry,
-- This is what I would expect the WLOG to give me to use as "this",
exact (hx p r q h.symm h1.symm h3 h2).flip
end

--A way around this is to change the statement, but that isn't ideal

example {a₁ b c : α} : S a₁ b c   p q r, S p q r  E a₁ b p q  E a₁ c p r  E b c q r :=
begin
intros h,
wlog h4 : D a₁ b a₁ c,
    exact t1 a₁ b a₁ c,
  introv h1 h2 h3,
  have h5 : D p q p r,
    exact t2 h4 h2 h3,
  have h6 : B a₁ b c,
    exact t3 h h4,
  have h7 : B p q r,
    exact t3 h1 h5,
  exact t4 h6 h7 h2 h3,
exact (this h.symm p r q a.symm a_2 a_1).flip
end

view this post on Zulip Ali Sever (Aug 14 2018 at 12:09):

I'd also like to know how to name everything WLOG gives me, and why I had to use a₁ instead of a.

view this post on Zulip Patrick Massot (Aug 14 2018 at 12:49):

You should never try to name anything a in Lean. That's a name Lean uses, and trying to also use it can only lead to cryptic error messages

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 12:58):

-- your example, upgraded to theorem t5
theorem t5 {a₁ b c : α} : S a₁ b c   p q r, S p q r  E a₁ b p q  E a₁ c p r  E b c q r :=
begin
intros h,
wlog h4 : D a₁ b a₁ c,
    exact t1 a₁ b a₁ c,
  introv h1 h2 h3,
  have h5 : D p q p r,
    exact t2 h4 h2 h3,
  have h6 : B a₁ b c,
    exact t3 h h4,
  have h7 : B p q r,
    exact t3 h1 h5,
  exact t4 h6 h7 h2 h3,
exact (this h.symm p r q a.symm a_2 a_1).flip
end

-- what you wanted
example {a₁ b c p q r : α} : S a₁ b c  S p q r  E a₁ b p q  E a₁ c p r  E b c q r :=
begin
  intro h,
  revert p q r,
  exact t5 h,
end

view this post on Zulip Kevin Buzzard (Aug 14 2018 at 12:59):

The a thing is a bug in the parser, which won't be fixed until Lean 4.

view this post on Zulip Ali Sever (Aug 14 2018 at 13:02):

Ok thanks, I was hoping wlog could revert for me,


Last updated: May 14 2021 at 06:16 UTC