# Zulip Chat Archive

## Stream: new members

### Topic: WLOG

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

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

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

#### Mario Carneiro (Aug 14 2018 at 09:53):

i.e. you want to prove `x * y <= 1`

, then wlog you can assume `x <= y`

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

#### Mario Carneiro (Aug 14 2018 at 09:56):

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

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

#### Mario Carneiro (Aug 14 2018 at 10:06):

What's the goal?

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

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

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

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

#### Ali Sever (Aug 14 2018 at 11:01):

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

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

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

.

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

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

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

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