Zulip Chat Archive

Stream: new members

Topic: Show equality of structures by fields

Jesse Slater (Jan 03 2023 at 16:57):

I have a structure

structure SystemState where
  evenCount : Nat
  oddCount : Nat
deriving Repr

and I have defined

def emptyState : SystemState
  := {evenCount := 0, oddCount := 0}

I am writing a proof where I have a SystemState S, and have that S.evenCount = 0 and S.oddCount = 0. How do I show that S = emptyState?

Kevin Buzzard (Jan 03 2023 at 17:33):

Do cases on S and on emptyState, and then it should reduce to what you know. I don't know whether @[ext] has been ported to mathlib4 yet, but in Lean 3 + mathlib you could tag structures with @[ext] and then you could also use the ext tactic to reduce a goal S = emptyState to precisely what you have.

Jesse Slater (Jan 03 2023 at 20:12):

Thanks, ext seems to work

Last updated: Dec 20 2023 at 11:08 UTC