Still more homework help - subgroups

Stream: new members

[Jeremy Teitelbaum]

I'm working through @Kevin Buzzard 's course and I'm looking at

theorem ext' {H K : subgroup G} (h : H.carrier = K.carrier) : H = K :=
begin
  -- first take H and K apart
  cases H, -- H now broken up into its underlying 3-tuple.
  cases K,
  -- and now it must be obvious, so let's see if the simplifier can do it.
  simp,
  assumption,
end

For the life of me I cannot figure out what simp is doing here. The context is:

G: Type
_inst_1: group G
H_carrier: set G
H_one_mem': 1 ∈ H_carrier
H_mul_mem': ∀ {x y : G}, x ∈ H_carrier → y ∈ H_carrier → x * y ∈ H_carrier
H_inv_mem': ∀ {x : G}, x ∈ H_carrier → x⁻¹ ∈ H_carrier
K_carrier: set G
K_one_mem': 1 ∈ K_carrier
K_mul_mem': ∀ {x y : G}, x ∈ K_carrier → y ∈ K_carrier → x * y ∈ K_carrier
K_inv_mem': ∀ {x : G}, x ∈ K_carrier → x⁻¹ ∈ K_carrier
h: {carrier := H_carrier, one_mem' := H_one_mem', mul_mem' := H_mul_mem', inv_mem' := H_inv_mem'}.carrier = {carrier := K_carrier, one_mem' := K_one_mem', mul_mem' := K_mul_mem', inv_mem' := K_inv_mem'}.carrier
⊢ {carrier := H_carrier, one_mem' := H_one_mem', mul_mem' := H_mul_mem', inv_mem' := H_inv_mem'} = {carrier := K_carrier, one_mem' := K_one_mem', mul_mem' := K_mul_mem', inv_mem' := K_inv_mem'}

I think the idea is: since the carriers are the same by h, you can use all the other hypotheses to show equality of the other components and get the result. But what are the actual manipulations to do this?

[Johan Commelin]

Hmm, I would think congr in place of simp should also work.

[Johan Commelin]

Which roughly means: "match the LHS up with the RHS, and turn all their differences into new subgoals"

[Patrick Massot]

Note that all other fields are proofs, so they are equal in a very strong sense as soon as they prove the same thing.

[Patrick Massot]

So Lean is applying injectivity of constructors of inductive types for you, as well as the proof irrelevance axiom.

[Jeremy Teitelbaum]

Patrick Massot said:

Note that all other fields are proofs, so they are equal in a very strong sense as soon as they prove the same thing.

Can you say a little bit more? about this? It seems like if you have a compound object and you want to prove equality, you need to prove
equality of the components. So the idea that congr would split the situation up into subgoals makes sense to me, with a subgoal for each component. But the equality of the component
proofs depends on equality of the carriers. It all seems magic.

[Patrick Massot]

It is indeed a bit subtle. But you really don't need to understand this in order to use Lean. That kind of extensionality lemma is automatically generated in practice.

[Jeremy Teitelbaum]

OK, I will table this for now and hope that clarity emerges from experience.

[Kevin Buzzard]

Yeah I had a choice here. I could either have written @[ext] structure subgroup... on line 26 of that file, which would have generated xena.subgroup.ext automatically (and which up to choice of brackets would be the same as ext' above) or I could have done it this way. In my copy of the repo I just seem to finish the proof with simp * at *. My take on this is "the thing is mathematically entirely trivial, the goal follows from h, I don't quite understand equality of structures and furthermore I even know that whatever equality of structures means it will change in Lean 4 (we'll have eta for structures, whatever that means), but I do know that the simplifier will know all the relevant lemmas so let's just use it"

[Kevin Buzzard]

This is the relevant Lean 4 issue.

[Kevin Buzzard]

PS Lean does not do magic, but on the other hand I don't understand what it's doing (and don't need to understand). Others here will if you really want to know what's going on. You could ask in #general what is happening under the hood and some expert will explain (Patrick probably knows but I don't know how often he frequents #new members )

[Kevin Buzzard]

The line I don't fully understand is congr.

theorem ext' {H K : subgroup G} (h : H.carrier = K.carrier) : H = K :=
begin
  -- first take H and K apart
  cases H, -- H now broken up into its underlying 3-tuple.
  cases K,
  congr,
  dsimp at h,
  assumption,
end

[Jeremy Teitelbaum]

Kevin Buzzard said:

PS Lean does not do magic,

Any sufficiently advanced technology is indistinguishable from magic.

[Kevin Buzzard]

I often feel that stuff like this is type theory 101 and the reason I don't know it is that I never went to any computer science courses, so it might just be my backwardness rather than the advancedness of the technology in this case.

[Kevin Buzzard]

But I'll be teaching this again in about a month so I'd be interested in hearing any more details if you get to the bottom of them!

[Jeremy Teitelbaum]

I've taken CS courses, and even taught them, but this is all very new to me and feels very strange. I think I just don't have any real understanding of what "dependent type theory" really is. But I guess that is what makes it interesting.

[Jeremy Teitelbaum]

I like your utilitarian attitude though, it's inspiring.

[Patrick Massot]

You get to decide why stuff is interesting to you.

[Patrick Massot]

And you can choose to spend time thinking about foundational stuff. What Kevin and I are saying is that you don't need to, at least if you only want to formalize math.

[Kevin Buzzard]

I'm living proof that you don't need to understand the details of equality of structures in order to formalise maths! On the other hand I am curious. It might be something to do with docs#heq :shrug:

[Ruben Van de Velde]

Not sure if it helps, but this also works:

variables {G : Type*} [group G]
theorem ext' {H K : subgroup G} (h : H.carrier = K.carrier) : H = K :=
begin
  -- first take H and K apart
  cases H, -- H now broken up into its underlying 3-tuple.
  cases K,
  dsimp only at h,
  subst h,
end

[Kevin Buzzard]

So I guess the question is: equality is defined as an inductive type and its recursor, automatically generated, is the substitution property a = b -> P a -> P b. Can one now write down an explicit P such that if a=H.carrier and b=K.carrier then P a can be proved by rfl and P b is the equality we want?

[Eric Wieser]

Another way to write it:

variables {G : Type*} [group G]
theorem ext' : ∀ {H K : subgroup G} (h : H.carrier = K.carrier), H = K
| ⟨Hc, _, _, _⟩ ⟨Kc, _, _, _⟩ rfl := rfl

[Eric Wieser]

(but that's worse because you have to count the _s)

[Jeremy Teitelbaum]

I am going to try to make sense of Chapter 8 of TPIL and then come back to this discussion.

[Kevin Buzzard]

The equation compiler is pretty spectacularly good at this sort of thing but I wanted to keep all proofs within begin end blocks for my students