Pi type/invalid field notation

Stream: new members

[Calle Sönne]

I have the following code and error I cant understand:
Code:

open_locale classical

lemma finite_prod_of_binary_prod [has_binary_products.{v} C] : ∀ (J : Type v) [fintype J], limits.has_limits_of_shape (discrete J) C
| J fin := if h : nonempty J then
begin
let x := classical.choice h,
let J' := {a // a ≠ x}, resetI,
have card_lt : fintype.card J' < fintype.card J, refine fintype.card_subtype_lt J _, exact x, simp,
have J'_lims : limits.has_limits_of_shape (discrete J') C, refine finite_prod_of_binary_prod J',
refine ⟨_⟩, intro,
let F' := (discrete.lift (subtype.val : J' -> J)) ⋙ F,
let test := J'_lims.has_limit,
have F'_has_lim : has_limit F', refine (J'_lims.has_limit F'),

end
else _
using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf (λ x, @fintype.card x.1 x.2)⟩]}

Error:

invalid field notation, function 'category_theory.limits.has_limits_of_shape.has_limit' does not have explicit argument with type (category_theory.limits.has_limits_of_shape ...)
state:
2 goals
C : Type u,
𝒞 : category C,
_inst_1 : limits.has_binary_products C,
finite_prod_of_binary_prod : Π (J : Type v) [_inst_2 : fintype J], limits.has_limits_of_shape (discrete J) C,
J : Type v,
fin : fintype J,
h : nonempty J,
x : J := classical.choice h,
J' : Type v := {a // a ≠ x},
card_lt : fintype.card J' < fintype.card J,
J'_lims : limits.has_limits_of_shape (discrete J') C,
F : discrete J ⥤ C,
F' : discrete {a // a ≠ x} ⥤ C := discrete.lift subtype.val ⋙ F,
test : Π (F : discrete J' ⥤ C), limits.has_limit F := limits.has_limits_of_shape.has_limit
⊢ limits.has_limit F'

I created the test hypothesis to show what the type of J'_lims.has_limit. It seems to me that I should just be able to supply F' (which is a functor from discrete J' -> C). What am I missing?

If it helps this is the definition of has_limits_of_shape:

class has_limits_of_shape :=
(has_limit : Π F : J ⥤ C, has_limit F)

[Calle Sönne]

Alternative quesiton: How do I make lean expand the ... in the error?

[Johan Commelin]

First remark @Calle Sönne: that should be a def, not a lemma. This might miraculously solve some problem, but probably not.

[Scott Morrison]

I don’t think you need to expand the .... The problem is that you’re trying to access a field of a class as if it were a structure.

[Scott Morrison]

(Back later.)

[Kenny Lau]

let test := J'_lims.has_limit should be the culprit, for the reason described above

[Calle Sönne]

Thank you, I have always treated classes and structures the same but I found the solution now.

[Kevin Buzzard]

@Calle Sönne do you know about the dot notation? When I learnt about this properly things started making a whole lot more sense to me.

[Calle Sönne]

I dont think so

[Kevin Buzzard]

I'm sure other people will think about things differently, but for me one big difference between classes and structures is that the dot notation works differently.

[Calle Sönne]

yeah yesterday I found out that with structures you have to refer to the structure itself to use dot notation, instead of a term of that structure.

[Calle Sönne]

no wait other way around

[Kevin Buzzard]

This was why I mentioned it -- it was one of the times when I had some "aha" moment and things got clearer.

[Kevin Buzzard]

class myclass (X : Type) :=
(b : X)
(c : ℕ)

structure mystructure (Y : Type) :=
(b : Y)
(c : ℕ)

#check @myclass.b -- X explicit
#check @mystructure.b -- Y implicit

def A : mystructure ℕ := ⟨4, 37⟩
instance : myclass ℤ := ⟨5, 37⟩ -- no name by default

variables (P Q : Type) (s : mystructure P) [myclass Q]
-- don't have a name for the class analogue of s!

#check A.c -- works fine
-- A has type `mystructure [something]` so `A.c *means* mystructure.c A`
-- this is the powerful dot notation. It's why `h.symm` works if `h : a = b`!
#check mystructure.c A -- even prettyprinter changes it to `A.c`

#check s.c -- works fine
-- but what are the analogues for classes?

#check myclass.c Q
#check myclass.c ℤ
-- have to do it this way because no names, but X explicit in myclass.c so it's OK

I know this is all trivial but I remember being very stuck on all this once.

[Kevin Buzzard]

We used h.symm for h : A = B on Thursday and I remember almost mentioning all this to you then.

[Kevin Buzzard]

It works because h has type eq <something>

[Kevin Buzzard]

but without the variable names, when you're dealing with classes, you can't use this so they had to give you another way.

[Kevin Buzzard]

example (R : Type) [myclass R] : ℕ  :=
begin
  exact _inst_2.c -- if you haven't got instances turned off in VS Code you can see it
  -- you're not supposed to think about the names but the names are there
end

[Johan Commelin]

@Kevin Buzzard I guess it's worth it to dump those examples in dot_notation.md in a docs folder. I've never really struggled with these, for some reason :oops: But looking at you examples, I can understand how this can lead to confusion.

[Kevin Buzzard]

Johan I think you had much more of a programming background when you came to this (like Patrick). I think there are lots of languages which use this dot notation, I just didn't know it at all, and the fact that it worked slightly differently for classes than structures just added to the confusion.

[Johan Commelin]

Maybe... I've played with other programming languages before, but so had you. I'm quite a cargo cult programmer actually. (That's also how I've learned Lean :hushed:)

[Kevin Buzzard]

I think that you were just better at them ;-)