quantification over zip

Stream: new members

[Horatiu Cheval]

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]

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]

It makes sense. Thanks!