Zulip Chat Archive

Stream: new members

Topic: arguing by symmetry


Marcus Zibrowius (Jul 03 2022 at 15:14):

In maths for humans, we frequently shortcut the second half of the proof of an equivalence or an equality by arguing by symmetry. Is there a way to emulate this with Lean's tactics?

For example, suppose my goal is an equality of sets A = B, and all my assumptions are symmetric in A and B. I would like to split the goal into two inclusions, prove one of them, and then just write some combination of symmetry and repeat for the other inclusion.

Does that make sense, and is it possible?

Eric Wieser (Jul 03 2022 at 15:40):

tactic#wlog can be used for that type of thing

Eric Wieser (Jul 03 2022 at 15:48):

More generally though, you can handle this manually with

suffices :  A B, p A  q B  A  B,
from set.subset.antisymm (this A B hA hB) (this B A hB hA),
-- now prove just one direction

Marcus Zibrowius (Jul 03 2022 at 19:52):

Thanks! After much contemplation, I think I've finally managed to figure out what the "manual" option is doing, and I got it to work in a baby case.

tactic#wlog also looks very stylish, but it's still unclear to me how to apply it in the kind of scenario I was asking about. I think I understand the example in the documentation, where for two natural numbers one can assume wlog m <= n because one can prove the disjunction (m <= n or n <= m). But what disjunction to look at for proving A(m,n) = A(n,m) or P(m,n) \<-> P(n,m)?

Kevin Buzzard (Jul 03 2022 at 20:20):

Can you post a #mwe ? You should hopefully be able to make a fully self-contained baby example/abstraction of the problem you want to solve.

Marcus Zibrowius (Jul 04 2022 at 06:44):

Sorry, I'm just asking out of curiosity and not because I'm running up against a problem. My baby example is from one of your sheets:

import tactic
open set

variables (X : Type) (A B : set X)

example : A  B = B  A :=
begin
  ext,
  split,
  -- **
end

At the point marked ** I have 2 goals which differ only by a permutation of the roles of A and B, so I'd like to say that it suffices to prove one of them.

Here's how I understood the "manual" solution (no invocation of ext and split):

begin
  suffices :  A' B': set X, A'  B'  B'  A',
  from set.subset.antisymm (this A B) (this B A),
  rintros A' B' x  hA, hB ⟩,
  exact  hB, hA⟩,
end

Kevin Buzzard (Jul 04 2022 at 07:06):

Right! So do you still have a question and if so can you formalise it?

Eric Wieser (Jul 04 2022 at 07:10):

I suspect the question is "how can use wlog to prove the above instead of suffices"

Marcus Zibrowius (Jul 04 2022 at 07:35):

Yes, that is the part I still don't understand.

Kevin Buzzard (Jul 04 2022 at 07:59):

I guess I don't know how to use WLOG in maths to solve this particular problem. WLOG is for things like "WLOG a<=b" when the goal is symmetric in a and b. I guess I'd use suffices here.

Johan Commelin (Jul 04 2022 at 08:03):

@Marcus Zibrowius I know this doesn't answer your question, but it might be nice to know that you can golf this to

example : A  B = B  A := by { ext, apply and.comm }

Marcus Zibrowius (Jul 04 2022 at 08:32):

@Kevin Buzzard OK, that's reassuring. So tactic#wlog applies in exactly the situations in which we'd usually say wlog, the situation I was wondering about is not one of them, and the confusion only arose because my initial question wasn't clear enough. Thank you.

Yakov Pechersky (Jul 04 2022 at 13:03):

Let's say your tactic proof for the first half cares that it's P(A, B) and not P(B, A). But the actually body would still hold if all the As were B and all the Bs were A. tactic#swap_var

Marcus Zibrowius (Jul 04 2022 at 15:32):

Right, three new commands I learn in this way :smile: (swap_var, work_on_goal, all_goals). Using swap_var does have the advantage over suffices ... that I don't need to explicitly type out what the goal is.

Eric Wieser (Jul 04 2022 at 16:16):

The downside in swap_var is that it's a little less robust, as instead of arguing mathematically that you only need to prove things in one direction, you're saying "just apply each of these steps to each direction separately".

Yakov Pechersky (Jul 04 2022 at 16:32):

Absolutely, it is a very dumb tactic that relies on getting the proof in _just_ the right way. But with that restriction, it is meant to be a very fast tactic.

Kyle Miller (Jul 04 2022 at 16:39):

Here's a variant on Eric's proof:

import tactic
open set

variables (X : Type) (A B : set X)

lemma inter_comm_aux : A  B  B  A :=
begin
  intro,
  rw [mem_inter_iff, mem_inter_iff, and_comm],
  apply id,
end

example : A  B = B  A :=
begin
  apply subset.antisymm; apply inter_comm_aux,
end

It's not uncommon to see an auxiliary lemma like this.

Eric Wieser (Jul 04 2022 at 16:40):

I think that's usually the case only if the auxiliary lemma holds true more generally than the bidirectional one (or provides more convenient notation)

Kyle Miller (Jul 04 2022 at 16:40):

(Don't mind that the specific proofs I used were different from Eric's. I just thought I'd mix things up by doing things more using tactics.)

Eric Wieser (Jul 04 2022 at 16:41):

Something like docs#commute.neg_left vs docs#commute.neg_left_iff is a good example of where it's better to add the auxiliary lemma like that

Patrick Johnson (Jul 05 2022 at 14:55):

If you really want to use wlog

import tactic
open_locale classical

example {X : Type} {A B : set X} : A  B = B  A :=
begin
  ext,
  by_contra h,
  wlog h₁ : x  A  B using [A B, B A],
  { tauto },
  rw not_iff at h,
  refine h.mpr _ h₁,
  rw set.mem_inter_iff at h₁ ,
  exact h₁.symm,
end

Emmanuel Beffara (Jul 11 2022 at 08:06):

Hello,

My question is also about how to transpose in Lean an argument by symmetry but when symmetry applies to hypotheses.

Say you have an inductive predicate P : X → Prop and a (provably symmetric) relation Q : X → X → Prop and you want to prove ∀ x y, P x → P y → Q x y. A direct way to proceed is along the lines of

theorem foo (x y : X) (Px : P x) (Py : P y) : Q x y :=
begin
  induction Px generalizing y; cases Py,
  -- lots of cases
end

If there are n cases in the definition of P, then you end up with cases, although the proof could be simplified into n(n+1)/2 by symmetry. Is there a tactic or a common practice to perform this simplification?

I did not include my actual use case for simplicity but I can provide it if relevant. The context is proving a confluence result, where P x means that x is a reduct of some term w and Q x y mean that x and y have a common reduct.

Yury G. Kudryashov (Jul 11 2022 at 10:23):

If you have some order, then you can use tactic#wlog. AFAIK, we don't have anything better yet.


Last updated: Dec 20 2023 at 11:08 UTC