Zulip Chat Archive

Stream: Is there code for X?

Topic: by symmetry


view this post on Zulip Greg Price (Apr 11 2021 at 22:25):

I have a proof that I'd like to be able to write in a shape like this:

import topology.opens
open function

example (α β : Type) (f : set α  β) : injective f :=
begin
  assume S T (hST : f S = f T),
  ext x,
  show x  S  x  T, symmetry'', -- hypothetical tactic
  show x  S  x  T, sorry -- some longish proof
end

That is, I have a goal of the form p S ↔ p T, and all my hypotheses are symmetrical on swapping S and T. I'd like to reduce the goal to just proving one direction p S → p T, "because obviously it's all symmetric."

Is there a tactic that can do this for me?

view this post on Zulip Yakov Pechersky (Apr 11 2021 at 22:30):

wlog can do this for inequalities. In your case, you have S \le T and T \le S, if you do apply le_antisymm instead of ext x

view this post on Zulip Greg Price (Apr 11 2021 at 22:32):

Hmm interesting! I'll try that

view this post on Zulip Greg Price (Apr 11 2021 at 22:34):

Here's what I get from one attempt at using wlog:

example (α β : Type) (f : set α  β) : injective f :=
begin
  assume S T (hST : f S = f T),
  apply le_antisymm,
  wlog : T  S using S T,
  /-
  3 goals
  case cases
  α β : Type,
  f : set α → β,
  S T : set α,
  hST : f S = f T
  ⊢ T ≤ S ∨ S ≤ T

  case main
  α β : Type,
  f : set α → β,
  S T : set α,
  case : T ≤ S,
  hST : f S = f T
  ⊢ S ≤ T

  α β : Type,
  f : set α → β,
  S T : set α,
  hST : f S = f T
  ⊢ T ≤ S
  -/

view this post on Zulip Greg Price (Apr 11 2021 at 22:35):

I'm clearly doing something wrong there because the first goal isn't even true a priori (not without basically proving the original goal)

view this post on Zulip Greg Price (Apr 11 2021 at 22:40):

I guess another version of the question is, if I just apply le_antisymm instead of the ext x, then I have these two goals:

αβ: Type
f: set α → β
ST: set α
hST: f S = f T
⊢ S ≤ T

αβ: Type
f: set α → β
ST: set α
hST: f S = f T
⊢ T ≤ S

And the thing I want to do is provide a proof of one of them, and somehow use that to discharge the other. Which will be by somehow using the fact that if you swap the variable names and apply symmetry to hST, that turns the one goal into the other one.

But I'm not seeing the match between that and what wlog does -- it seems to want to split the goal into more goals, not coalesce symmetrical goals.

view this post on Zulip Yakov Pechersky (Apr 11 2021 at 22:57):

example (α β : Type) (f : set α  β) : function.injective f :=
begin
  assume S T (hST : f S = f T),
  wlog : T  S using T S,
  { -- pick one of the directions of `T ≤ S` or `S ≤ T` to prove here
    sorry },
  { -- now knowing that `T ≤ S`, use that to prove `T = S` using your "longish proof"
    sorry }
end

view this post on Zulip Greg Price (Apr 11 2021 at 22:58):

Hmm -- but how does that avoid repeating the main proof twice?

view this post on Zulip Greg Price (Apr 11 2021 at 22:59):

Once for TS T \leq S and once for ST S \leq T

view this post on Zulip Yakov Pechersky (Apr 11 2021 at 23:00):

maybe it'll be easier to understand if you have the actual mathematical setup

view this post on Zulip Greg Price (Apr 11 2021 at 23:00):

Sure, one moment

view this post on Zulip Greg Price (Apr 11 2021 at 23:03):

The details of the proof are rather messy at present, but here it is:

import topology.instances.real
import topology.opens

open function
open metric
open topological_space
open_locale cardinal
open_locale topological_space

namespace cardinal

lemma mk_opens_R_aux : #(opens )  #(set ( × )) :=
-- An open set in ℝ is uniquely determined by the rational balls included in it.
-- (Any dense set would do just as well in place of ℚ.)
let f (S : opens ) : set ( × ) := { p | ball (p.1 : ) p.2  S } in
mk_le_of_injective (show injective f, by {
  assume S T hST,
  ext x, split, {
    assume hxS,
    have : S  𝓝 x, from mem_nhds_sets S.property hxS,
    rcases mem_nhds_iff.mp this with ε, hεpos, hball⟩⟩,
    rcases exists_pos_rat_lt (half_pos hεpos) with εQ, h0εQ, hεQ⟩⟩,
    have : ball x (εQ)  𝓝 x, from ball_mem_nhds x (rat.cast_pos.mpr h0εQ),
    apply exists.elim (dense_embedding_of_rat.dense.inter_nhds_nonempty this),
    rintro yR ⟨⟨yQ, hy⟩, hyballx⟩,
    have : dist yR x < εQ, from set.mem_def.mp hyballx,
    have : ball (yQ : ) εQ  ball x ε, by { apply ball_subset, rw hy, linarith },
    have : ball (yQ : ) εQ  S, from set.subset.trans this hball,
    have : (yQ, εQ)  f S, from set.mem_def.mpr this,
    have : (yQ, εQ)  f T, from hST  this,
    have : ball (yQ : ) εQ  T, from set.mem_def.mp this,
    have hyballT : ball yR εQ  T, from hy  this,
    exact set.mem_of_subset_of_mem hyballT (mem_ball_comm.mp hyballx),
  },

  sorry, -- "by symmetry"
})

view this post on Zulip Greg Price (Apr 11 2021 at 23:05):

(I think all the details in that block after split don't matter, except to see why I don't want to just say it twice with S and T swapped)

view this post on Zulip Yaël Dillies (Apr 13 2021 at 08:28):

Another trick would be to prove the implication for general variables (X, Y) first, and then apply it twice: once on (S, T) and once on (T, S).

open function

example (α β : Type) (f : set α → β) : injective f :=
begin
  assume S T (hST : f S = f T),
  have aux_lemma : ∀ X Y : whatever_S_and_T_are, any_condition_on_S_and_T → S ⊆ T := sorry,
  have : S = T := subset.antisymm (aux_lemma S T conditions_on_S conditions_on_T) (aux_lemma T S conditions_on_T conditions_on_S),
