equality for structures

Stream: new members

[Jake Levinson]

Here is a lemma I am stuck on:

structure bundle (B : Type) :=
  (space : Type)
  (π : space → B)

structure bundle_map {B : Type} (E F : bundle B) :=
  (map : E.space → F.space)
  (h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
  (h1 : φ1.map = φ2.map) : φ1 = φ2 :
begin
  split
  /- invalid apply tactic, failed to unify
  φ1 = φ2
  with
  ?m_2 = ?m_2 -/
end

I thought that split or cases or something should work here. For example I can prove associativity of compositions (which involves showing that two bundle_maps are equal) that way:

def bundle_map.comp {B : Type} {E F G : bundle B}
  (φ' : bundle_map F G) (φ : bundle_map E F) : bundle_map E G :=
{ map := φ'.map ∘ φ.map,
  h   := by rw [← function.comp.assoc, φ'.h, φ.h], }
infix `∘∘`:110 := bundle_map.comp

lemma bundle_map.comp.assoc {B : Type} {E F G H : bundle B}
  (φ'' : bundle_map G H) (φ' : bundle_map F G) (φ : bundle_map E F) :
  (φ'' ∘∘ φ') ∘∘ φ = φ'' ∘∘ φ' ∘∘ φ := by split

Thanks for any help!

[Kyle Miller]

For this, you need an extensionality lemma. The @[ext] attribute is a way to generate one for you automatically:

@[ext]
structure bundle_map {B : Type} (E F : bundle B) :=
  (map : E.space → F.space)
  (h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
  (h1 : φ1.map = φ2.map) : φ1 = φ2 :=
begin
  ext x,  -- or ext1 to just do a single level; follow by `exact h1`

end

[Kevin Buzzard]

Cases works for me:

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
  (h1 : φ1.map = φ2.map) : φ1 = φ2 :=
begin
  cases φ1 with map1 h1,
  cases φ2 with map2 h2,
  simp * at *,
end

[Kevin Buzzard]

(Kyle's answer is in some sense "the same as mine", because you prove ext lemmas for structures precisely by doing cases on the components)

[Jake Levinson]

Thank you both!

[Kevin Buzzard]

PS your by split proof is bogus:

lemma bundle_map.comp.assoc {B : Type} {E F G H : bundle B}
  (φ'' : bundle_map G H) (φ' : bundle_map F G) (φ : bundle_map E F) :
  (φ'' ∘∘ φ') ∘∘ φ = φ'' ∘∘ φ' ∘∘ φ := rfl

[Jake Levinson]

Oooh.

[Kevin Buzzard]

split never closes goals unless they are somehow degenerate, in my experience.

[Kyle Miller]

Also, split is for splitting a goal that's a constructor of some kind (something with parts) -- the goal is an equality, which can't be split.

Using Kevin's direct proof, you'd want congr, like cases φ1, cases φ2, congr, exact h1,

[Kyle Miller]

I should have been paying more attention... you're proving the extensionality lemma that @[ext] generates of course, so my suggestion is sort of absurd.

@[ext]
structure bundle_map {B : Type} (E F : bundle B) :=
  (map : E.space → F.space)
  (h : F.π ∘ map = E.π)

lemma bundle_map.eq_of_map {B : Type} {E F : bundle B} (φ1 φ2 : bundle_map E F)
  (h1 : φ1.map = φ2.map) : φ1 = φ2 := bundle_map.ext _ _ h1

[Jake Levinson]

Thanks Kyle and Kevin! That's very helpful.