## Stream: new members

### Topic: lean4 structure equality

#### Arien Malec (Oct 24 2022 at 21:09):

What's the Lean4 approach for this proof (or even one direction of it?)

structure Foo where
mk :: (bar : Nat)

theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar := sorry


#### Arien Malec (Oct 24 2022 at 22:11):

should probably note that I've tried what I would consider the usual; rfl, various flavors of trying to destructure, rw etc.

#### Julian Berman (Oct 24 2022 at 22:16):

Possibly there's a clevererer way to do it (which I can't check because I can't update mathlib4 yet :/), but here's a simplistic way that seems to work:

structure Foo where
mk :: (bar : Nat)

theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar :=
⟨λ h => by rw [h],
λ h => by cases a; cases b; simp [h]⟩


seems to do it here at least.

#### Mario Carneiro (Oct 24 2022 at 22:18):

With the ext tactic you get it for free:

import Std.Tactic.Ext

@[ext] structure Foo where
mk :: (bar : Nat)

theorem eq_ext : ∀ (a b: Foo), a = b ↔ a.bar = b.bar := Foo.ext_iff


#### Arien Malec (Oct 24 2022 at 22:28):

Julian Berman said:

Possibly there's a clevererer way to do it (which I can't check because I can't update mathlib4 yet :/), but here's a simplistic way that seems to work:

structure Foo where
mk :: (bar : Nat)

theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar :=
⟨λ h => by rw [h],
λ h => by cases a; cases b; simp [h]⟩


seems to do it here at least.

OK, I get the mp direction, which seems obvious in retrospect. The mpr direction seems like magic.

I go from

case mpr.mk.mk
bar✝¹bar✝: Nat
h: { bar := bar✝¹ }.bar = { bar := bar✝ }.bar
⊢ { bar := bar✝¹ } = { bar := bar✝ }


to :tada: via simp [h] but it doesn't feel like there's anything to apply simp to that isn't already in the premise...

#### Mario Carneiro (Oct 24 2022 at 22:37):

Here's another way to write the proof:

theorem eq_ext (a b: Foo) : a = b ↔ a.bar = b.bar :=
⟨λ h => by rw [h],
λ h => by
match a, b, h with
| ⟨a_bar⟩, ⟨b_bar⟩, (h : a_bar = b_bar) =>
rw [h]⟩


#### Mario Carneiro (Oct 24 2022 at 22:38):

The point is that after the two cases, h, which has the type ⟨a_bar⟩.bar = ⟨b_bar⟩.bar, is definitionally equal to h : a_bar = b_bar and so we can use the same proof as the first half - we're just applying the mk function to both sides to get equal values.

Last updated: Dec 20 2023 at 11:08 UTC