# Zulip Chat Archive

## Stream: new members

### Topic: use proof in function

#### Joscha Mennicken (Nov 10 2021 at 13:35):

I'm wondering if it is possible to define a function like

```
myPrev (n : Nat) : n != 0 → Nat
```

or

```
myPrev : {n : Nat // n != 0} → Nat
```

When I tried, I expected there to be some way to get a `n = 0`

in the `| Nat.zero => ...`

case of a `match n with`

, but couldn't find any.

#### Floris van Doorn (Nov 10 2021 at 13:47):

This works:

```
def myPrev : (n : Nat) → n != 0 → Nat
| n+1, _ => n
def myPrev' : {n : Nat // n != 0} → Nat
| ⟨n+1, _⟩ => n
```

Lean will automatically figure out that you don't need to provide the `0`

case.

#### Floris van Doorn (Nov 10 2021 at 13:51):

If you want to use the word `match`

, you can do this:

```
def myPrev (n : Nat) (h : n != 0) : Nat :=
match n, h with
| 0, _ => by contradiction -- this line is optional, and can be removed
| n+1, _ => n
```

#### Floris van Doorn (Nov 10 2021 at 13:52):

In particular, you have to put `h`

in the match, so that it changes when you consider different cases on `n`

.

#### Joscha Mennicken (Nov 10 2021 at 13:54):

Thanks, that second example was what I was looking for. It's cool that the first version works, but it's a bit too much magic to understand what's going on.

#### Joscha Mennicken (Nov 10 2021 at 13:58):

I'm still wondering if there's a way to end up with a hypothesis `n = 0`

in the first match case and `n != 0`

(or `n = x + 1`

or similar) in the second and to then use the `n = 0`

as contradiction to `n != 0`

instead of using `0 != 0`

as contradiction.

#### Joscha Mennicken (Nov 10 2021 at 14:01):

Something like

```
def myPrev (n : Nat) (h : n != 0) : Nat :=
have hn : n = n := Eq.refl n
match n, hn with
| 0, _ => sorry
| x+1, _ => x
```

but where lean doesn't rewrite all occurrences of `n`

in `hn`

#### Floris van Doorn (Nov 10 2021 at 19:00):

Oh, I see what you mean.

Yes, you can write

```
def myPrev (n : Nat) (h : n != 0) : Nat :=
match n_eq_0:n with
| 0 => by subst n_eq_0; contradiction
| n+1 => n
```

#### Eric Wieser (Nov 10 2021 at 19:12):

Note you could also just send `0 => 0`

, and your function would be equal

#### Joscha Mennicken (Nov 12 2021 at 14:20):

That makes sense. Thanks for those answers, although I'm slightly surprised you can't put a space before the colon, only after: `match n_eq_0: n with`

.

Last updated: Dec 20 2023 at 11:08 UTC