lean4 structure equality

Stream: new members

[Arien Malec]

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]

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

[Julian Berman]

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]

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]

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]

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]

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.