## Stream: Is there code for X?

### Topic: by symmetry

#### 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?

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

#### Greg Price (Apr 11 2021 at 22:32):

Hmm interesting! I'll try that

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


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

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

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


#### Greg Price (Apr 11 2021 at 22:58):

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

#### Greg Price (Apr 11 2021 at 22:59):

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

#### Yakov Pechersky (Apr 11 2021 at 23:00):

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

Sure, one moment

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


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

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


#### Greg Price (Apr 14 2021 at 06:13):

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

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


#### 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:

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

#### Greg Price (Apr 14 2021 at 06:31):

Yeah, that makes sense

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


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

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

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

#### Mario Carneiro (Apr 14 2021 at 06:41):

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

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

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

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

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