Zulip Chat Archive

Stream: general

Topic: Wlog for conjunction

Simon Hudon (Jul 23 2020 at 17:13):

wlog is pretty good I think at adopting assumptions of the kind a ≤ b when there's a symmetry between a and b and that the order is total. I'd like to use it to prove a ≤ b /\ b ≤ a by only showing a ≤ b. Has anyone tried it? Any success?

Yury G. Kudryashov (Jul 23 2020 at 17:15):

wlog : a ≤ b → b ≤ a?

Johan Commelin (Jul 23 2020 at 17:16):

@Simon Hudon You should ask the author of wlog :wink:

Johan Commelin (Jul 23 2020 at 17:16):

He is really kind, and very responsive!

Simon Hudon (Jul 23 2020 at 17:17):

@Johan Commelin I already sound crazy talking to myself alone in my apartment, I need to speak to living beings

Simon Hudon (Jul 23 2020 at 17:17):

Thanks! I didn't think I was that responsive. I'm pretty absent lately

Johan Commelin (Jul 23 2020 at 17:18):

Ooh, but whenever someone pings you, you're there

Simon Hudon (Jul 23 2020 at 17:18):

@Yury G. Kudryashov Thanks for the suggestion. I need to wrap my head around it

Simon Hudon (Jul 23 2020 at 17:18):

Thanks! I'm glad I'm not missed too much :)

Simon Hudon (Jul 23 2020 at 17:22):

@Yury G. Kudryashov

I get blocked here:

case main
j i : ℕ,
case : i ≤ j → j ≤ i
⊢ i = j

Yury G. Kudryashov (Jul 23 2020 at 17:23):

Could you please post your code?

Simon Hudon (Jul 23 2020 at 17:24):

Certainly:

example (i j : ℕ) : i = j :=
begin
  wlog : (i ≤ j → j ≤ i),
    -- 2 goals
    -- case cases
    -- i j : ℕ
    -- ⊢ (i ≤ j → j ≤ i) ∨ (j ≤ i → i ≤ j)

    -- case main
    -- j i : ℕ,
    -- case : i ≤ j → j ≤ i
    -- ⊢ i = j

end

Johan Commelin (Jul 23 2020 at 17:25):

I'm confused... don't you want a \le b \or b \le a? Instead of \and?

Yury G. Kudryashov (Jul 23 2020 at 17:26):

In the case main you should somehow prove H : i ≤ j, then use le_antisymm H (case H).

Simon Hudon (Jul 23 2020 at 17:27):

Oh! Of course! Thank you!

Simon Hudon (Jul 23 2020 at 17:27):

How useful would you find having syntax for this?

Yury G. Kudryashov (Jul 23 2020 at 17:28):

I saw several people coming with questions like this one on Zulip, so I think this is useful.

Simon Hudon (Jul 23 2020 at 17:29):

What do you think of wlog show i ≤ j using [i j]?

Yury G. Kudryashov (Jul 23 2020 at 17:33):

Another feature request: being able to say wlog : p generalizing H1 H2 (possibly under a different name). It should revert H1 H2, then replace the goal G with the pair of goals p → G, (p → G) → G.

Yury G. Kudryashov (Jul 23 2020 at 17:34):

This is useful, e.g., if I want to say wlog : 0 ≤ x and in the general case do cases on le_total 0 x.

Yury G. Kudryashov (Jul 23 2020 at 17:35):

Or if I have ε > 0 and want to add ε < 1 to the context.

Simon Hudon (Jul 23 2020 at 17:36):

This is useful, e.g., if I want to say wlog : 0 ≤ x and in the general case do cases on le_total 0 x.

I don't see the connection between the two. Wouldn't you deal with that situation with wlog : 0 ≤ x := le_total 0 x?

Yury G. Kudryashov (Jul 23 2020 at 17:37):

Currently wlog assumes that other cases follow from the "main" case by permutation of variables.

Yury G. Kudryashov (Jul 23 2020 at 17:37):

BTW, here is what ssreflect have.

Yury G. Kudryashov (Jul 23 2020 at 17:38):

I do not suggest copying the whole syntax (some of it is not very readable).

Simon Hudon (Jul 23 2020 at 17:43):

Thanks for the reference. I'm still not fluent in ssreflect, I should really get to it

Simon Hudon (Jul 23 2020 at 17:44):

With your le_total example, can you show me the goals you'd expect the tactic to produce?

Yury G. Kudryashov (Jul 23 2020 at 17:53):

I'm not fluent in ssreflect either...

Yury G. Kudryashov (Jul 23 2020 at 17:56):

example (m n : ℤ) : m + n = n + m :=
begin
  suffices : 0 ≤ m → ∀ n : ℤ, m + n = n + m,
  { sorry },
  sorry
end

Yury G. Kudryashov (Jul 23 2020 at 17:57):

I don't want any "clever" tactic here, just a replacement for this suffices that allows me not to copy the goal.

Yury G. Kudryashov (Jul 23 2020 at 17:59):

A "clever" version could take abs as another argument.

Yury G. Kudryashov (Jul 23 2020 at 18:00):

And ask for proofs 0 ≤ abs m and H (abs m) → H m.

Simon Hudon (Jul 23 2020 at 18:07):

Ok, I think I see what you mean. You'd be achieving that effect with wlog : 0 ≤ m := le_total 0 m generalizing n. Is this what you have in mind?

Yury G. Kudryashov (Jul 23 2020 at 18:13):

I don't need le_total 0 m here because in the ε > 0 case I want to say "OK, we only care about small ε, so assume ε ≤ 1; in the general case we set ε' := min ε 1 and apply the new lemma".

Simon Hudon (Jul 23 2020 at 18:17):

Ok, but otherwise, in the example with suffices, n is the variable you want to generalize, right?

Yury G. Kudryashov (Jul 23 2020 at 18:17):

Yes.

Simon Hudon (Jul 23 2020 at 18:19):

Ok, I think I get it. Let me see how I'm going to make it fit. wlog has a lot of nice features but it has really grown into a real mess

Simon Hudon (Jul 23 2020 at 20:10):

In the case of wlog show i ≤ j, do we care about more two permutations and if so do we want it to behave like wlog : A -> B -> C using [i j k, j k i, k i j]?

Last updated: Dec 20 2023 at 11:08 UTC