Zulip Chat Archive

Stream: new members

Topic: struct equality


Evan Lohn (Nov 21 2021 at 23:56):

I saw a topic about this in #general, but it didn't answer the more general question I have. How do I define equality for a new type of structure I want to use? i.e.

import data.equiv.basic
import data.finset.basic
import data.prod

structure foo (α β: ):=
mk :: (edge : (fin α)  (fin β)) (h: α < β)

lemma foos_equal {a b : } {edge1 edge2 : (fin a)  (fin b)} {h1 h2: _} (h: edge1 = edge2): (foo.mk edge1 h1) = (foo.mk edge2 h2) :=
begin
  -- ext, -- (doesn't work?)
  sorry
end

I have a more complicated setting where I'd like to prove things that look like this; the general idea is to be able to define and use an equivalence that hinges on the data used to create the struct and not the proofs about that data. Any help would be greatly appreciated!

Kevin Buzzard (Nov 21 2021 at 23:57):

@[ext]
structure foo (α β: ):=
mk :: (edge : (fin α)  (fin β)) (h: α < β)

lemma foos_equal {a b : } {edge1 edge2 : (fin a)  (fin b)} {h1 h2: _} (h: edge1 = edge2): (foo.mk edge1 h1) = (foo.mk edge2 h2) :=
begin
  ext, -- works!
  dsimp only,
  rw h,
end

Eric Wieser (Nov 21 2021 at 23:58):

subst h ought to work on your goal, no ext needed (because you have mk on both sides of the = so there's nothing that needs to be pulled apart)


Last updated: Dec 20 2023 at 11:08 UTC