structures, classes, etc?

Stream: new members

[Thomas Laraia]

What do I use each for, and is there a good mental way to follow what I want to do when I want to construct something?

[Kevin Buzzard]

What's your background? group G is a class because given a type G 99 times out 100 it will have at most one group structure. But subgroup G is a structure because given a group G 99 times out of 100 it will have more than one subgroup.

[Thomas Laraia]

My background is undergraduate mathematics student headed into fourth year. I am working on the formalising-mathematics tutorial mentioned in the group theory conversation, and will specifically look at the group and subgroup section because I want to attempt a proof of Euler's theorem through group theory, as well as take a look at Lagrange's theorem. I browse the new members conversations and see structures and classes come up quite a bit and want to understand them so I can use them, since they seem directly relevant, although I will obviously borrow the definitions from groups and subgroups to get started.

[Thomas Laraia]

There are several things I am trying to get my head around.

import tactic

@[ext] structure partition (α : Type) :=
(C : set (set α))
(Hnonempty : ∀ X ∈ C, (X : set α).nonempty)
(Hcover : ∀ a, ∃ X ∈ C, a ∈ X)
(Hdisjoint : ∀ X Y ∈ C, (X ∩ Y : set α).nonempty → X = Y)

namespace partition

-- let α be a type, and fix a partition P on α. Let X and Y be subsets of α.
variables {α : Type} {P : partition α} {X Y : set α}

/-- If X and Y are blocks, and a is in X and Y, then X = Y. -/
theorem eq_of_mem (hX : X ∈ P.C) (hY : Y ∈ P.C) {a : α} (haX : a ∈ X)
  (haY : a ∈ Y) : X = Y :=
-- Proof: follows immediately from the disjointness hypothesis.
P.Hdisjoint _ _ hX hY ⟨a, haX, haY⟩

theorem mem_of_mem (hX : X ∈ P.C) (hY : Y ∈ P.C) {a b : α}
  (haX : a ∈ X) (haY : a ∈ Y) (hbX : b ∈ X) : b ∈ Y :=
begin
  -- you might want to start with `have hXY : X = Y`
  -- and prove it from the previous lemma
  have hXY : X = Y,
  { exact eq_of_mem hX hY haX haY },
  rw ← hXY,
  assumption,
end

end partition

section equivalence_classes

/-!

## Definition of equivalence classes

-/

-- Notation and variables for the equivalence class section:

-- let α be a type, and let R be a binary relation on R.
variables {α : Type} (R : α → α → Prop)

/-- The equivalence class of `a` is the set of `b` related to `a`. -/
def cl (a : α) :=
{b : α | R b a}

/-!

## Basic lemmas about equivalence classes

-/

/-- Useful for rewriting -- `b` is in the equivalence class of `a` iff
`b` is related to `a`. True by definition. -/
theorem mem_cl_iff {a b : α} : b ∈ cl R a ↔ R b a :=
begin
  -- true by definition
  refl
end

variables {R} (hR : equivalence R)
include hR

lemma cl_sub_cl_of_mem_cl {a b : α} :
  a ∈ cl R b →
  cl R a ⊆ cl R b :=
