Zulip Chat Archive

Stream: general

Topic: Wlog for conjunction


view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:15):

wlog : a ≤ b → b ≤ a?

view this post on Zulip Johan Commelin (Jul 23 2020 at 17:16):

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

view this post on Zulip Johan Commelin (Jul 23 2020 at 17:16):

He is really kind, and very responsive!

view this post on Zulip 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

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:17):

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

view this post on Zulip Johan Commelin (Jul 23 2020 at 17:18):

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

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:18):

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

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:18):

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

view this post on Zulip 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

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:23):

Could you please post your code?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:27):

Oh! Of course! Thank you!

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:27):

How useful would you find having syntax for this?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Jul 23 2020 at 17:29):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:35):

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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:37):

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

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:37):

BTW, here is what ssreflect have.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:38):

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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:53):

I'm not fluent in ssreflect either...

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 17:59):

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

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 18:00):

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

view this post on Zulip 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?

view this post on Zulip 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".

view this post on Zulip 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?

view this post on Zulip Yury G. Kudryashov (Jul 23 2020 at 18:17):

Yes.

view this post on Zulip 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

view this post on Zulip 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: May 14 2021 at 12:18 UTC