## Stream: general

### Topic: finset.prod and fin.cons

#### Yury G. Kudryashov (Jun 12 2020 at 05:10):

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 (Jun 12 2020 at 05:11):

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 (Jun 12 2020 at 05:42):

give it the expected type

#### Mario Carneiro (Jun 12 2020 at 05:43):

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 (Jun 12 2020 at 05:43):

fin.cons should be @[elab_as_eliminator]

#### Yury G. Kudryashov (Jun 12 2020 at 05:56):

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

#### Yury G. Kudryashov (Jun 12 2020 at 05:57):

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

#### Mario Carneiro (Jun 12 2020 at 06:11):

I mean global @[elab_as_eliminator]

#### Mario Carneiro (Jun 12 2020 at 06:15):

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

#### Yury G. Kudryashov (Jun 12 2020 at 06:16):

@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 (Jun 12 2020 at 07:14):

I think I used the sum version last week

#### Johan Commelin (Jun 12 2020 at 07:16):

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

#### Sebastien Gouezel (Jun 12 2020 at 07:33):

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.

Last updated: Dec 20 2023 at 11:08 UTC