begin
  -- remember `set.subset_def` says `X ⊆ Y ↔ ∀ a, a ∈ X → a ∈ Y
  intro hab,
  intros z hza,
  rw mem_cl_iff at hab hza ⊢,
  obtain ⟨hrefl, hsymm, htrans⟩ := hR,
  exact htrans hza hab,
end

lemma cl_eq_cl_of_mem_cl {a b : α} :
  a ∈ cl R b →
  cl R a = cl R b :=
begin
  intro hab,
  -- remember `set.subset.antisymm` says `X ⊆ Y → Y ⊆ X → X = Y`
  apply set.subset.antisymm,
  { exact cl_sub_cl_of_mem_cl hR hab},
  { apply cl_sub_cl_of_mem_cl hR,
    obtain ⟨hrefl, hsymm, htrans⟩ := hR,
    exact hsymm hab }
end


end equivalence_classes





open partition


example (α : Type) : {R : α → α → Prop // equivalence R} ≃ partition α :=
-- We define constructions (functions!) in both directions and prove that
-- one is a two-sided inverse of the other
{ -- Here is the first construction, from equivalence
  -- relations to partitions.
  -- Let R be an equivalence relation.
  to_fun := λ R, {
    -- Let C be the set of equivalence classes for R.
    C := { B : set α | ∃ x : α, B = cl R.1 x},
    -- I claim that C is a partition. We need to check the three
    -- hypotheses for a partition (`Hnonempty`, `Hcover` and `Hdisjoint`),
    -- so we need to supply three proofs.
    Hnonempty := begin
      cases R with R hR,
      -- If X is an equivalence class then X is nonempty.
      show ∀ (X : set α), (∃ (a : α), X = cl R a) → X.nonempty,
      rintros _ ⟨a, rfl⟩,
      use a,
      rw mem_cl_iff,
      obtain ⟨hrefl, hsymm, htrans⟩ := hR,
      apply hrefl,
    end,
    Hcover := begin
      cases R with R hR,
      -- The equivalence classes cover α
      show ∀ (a : α), ∃ (X : set α) (H : ∃ (b : α), X = cl R b), a ∈ X,
      intro a,
      use cl R a,
      split,
      { use a },
      { apply hR.1 },
    end,
    Hdisjoint := begin
      cases R with R hR,
      -- If two equivalence classes overlap, they are equal.
      show ∀ (X Y : set α), (∃ (a : α), X = cl R a) →
        (∃ (b : α), Y = cl _ b) → (X ∩ Y).nonempty → X = Y,
      rintros X Y ⟨a, rfl⟩ ⟨b, rfl⟩ ⟨c, hca, hcb⟩,
      apply cl_eq_cl_of_mem_cl hR,
      apply hR.2.2,
        apply hR.2.1,
        exact hca,
      exact hcb,
    end },
  -- Conversely, say P is an partition.
  inv_fun := λ P,
    -- Let's define a binary relation `R` thus:
    --  `R a b` iff *every* block containing `a` also contains `b`.
    -- Because only one block contains a, this will work,
    -- and it turns out to be a nice way of thinking about it.
    ⟨λ a b, ∀ X ∈ P.C, a ∈ X → b ∈ X, begin
      -- I claim this is an equivalence relation.
    split,
    { -- It's reflexive
      show ∀ (a : α)
        (X : set α), X ∈ P.C → a ∈ X → a ∈ X,
      intros a X hXC haX,
      assumption,
    },
    split,
    { -- it's symmetric
      show ∀ (a b : α),
        (∀ (X : set α), X ∈ P.C → a ∈ X → b ∈ X) →
         ∀ (X : set α), X ∈ P.C → b ∈ X → a ∈ X,
      intros a b h X hX hbX,
      obtain ⟨Y, hY, haY⟩ := P.Hcover a,
      specialize h Y hY haY,
      exact mem_of_mem hY hX h hbX haY,
    },
    { -- it's transitive
      unfold transitive,
      show ∀ (a b c : α),
        (∀ (X : set α), X ∈ P.C → a ∈ X → b ∈ X) →
        (∀ (X : set α), X ∈ P.C → b ∈ X → c ∈ X) →
         ∀ (X : set α), X ∈ P.C → a ∈ X → c ∈ X,
      intros a b c hbX hcX X hX haX,
      apply hcX, assumption,
      apply hbX, assumption,
      assumption,
    }
  end⟩,
  -- If you start with the equivalence relation, and then make the partition
  -- and a new equivalence relation, you get back to where you started.
  left_inv := begin
    rintro ⟨R, hR⟩,
    -- Tidying up the mess...
    suffices : (λ (a b : α), ∀ (c : α), a ∈ cl R c → b ∈ cl R c) = R,
      simpa,
    -- ... you have to prove two binary relations are equal.
    ext a b,
    -- so you have to prove an if and only if.
    show (∀ (c : α), a ∈ cl R c → b ∈ cl R c) ↔ R a b,
    split,
    { intros hab,
      apply hR.2.1,
      apply hab,
      apply hR.1,
    },
    { intros hab c hac,
      apply hR.2.2,
        apply hR.2.1,
        exact hab,
      exact hac,
    }
  end,
  -- Similarly, if you start with the partition, and then make the
  -- equivalence relation, and then construct the corresponding partition
  -- into equivalence classes, you have the same partition you started with.
  right_inv := begin
    -- Let P be a partition
    intro P,
    -- It suffices to prove that a subset X is in the original partition
    -- if and only if it's in the one made from the equivalence relation.
    ext X,
    show (∃ (a : α), X = cl _ a) ↔ X ∈ P.C,
    dsimp only,
    split,
    { rintro ⟨a, rfl⟩,
      obtain ⟨X, hX, haX⟩ := P.Hcover a,
      convert hX,
      ext b,
      rw mem_cl_iff,
      split,
      { intro haY,
      obtain ⟨Y, hY, hbY⟩ := P.Hcover b,
      specialize haY Y hY hbY,
      convert hbY,
      exact eq_of_mem hX hY haX haY,
      },
      { intros hbX Y hY hbY,
        apply mem_of_mem hX hY hbX hbY haX,
      }
    },
    { intro hX,
      rcases P.Hnonempty X hX with ⟨a, ha⟩,
      use a,
      ext b,
      split,
      { intro hbX,
        rw mem_cl_iff,
        intros Y hY hbY,
        exact mem_of_mem hX hY hbX hbY ha,
      },
      { rw mem_cl_iff,
        intro haY,
        obtain ⟨Y, hY, hbY⟩ := P.Hcover b,
        specialize haY Y hY hbY,
        exact mem_of_mem hY hX haY ha hbY,
      }
    }
  end }

In the culmination of this exercise, in lines 226 and 236, obtain and rcases are used in the solution and I am still fighting a little bit with when these are applicable. I was happy to watch the demo on the leanprover community Youtube channel about proving there are infinitely many primes, because so far this is the structure I understood the best and will try to replicate, but there are still here big questions for me on moving forward in a proof through means like obtain.

[Kevin Buzzard]

obtain is just a glorified cases tactic.

[Kevin Buzzard]

e.g. obtain ⟨X, hX, haX⟩ := P.Hcover a just means : P is a partition, P.Hcover is the proof that for all a there's a block of the partition P such that a is in the block, P.Hcover a is the proof that for this specific a, there's a block of the partition P such that this a is in that block, and the obtain tactic just lets X be the subset, hX be the proof that it's in the set P.C of blocks and haX be the proof that $a\in X$.

[Kevin Buzzard]

rcases does the same sort of thing. You can do all of this stuff with the cases tactic but it's a bit longer.

[Kevin Buzzard]

If you're going into 4th year then I assume you understand the maths proof of what's going on here! Looks like I got lazy with the commenting.

[Kevin Buzzard]

Similarly rcases P.Hnonempty X hX with ⟨a, ha⟩ means the following: P is a partition, P.Hnonempty is the proof that all blocks in it are nonempty, X is a subset of alpha, hX is the proof that it's a block, so P.Hnonempty X hX is a proof that X is nonempty, i.e. has an element, and rcases P.Hnonempty X hX with ⟨a, ha⟩ just defines a to be such an element and lets ha be the proof that it's in X.

[Kevin Buzzard]

My idea with that exercise was that you could try and fill in all the sorrys on your own, using the tactics you know, and then you can look at my model answer to see how I did it. I intentionally use some more high-powered tactics to make my proof shorter, but you can do all the proofs here with the ten basic tactics (i.e. the stuff in the natural number game) as long as you know a little about how subsets work, and I learnt from that workshop that I hadn't really said enough about how subsets work. Maybe you would learn more if you just tried to fill in the sorrys yourself instead of being intimidated by my solution?

[Thomas Laraia]

Perfect, I will do that. I was working through it alone but there were three places where I hit a block and checked. I will do it properly again tonight. Thank you for the explanations of obtain and rcases, they make a lot of sense, I'm sure I will reread your comments several times over time to remember long term. Cheers!

[Kevin Buzzard]

I introduce obtain on line 96 or so

[Kevin Buzzard]

I introduce rcases on line 153 or so

[Kevin Buzzard]

@Thomas Laraia I just pushed a ton of comments about those proofs to the repo. You can check them out here.