end```
It would be great if a tactic could figure out how to change the goal on its own, but I slightly doubt it's feasible.

view this post on Zulip Greg Price (Apr 14 2021 at 06:13):

Thanks! Yeah, that's the best existing solution I've found.

view this post on Zulip Greg Price (Apr 14 2021 at 06:20):

For my example above, it might look like:

lemma mk_opens_R_aux : #(opens )  #(set ( × )) :=
-- An open set in ℝ is uniquely determined by the rational balls included in it.
-- (Any dense set would do just as well in place of ℚ.)
let f (S : opens ) : set ( × ) := { p | ball (p.1 : ) p.2  S } in
mk_le_of_injective (show injective f, from
suffices  S T, f S = f T  S  T,
  from assume S T hST, opens.ext $ set.subset.antisymm (this S T hST) (this T S hST.symm),
by {
  assume S T hST,
  assume x hxS,
  have : S  𝓝 x, from mem_nhds_sets S.property hxS,
  -- … same long detailed proof as before …
  sorry,
})

view this post on Zulip Greg Price (Apr 14 2021 at 06:26):

I don't find that totally satisfying, because it feels like a fair bit of fuss for what in a paper/blackboard proof would be done almost without comment, and it feels like something that should in principle be totally possible for a computer to see.

But I guess there isn't currently code around that can do it. Maybe I'll see if if I can figure out how to make a tactic that does. :smile:

view this post on Zulip Mario Carneiro (Apr 14 2021 at 06:31):

Yeah, wlog doesn't handle "by symmetry" proofs of this form. It can case split on S <= T \/ T <= S but that doesn't make sense here because opens real is not totally ordered.

view this post on Zulip Greg Price (Apr 14 2021 at 06:31):

Yeah, that makes sense

view this post on Zulip Mario Carneiro (Apr 14 2021 at 06:37):

FWIW I would set up your proof like this:

lemma mk_opens_R_aux : #(opens )  #(set ( × )) :=
begin
  -- An open set in ℝ is uniquely determined by the rational balls included in it.
  -- (Any dense set would do just as well in place of ℚ.)
  let f := λ (S : opens ), {p :  ×  | ball (p.1 : ) p.2  S},
  suffices :  {S T}, f S = f T  S  T,
  { exact @mk_le_of_injective _ _ f (λ S T hST, (this hST).antisymm (this hST.symm)) },
  intros S T hST x hxS,
  have : S  𝓝 x, from mem_nhds_sets S.property hxS,
  ... -- as before
end

view this post on Zulip Greg Price (Apr 14 2021 at 06:39):

Thanks. Ah, yeah, the {S T} trick simplifies that next line. And using \le instead of \sub means skipping the opens.ext translation.

view this post on Zulip Scott Morrison (Apr 14 2021 at 06:39):

Presumably the commented fact "An open set in ℝ is uniquely determined by the [any dense set] balls included in it." is itself a mathlib worthy lemma, separated from any cardinality facts.

view this post on Zulip Greg Price (Apr 14 2021 at 06:40):

I'd be happy to PR it! I will certainly clean up the proof first (most of all in the parts that come after the part this question is about.)

view this post on Zulip Mario Carneiro (Apr 14 2021 at 06:41):

the statement can also be stated in terms of 2^omega

view this post on Zulip Greg Price (Apr 14 2021 at 06:42):

I was writing it up as the main part of another fun fact about the open sets in ℝ:

/-- The open sets in ℝ have the same cardinality as ℝ. -/
-- Probably the right level of generality for this is a separable... uniform space?
-- At least any separable metric space.
lemma mk_opens_R : #(opens ) = # :=

which I think likely also belongs in mathlib. Though it's possible the main work needed for that is already present -- I looked in places specific to ℝ but haven't tried to find it in the places where the main lemma at the right level of generality would live.

view this post on Zulip Greg Price (Apr 14 2021 at 06:43):

(And as the comment says, I haven't even worked out yet at a mathematical level what level of generality that is.)

view this post on Zulip Greg Price (Apr 14 2021 at 07:19):

Mario Carneiro said:

  { exact @mk_le_of_injective _ _ f (λ S T hST, (this hST).antisymm (this hST.symm)) },

Ah, and the reason you're using @mk_le_of_injective there is to specify f, which is the same effect my version above was getting with show injective f,.

I do like show when it makes things clearer, but here it really isn't adding anything beyond specifying f.

view this post on Zulip Mario Carneiro (Apr 14 2021 at 08:40):

@Greg Price Here's a golf of the remainder of your proof, without fundamentally changing the proof approach:

lemma mk_opens_R_aux : #(opens )  #(set ( × )) :=
begin
  -- An open set in ℝ is uniquely determined by the rational balls included in it.
  -- (Any dense set would do just as well in place of ℚ.)
  let f := λ (S : opens ), {p :  ×  | ball (p.1 : ) p.2  S},
  suffices :  {S T}, f S = f T  S  T,
  { exact @mk_le_of_injective _ _ f (λ S T hST, (this hST).antisymm (this hST.symm)) },
  rintro S T hST x (hxS : x  S), show x  T,
  obtain ε, hεpos, hball := mem_nhds_iff.1 (mem_nhds_sets S.2 hxS),
  obtain εQ, h0εQ, hεQ := exists_pos_rat_lt (half_pos hεpos),
  have := ball_mem_nhds x (rat.cast_pos.2 h0εQ),
  obtain yR, yQ, rfl⟩, hyballx := dense_embedding_of_rat.dense.inter_nhds_nonempty this,
  have := set.subset.trans (ball_half_subset _ (ball_subset_ball hεQ.le hyballx)) hball,
  have : (yQ, εQ)  f S := set.subset.trans (ball_subset_ball hεQ.le) this,
  rw hST at this,
  exact this (mem_ball_comm.mp hyballx),
end

It's possible that you can do more by generalizing to dense embeddings or something


Last updated: May 07 2021 at 22:14 UTC