# Zulip Chat Archive

## Stream: new members

### Topic: basic dependent types question

#### Rado Kirov (Mar 27 2022 at 04:37):

Hello, I am playing with LEAN and quite new to dependent types so I have some basic questions. A function that takes a value and returns a type makes sense to me

```
def f(x: Nat) = if x > 1 then Nat else Bool
```

but what is a value of type `f x`

and how does one construct one? My simple attempt to construct a typed pair is not accepted by LEAN

```
def test := Sigma.mk 2 1
```

Adding explicit type assertion `(1 : f 2)`

doesn't seem to help. Doesn't LEAN evaluate `f 2`

at type-checking time turn it into `Nat`

and pass the checker?

#### Kyle Miller (Mar 27 2022 at 06:04):

What you're running into with `(1 : f 2)`

is that there's a somewhat complicated system in Lean to turn numerals into values -- it's able to tell that `f 2`

is `Nat`

, but that takes a stronger sort of evaluation than it's willing to do. The error I'm seeing is `failed to synthesize instance OfNat (f 2) 1`

. That means it's trying to take the natural number `1`

and interpret it as a `f 2`

, which it doesn't immediately know how to do. You can help it out though with `((1 : Nat) : f 2)`

.

#### Kyle Miller (Mar 27 2022 at 06:08):

With `Sigma`

, Lean usually needs help to figure out *which* `Sigma`

you mean (especially here -- how is it supposed to guess to use `f`

?) Even so, you need to give it the `(1 : Nat)`

hint to help it interpret the natural number literal.

```
def test : Sigma f := Sigma.mk 2 (1 : Nat)
```

#### Kyle Miller (Mar 27 2022 at 06:09):

That `Sigma f`

can also be written using the `Σ x, f x`

notation

#### Kyle Miller (Mar 27 2022 at 06:15):

This `OfNat`

business doesn't apply to things that aren't literals. For example this passes the type checker:

```
def mk2 (n : Nat) : f 2 := n
```

#### Rado Kirov (Apr 03 2022 at 04:11):

Ah, makes sense. Extra confusion around literals. A quick follow up then. How would I tell LEAN that the following function has type `(x: Nat) -> f x`

(where `f x`

is above).

```
def fn(x: Nat) : f x = if x > 1 then (1 : Nat) else false
```

This doesn't seem to work.

#### Kyle Miller (Apr 03 2022 at 04:33):

It won't fix it, but make sure to use `:=`

instead of `=`

for a definition.

The reason things worked with, for example, `(true : f 0)`

is that Lean is able to compute what `f 0`

is. In an `if`

expression, however, at best you have an additional assumption `x > 1`

, but that's not enough for Lean to compute what `f x`

might be (`x`

is still a variable, it's not a literal number). You can help it out using tactics though:

```
def fn(x: Nat) : f x :=
if h : x > 1
then by
simp [f, h]
exact (1 : Nat)
else by
simp [f, h]
exact false
```

I'm using the "dependent if" notation; here `h`

is a proof of either `x > 1`

or its negation.

#### Kyle Miller (Apr 03 2022 at 04:42):

You can also define some constructors

```
def f (x : Nat) := if x > 1 then Nat else Bool
def f.mk_nat (x : Nat) (h : x > 1) (n : Nat) : f x := by
simp [f, h]
exact n
-- I wasn't sure whether to write this as `¬ x > 1` just to make the `if` more convenient.
def f.mk_bool (x : Nat) (h : x ≤ 1) (b : Bool) : f x := by
rw [← Nat.not_lt_eq] at h
simp [f, h]
exact b
def fn (x: Nat) : f x :=
if h : x > 1 then f.mk_nat x h 1 else f.mk_bool x (Nat.not_lt_eq _ _ ▸ h) false
```

#### Rado Kirov (Apr 04 2022 at 18:40):

I didn't know about the 'dependent if' notation, this makes a lot of sense. Thanks!

Last updated: Dec 20 2023 at 11:08 UTC