Zulip Chat Archive

Stream: general

Topic: variables weirdness


view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 18:46):

I have a weird behavior with variables and dot notation, in the following snippet

structure foo_class (H : Type) :=
(foo : H)

variables {H : Type}

structure foo_class.bar_class (G : foo_class H) (P : H  Prop) : Prop :=
(bar : P G.foo)

variable (G : foo_class H)

lemma works_fine {P : H  Prop} (h : G.bar_class P) : true := trivial

structure foo_class.bar_class' (P : H  Prop) : Prop :=
(bar' : P G.foo)

lemma why_oh_why {P : H  Prop} (h : G.bar_class' P) : true := sorry

I am declaring two structures foo_class.bar_class and foo_class.bar_class' which are exactly the same, except that in the first one the variable G is given right in the structure definition, while in the second one it is defined as a variable. Then dot notation works with the first one (the lemma works_fine, well, works fine), but it doesn't with the second.

view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 18:49):

Also, #print foo_class.bar_class gives

structure foo_class.bar_class : Π {H : Type}, foo_class H  (H  Prop)  Prop
fields:
foo_class.bar_class.bar :  {H : Type} {G : foo_class H} {P : H  Prop}, G.bar_class P  P G.foo

and #print foo_class.bar_class' gives

structure foo_class.bar_class' : Π {H : Type}, foo_class H  (H  Prop)  Prop
fields:
foo_class.bar_class'.bar' :  {H : Type} {G : foo_class H} {P : H  Prop}, foo_class.bar_class' G P  P G.foo

view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 18:50):

Note how it is not printed with the same dot notation.

view this post on Zulip Sebastien Gouezel (Jun 15 2020 at 19:41):

I just opened lean#334 to keep track of it. For now, declaring the variable in the definition is a good enough workaround for me.


Last updated: May 12 2021 at 04:19 UTC