WLOG

Stream: new members

[Ali Sever]

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]

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]

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]

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

[Mario Carneiro]

import tactic.wlog

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

[Mario Carneiro]

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

[Ali Sever]

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]

What's the goal?

[Mario Carneiro]

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]

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]

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]

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]

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

[Ali Sever]

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]

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]

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]

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

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

[Ali Sever]

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