finset.prod and fin.cons

Stream: general

[Yury G. Kudryashov]

I'm trying to formulate a simp lemma:

import data.fintype.card

open_locale big_operators

theorem fin.prod_univ_cons {M : Type*} [comm_monoid M] {n : ℕ} (x : M) (f : fin n → M) :
  ∏ i : fin (n + 1), (@fin.cons _ (λ _, M) x f i) = x * ∏ i : fin n, f i :=
sorry

and get the following error:

6:3: type mismatch at application
  ∏ (i : fin (n + 1)), fin.cons x f i
term
  λ (i : fin (n + 1)), fin.cons x f i
has type
  Π (i : fin (n + 1)), (λ (_x : fin (n + 1)), M) i : Type ?
but is expected to have type
  fin (n + 1) → ?m_1 : Type ?

[Yury G. Kudryashov]

It seems that Lean can't unify (λ _, β) i with β. Is there any way to add this lemma without adding a non-dependent version of fin.cons?

[Mario Carneiro]

give it the expected type

[Mario Carneiro]

theorem fin.prod_univ_cons {M : Type*} [comm_monoid M] {n : ℕ} (x : M) (f : fin n → M) :
  (∏ i : fin (n + 1), @fin.cons _ (λ _, M) x f i : M) = x * ∏ i : fin n, f i :=
sorry

[Mario Carneiro]

fin.cons should be @[elab_as_eliminator]

[Yury G. Kudryashov]

Do you mean local attribute [elab_as_eliminator] fin.cons?

[Yury G. Kudryashov]

If I add @[elab_as_eliminator] to the definition, the next few lemmas fail.

[Mario Carneiro]

I mean global @[elab_as_eliminator]

[Mario Carneiro]

Oof, yeah these are messy. I think either cons should take an explicit motive argument, or it should be nondependent

[Yury G. Kudryashov]

@Sebastien Gouezel you use fin.cons a lot in multilinear maps. What's your experience? How often did you hit something like the issue described above?

[Johan Commelin]

Isn't that lemma already there?

[Johan Commelin]

I think I used the sum version last week

[Johan Commelin]

Nevermind, I was confusing it with src#fin.prod_univ_succ

[Sebastien Gouezel]

Yes, I encountered several times the issue that (λ _, β) i and β don't always unify. Since fin.cons doesn't have too many implicit arguments, it wasn't too painful to provide explicitly the type to the @ version, though, and to add type annotations where necessary.