## Stream: general

### Topic: suffices to prove

#### Kevin Buzzard (Dec 28 2019 at 17:28):

Idly proving that equivalence relations are the same as partitions (thinking about a future Lean maths challenge). Here's a goal:

1 goal
X : Type,
R : {R // equivalence R},
c d : set X,
hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class ↑R x},
hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class ↑R x},
x : X,
hx : x ∈ c ∩ d
⊢ c = d


I want to prove this by saying "it suffices to prove c \sub d and d \sub c, but by symmetry we only need to prove c \sub d". I know I can factor out a lemma saying "if all the things in the local context are true then c \sub d" and then I can just apply this lemma twice -- but I don't see any obstruction in theory to having a tactic where I say "by set.subset.antisymm and the underlying symmetry, change the goal to c \sub d please" and maybe Lean replies "just convince me that x ∈ d ∩ c and you're good to go".

Can this already be done with some wlog trickery? I couldn't see how.

#### Kevin Buzzard (Dec 28 2019 at 17:29):

PS def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y}, not that it matters here (all that matters is that the local context is symmetric in c and d)

#### Patrick Massot (Dec 28 2019 at 17:49):

I came across the same question last week, and I don't think wlog helps here.

#### Patrick Massot (Dec 28 2019 at 17:52):

If you post a realistic MWE I can try to cook up something.

#### Kevin Buzzard (Dec 28 2019 at 17:55):

Is this realistic:

def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y}

example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X),
c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} →
d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d :=
begin
intros c d hc hd hcd,
sorry
end


?

#### Yury G. Kudryashov (Dec 28 2019 at 18:25):

wlog not (c ⊂ d)?

#### Kevin Buzzard (Dec 28 2019 at 18:40):

I don't think that's syntactically correct (but I don't know much about wlog). wlog not (c ⊂ d) gives me complaints about unknown identifiers c and d. wlog h: not (c ⊂ d) gives me

To generate cases at least two permutations are required, i.e. using [x y, y x] or exactly 0 or 2 variables
state:
X : Type,
R : X → X → Prop,
HR : equivalence R,
c d : set X,
hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hcd : c ∩ d ≠ ∅
⊢ c = d


#### Patrick Massot (Dec 28 2019 at 18:41):

Can you write a tactic script that you would like to see reduced to one tactic?

#### Yury G. Kudryashov (Dec 28 2019 at 18:52):

Sorry, does wlog h : (not (c ⊂ d)) work?

#### Kevin Buzzard (Dec 28 2019 at 18:56):

I get the same error "To generate cases at least two permutations..." as above.

#### Kevin Buzzard (Dec 28 2019 at 19:10):

import tactic

def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y}

example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X),
c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} →
d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d :=
begin
intros c d hc hd hcd,
/-
1 goal
X : Type,
R : X → X → Prop,
HR : equivalence R,
c d : set X,
hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hcd : c ∩ d ≠ ∅
⊢ c = d
-/
suffices htemp : ∀ (X : Type) (R : X → X → Prop) (HR : equivalence R) (c d : set X)
(hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x})
(hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x})
(hcd : c ∩ d ≠ ∅), c ⊆ d, -- I want this to be my final goal
apply set.subset.antisymm,
exact htemp X R HR c d (by assumption) (by assumption) (by assumption),
suffices htemp2 : d ∩ c ≠ ∅, -- I want this to be the last but one goal
exact htemp X R HR d c (by assumption) (by assumption) (htemp2), -- by assumption fails for htemp2
/- currently two goals.
first is
⊢ d ∩ c ≠ ∅
and we have a hypothesis
hcd : c ∩ d ≠ ∅,
-/
sorry,
/- other goal is overkill currently:

X : Type,
R : X → X → Prop,
HR : equivalence R,
c d : set X,
hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hcd : c ∩ d ≠ ∅
⊢ ∀ (X : Type) (R : X → X → Prop),
equivalence R →
∀ (c d : set X),
c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} →
d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c ⊆ d
-/
clear hcd hd hc c d HR R X,
intros X R HR c d hc hd hcd,
/-
X : Type,
R : X → X → Prop,
HR : equivalence R,
c d : set X,
hc : c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hd : d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x},
hcd : c ∩ d ≠ ∅
⊢ c ⊆ d
-/
sorry
end


#### Kevin Buzzard (Dec 28 2019 at 19:24):

It's the "suffices : htemp" line which I can't be bothered to write. On the blackboard I'd just say "we want c=d, but it suffices to prove c sub d as the other inclusion then follows by symmetry"

#### Kevin Buzzard (Dec 28 2019 at 19:24):

I don't have to quantify over X and R, I could have left them as constants

#### Kenny Lau (Dec 29 2019 at 00:11):

import tactic.wlog

def equivalence_class {X : Type} (R : X → X → Prop) (x : X) := {y : X | R x y}

example (X : Type) (R : X → X → Prop) (HR : equivalence R) : ∀ (c d : set X),
c ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} →
d ∈ {S : set X | ∃ (x : X), S = equivalence_class R x} → c ∩ d ≠ ∅ → c = d :=
begin
classical, intros c d hc hd hcd,
rw set.subset.antisymm_iff, by_contra h, rw not_and_distrib at h,
wlog h1 : ¬c ⊆ d := h using [c d, d c],
end


#### Kevin Buzzard (Dec 29 2019 at 01:34):

Oh nice :-) I think this is what Yury was thinking of?

Last updated: Aug 03 2023 at 10:10 UTC