Zulip Chat Archive

Stream: lean4

Topic: Structure Extensions


view this post on Zulip François G. Dorais (Mar 16 2021 at 07:38):

First, I think it's really cool that this works as I expect it to:

structure Bar (α) where bar : α

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Bar α, Foo bar

#print FooBar
/-
inductive FooBar.{u_1} : Sort u_1 → Sort (max 1 u_1)
constructors:
FooBar.mk : {α : Sort u_1} → (_toBar : Bar α) → Foo _toBar.bar → FooBar α
-/

However, I don't understand how to make this work:

protected theorem FooBar.eq {α} :  (f g : FooBar α), f.bar = g.bar  f = g
| _,_⟩, _,_⟩, rfl => rfl
/-
dependent elimination failed, stuck at auxiliary equation
  { toBar := _toBar✝, toFoo := _toFoo✝ }.toBar.1 = { toBar := _toBar✝¹, toFoo := _toFoo✝¹ }.toBar.1
-/

Is there a reason why this shouldn't work?

PS: I kind of wish this shorthand worked too but this one seems like more of a rabbit hole.

structure Foo {α} (x : α) : Prop where foo : True

structure FooBar (α) extends Foo bar where bar : α

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:20):

protected theorem FooBar.eq {α} :  (f g : FooBar α), f.bar = g.bar  f = g
| ⟨⟨_⟩,_⟩, ⟨⟨_⟩,_⟩, rfl => rfl

works

view this post on Zulip François G. Dorais (Mar 16 2021 at 08:23):

Of course! I see the .1 was the hint in the error message... subtle! Thanks!


Last updated: May 18 2021 at 23:14 UTC