variables weirdness

Stream: general

[Sebastien Gouezel]

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.

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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.