by symmetry

Stream: Is there code for X?

[Greg Price]

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?

[Yakov Pechersky]

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

[Greg Price]

Hmm interesting! I'll try that

[Greg Price]

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

[Greg Price]

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

[Greg Price]

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.

[Yakov Pechersky]

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

[Greg Price]

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

[Greg Price]

Once for $T \leq S$ and once for $S \leq T$

[Yakov Pechersky]

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

[Greg Price]

Sure, one moment

[Greg Price]

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"
})

[Greg Price]

(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)

[Yaël Dillies]

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.

[Greg Price]

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

[Greg Price]

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,
})

[Greg Price]

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:

[Mario Carneiro]

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.

[Greg Price]

Yeah, that makes sense

[Mario Carneiro]

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

[Greg Price]

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

[Scott Morrison]

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.

[Greg Price]

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.)

[Mario Carneiro]

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

[Greg Price]

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.

[Greg Price]

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

[Greg Price]

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.

[Mario Carneiro]

@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