simple set proof

Stream: new members

[Kevin Doran]

Hi everyone.

I'm reading the fantastic "Logic and Proof" guide. My first attempt to explore outside the guide was to try prove the simple example pasted below.
I have two questions:

• is there a more efficient way to set up the problem statement? The worded description
  of the problem is so simple, yet I use an additional 4 propositions in Lean.

• how to replace the single 'sorry'?

import data.set -- unused, but I think I need it to replace the 'sorry' below.

-- Problem Statement
-- Let a, b, c, d be objects such that {a, b} = {c, d}. Show that at least one
-- of the two statements "a = c and b = d" and "a = d and b = c" hold.

section
variable U : Type
-- There are 4 objects: a, b, c and d.
variables a b c d: U
-- There are two sets.
--   s₁ = {a, b}
--   s₂ = {c, d}
-- This seems to require 2 variables and 4 hypotheses. Is there a better way of
-- constructing the sets?
variables s₁  s₂ : set U
-- 1. a and b are in s₁.
-- 2. c and d are in s₂.
variables (h1 : a ∈ s₁ ∧ b ∈ s₁) (h2 : c ∈ s₂ ∧ d ∈ s₂)
-- 3. Nothing other than a and b are in s₁.
-- 4. Nothing other than c and d are in s₂.
variables (h3 : ∀ x, x ∈ s₁ → x = a ∨ x = b)
variables (h4 : ∀ x, x ∈ s₂ → x = c ∨ x = d)

-- Proof outline:
-- a = c or a = d
-- case 1: if a = c, we have b = d
-- case 2: if a = d, we have b = c
-- Thus, (a = c ∧ b = d) ∨ (a = d ∧ b = c).

example (h5 : s₁ = s₂) : (a = c ∧ b = d) ∨ (a = d ∧ b = c) :=
    -- 1. Somehow use s₁ = s₂ to get h6. Can I use the reverse of set.ext somehow?
    have h6 : ∀ x, x ∈ s₁ ↔ x ∈ s₂, from sorry, -- using h5
    have a ∈ s₂, from (iff.elim_left (h6 a)) h1.left,
    have b ∈ s₂, from (iff.elim_left (h6 b)) h1.right,
    have h7 : a = c ∨ a = d, from (h4 a) ‹ a ∈ s₂›,
    have h8 : b = c ∨ b = d, from (h4 b) ‹ b ∈ s₂›,
    show (a = c ∧ b = d) ∨ (a = d ∧ b = c),
        from or.elim h7
        (assume : a = c,
         have b = d, from or.elim h8
            (assume : b = c,
             have b = a, from eq.trans this (eq.symm ‹a = c›),
             have d ∈ s₁, from iff.elim_right (h6 d) h2.right,
             have d = a ∨ d = b, from (h3 d) this,
             have d = a, from or.elim this
                (assume : d = a, this)
                (assume : d = b, show d = a, from eq.subst ‹b = a› this),
             show b = d, from eq.trans ‹b = a› (eq.symm ‹d = a›))
            (assume : b = d, this),
         have a = c ∧ b = d, from and.intro ‹a = c› ‹b = d›,
         or.inl this)
        -- A bit of duplication follows. A theorem might be a good fit to remove
        -- the duplication.
        (assume : a = d,
         have b = c, from or.elim h8
            (assume : b = c, this)
            (assume : b = d,
             have b = a, from eq.trans this (eq.symm ‹a = d›),
             have c ∈ s₁, from iff.elim_right (h6 c) h2.left,
             have c = a ∨ c = b, from (h3 c) this,
             show b = c, from or.elim this
                (assume : c = a,
                 show b = c, from eq.trans ‹b = a› (eq.symm this))
                (assume : c = b, eq.symm this)
            ),
         have a = d ∧  b = c, from and.intro ‹a = d› ‹b = c›,
         or.inr this)
end

I'm excited to join this community!

[Kevin Buzzard]

def s₁ : set U := {a, b}
def s₂ : set U := {c, d}

[Kevin Buzzard]

Course, this breaks everything ;-)

[Kevin Doran]

Thanks for the speedy reply, @Kevin Buzzard! Using that notation, what propositions become available? Is there docs/source on that syntax?

[Kevin Buzzard]

erm, does Theorem Proving In Lean talk about it?

[Kevin Buzzard]

