## 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).

Nice!

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