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 aABa\prod_{a\in A} B_a and aABa\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