Sticking with what you did, have h6 : ∀ x, x ∈ s₁ ↔ x ∈ s₂, by intros; rw h5,

[Kevin Buzzard]

I don't know how many theorems there are about sets with two elements in the library! Here's a place to look: https://leanprover-community.github.io/mathlib_docs/data/set/basic.html

[Kevin Buzzard]

by puts you into tactic mode (like begin ... end) and rw is a tactic which is hard to emulate in term mode (the mode you're writing in).

[Kevin Buzzard]

I can't find example (a b x : U) : x ∈ ({a, b} : set U) ↔ x = a ∨ x = b in mathlib :-/

[Kevin Doran]

Regarding the syntax:

def s₁: set U := {a, b}

I did a search for 'set' on the "Theorem Proving in Lean" guide, but I didn't recognize anything related to that syntax. But quite likely I might need some more background knowledge before I can make that call.

I checked out the mathlib docs on set/basic. It looked like I could use set.ext_iff, but the IDE reports unknown identifier for set.ext_iff.

[Kevin Buzzard]

Did you import data.set.basic or data.set?

[Kevin Doran]

Just data.set, and tried referencingext_iffwith set.basic.ext_iff and set.ext_iff.
Should it be import data.set.basic?

[Kevin Buzzard]

theorem set.mem_doubleton_iff (a b x : U) : x ∈ ({a, b} : set U) ↔ x = a ∨ x = b :=
⟨by rintro (h | h | h); cases h; simp,
  begin rintro (h | h), {right, left, assumption}, {left, assumption} end⟩

I'm sure there will be a much better proof of that.

[Kevin Buzzard]

import data.set

#check set.ext_iff -- set.ext_iff : ∀ (s t : set ?M_1), s = t ↔ ∀ (x : ?M_1), x ∈ s ↔ x ∈ t

Is your mathlib over a year old? That might also explain it

[Joe]

I remember the definition of {a, b} is this

lemma foo (a b x : α) : (x ∈ ({a, b} : set α)) ↔ x = b ∨ x = a ∨ false := iff.rfl

and so

lemma foo (a b x : α) : (x ∈ ({a, b} : set α)) ↔ x = b ∨ x = a ∨ false := iff.rfl

example (a b x : α) : x ∈ ({a, b} : set α) ↔ x = b ∨ x = a :=
by rw [foo, or_false]

[Kenny Lau]

import data.set.basic

theorem set.mem_doubleton_iff {U : Type*} (a b x : U) : x ∈ ({a, b} : set U) ↔ x = a ∨ x = b :=
by simp [or.comm]

[Kevin Doran]

Just using the live env https://leanprover.github.io/live/3.4.1

[Kevin Buzzard]

eew your mathlib is very old, use the more modern live env

[Kevin Buzzard]

Try a challenge here: https://github.com/kbuzzard/xena/blob/master/Maths_Challenges/challenges.md . That'll take you to a modern mathlib

[Kevin Buzzard]

Then delete the challenge and bookmark ;-)

[Kevin Doran]

Okay! That explains a lot. I thought there was some special syntax to use ext_iff from ext, but it's just an old version!

[Kevin Doran]

One final question: if I see some other unknown syntax, like the set notation {a , b}, is there a method of searching Lean code or mathlib for the definition?

[Kevin Buzzard]

If you see some unknown notation, then you can search for it with #print notation. This does not work with the following very small amount of Lean inbuilt syntax:

[a, b]
{a, b, c}
∀
∃

and the ones I've forgotten

[Kevin Doran]

okay, noted. Thanks a million!

[Kevin Buzzard]

Most of the time Lean is very good at being able to tell you absolutely everything about an object which you can't understand. But there are just a few edge cases which you have to know.

[Kevin Buzzard]

This might change in Lean 4.

[Joe]

Or you can shut down notations entirely and see what they really are

set_option pp.notation false

lemma foo (a b x : α) : (x ∈ ({a, b} : set α)) ↔ x = b ∨ x = a ∨ false :=
begin
  -- iff (has_mem.mem x (has_insert.insert b (singleton a))) (or (eq x b) (or (eq x a) false))
end

[Joe]

So {a, b} is has_insert.insert b (singleton a) (set.insert b (singleton a)).

[Kevin Buzzard]

oh wow I thought that this would just give you junk.

[Kevin Buzzard]

That trick works for ∃ too, but not for ∀