Returning a dependent pair

Stream: new members

[Tomaz Gomes Mascarenhas]

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]

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

[Yaël Dillies]

(n : Nat) × f n does not make sense. Not sure why Lean does not throw an error at that point

[Adam Topaz]

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]

I'm also a little puzzled about this ((n : Nat) × f n). Is this some Lean4 thing I'm not familiar with?

[Adam Topaz]

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]

Does Lean4 have a new notation for sigma types?

[Adam Topaz]

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]

Lean 4 has (a : A) -> B a for dependent functions (pi types) and (a : A) × B a for dependent pairs (sigma types).

[Adam Topaz]

Nice!

[Tomaz Gomes Mascarenhas]

got it, thanks!

[Kyle Miller]

(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]

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)⟩