## Stream: new members

### Topic: quantification over zip

#### Horatiu Cheval (Apr 09 2021 at 19:34):

In the following example, what's the reason for which well_typed_list1 and well_typed_list2 work fine, while in well_typed_list3 Lean doesn't x see as a product?

import data.list.alist

inductive type
| zero : type
| arrow : type → type → type

infixr ↣ : 50 := type.arrow --input with \ pr

inductive preterm : Type
| suc : preterm
| app : preterm → preterm → preterm

@[reducible]
def context := alist \$ λ _ : ℕ, type

open type preterm

inductive well_typed (ctx : context) : preterm → type → Prop
| suc : well_typed suc (zero ↣ zero)
| app {σ τ} {t u} : well_typed t (σ ↣ τ) → well_typed u σ → well_typed (t.app u) τ

def well_typed_list1 (ctx : context) : list preterm → list type → Prop :=
λ ts σs, ∀ x ∈ list.zip ts σs, (by {exact (well_typed ctx x.fst x.snd)})

def well_typed_list2 (ctx : context) : list preterm → list type → Prop :=
λ ts σs, ∀ x : preterm × type, x ∈ list.zip ts σs → well_typed ctx x.fst x.snd

def well_typed_list3 (ctx : context) : list preterm → list type → Prop :=
λ ts σs, ∀ x ∈ list.zip ts σs, well_typed ctx x.fst x.snd
/-
invalid field notation, type is not of the form (C ...) where C is a constant
x
has type
?m_1
-/


#### Yury G. Kudryashov (Apr 09 2021 at 20:41):

In the first definition lean deduces the type of x before evaluating the tactic mode term. In the second definition you explicitly specify the type. In the third definition lean doesn't know the type of x when it needs to parse x.fst. It should work if you add a type annotation somewhere or use prod.fst x.

#### Horatiu Cheval (Apr 09 2021 at 20:47):

It makes sense. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC