suffices to prove

Stream: general

[Kevin Buzzard]

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]

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]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

wlog not (c ⊂ d)?

[Kevin Buzzard]

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]

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

[Yury G. Kudryashov]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

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]

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