# Zulip Chat Archive

## Stream: new members

### Topic: Returning a dependent pair

#### Tomaz Gomes Mascarenhas (Apr 07 2022 at 22:48):

Hello!

I need to write a function that returns a pair, in which the type of the second coordinate depends on the first coordinate. Something like this:

```
def f : Nat → Type
| 0 => Bool
| _ => Nat
def g : Nat → ((n : Nat) × f n)
| 0 => (0, true)
| k => (k, 1)
```

but with this code I'm getting this error:

```
type mismatch
(0, true)
has type
?m.118 × Bool : Type ?u.114
but is expected to have type
(n : Nat) × f n : Type
```

It seems Lean can't unify `f n`

with `Bool`

, even after I instantiate `n`

with `0`

. Am I missing something? Is there a different way to do dependent pattern matching?

#### Yaël Dillies (Apr 07 2022 at 23:04):

You should use a sigma type, not a product type. docs#sigma

#### Yaël Dillies (Apr 07 2022 at 23:05):

`(n : Nat) × f n`

does not make sense. Not sure why Lean does not throw an error at that point

#### Adam Topaz (Apr 07 2022 at 23:08):

```
def f : Nat → Type
| 0 => Bool
| _ => Nat
def g : Nat → (Σ (i : Nat), f i) := λ n =>
match n with
| 0 => ⟨0, true⟩
| k+1 => ⟨k+1, (1 : Nat)⟩
```

#### Adam Topaz (Apr 07 2022 at 23:11):

I'm also a little puzzled about this `((n : Nat) × f n)`

. Is this some Lean4 thing I'm not familiar with?

#### Adam Topaz (Apr 07 2022 at 23:12):

Hey, it works!

```
def f : Nat → Type
| 0 => Bool
| _ => Nat
def g : Nat → ((n : Nat) × f n) := λ k =>
⟨k, match k with | 0 => true | k+1 => (1 : Nat)⟩
```

#### Adam Topaz (Apr 07 2022 at 23:12):

Does Lean4 have a new notation for sigma types?

#### Adam Topaz (Apr 07 2022 at 23:15):

And for the original question, this works:

```
def f : Nat → Type
| 0 => Bool
| _ => Nat
def g : Nat → ((n : Nat) × f n)
| 0 => ⟨0,true⟩
| k+1 => ⟨k+1, (1 : Nat)⟩
```

I guess the issue was that you used regular parens, which really are only used for regular products, and I used the anonymous constructor brackets because (I suppose) this is just a plain old sigma type.

#### Kyle Miller (Apr 07 2022 at 23:17):

Lean 4 has `(a : A) -> B a`

for dependent functions (pi types) and `(a : A) × B a`

for dependent pairs (sigma types).

#### Adam Topaz (Apr 07 2022 at 23:18):

Nice!

#### Tomaz Gomes Mascarenhas (Apr 07 2022 at 23:18):

got it, thanks!

#### Kyle Miller (Apr 07 2022 at 23:19):

(I really wish we had these notations in math for indexed Cartesian products and indexed disjoint unions! They're so much more suggestive than $\prod_{a\in A} B_a$ and $\coprod_{a\in A}B_a$.)

#### Kyle Miller (Apr 07 2022 at 23:22):

FYI, for the dependent pairs, you don't need parentheses around the whole type:

```
def g : Nat → (n : Nat) × f n
| 0 => ⟨0, true⟩
| k+1 => ⟨k+1, (1 : Nat)⟩
```

Last updated: Dec 20 2023 at 11:08 UTC